what4-1.0: Solver-agnostic symbolic values support for issuing queries

Copyright(c) Galois Inc 2014-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.ProgramLoc

Contents

Description

This module primarily defines the Position datatype for handling program location data. A program location may refer either to a source file location (file name, line and column number), a binary file location (file name and byte offset) or be a dummy "internal" location assigned to generated program fragments.

Synopsis

Documentation

data Position Source #

Constructors

SourcePos !Text !Int !Int

A source position containing filename, line, and column.

BinaryPos !Text !Word64

A binary position containing a filename and address in memory.

OtherPos !Text

Some unstructured position information that doesn't fit into the other categories.

InternalPos

Generated internally by the simulator, or otherwise unknown.

Instances
Eq Position Source # 
Instance details

Defined in What4.ProgramLoc

Ord Position Source # 
Instance details

Defined in What4.ProgramLoc

Show Position Source # 
Instance details

Defined in What4.ProgramLoc

Pretty Position Source # 
Instance details

Defined in What4.ProgramLoc

Methods

pretty :: Position -> Doc #

prettyList :: [Position] -> Doc #

NFData Position Source # 
Instance details

Defined in What4.ProgramLoc

Methods

rnf :: Position -> () #

data Posd v Source #

A value with a source position associated.

Constructors

Posd 

Fields

Instances
Functor Posd Source # 
Instance details

Defined in What4.ProgramLoc

Methods

fmap :: (a -> b) -> Posd a -> Posd b #

(<$) :: a -> Posd b -> Posd a #

Foldable Posd Source # 
Instance details

Defined in What4.ProgramLoc

Methods

fold :: Monoid m => Posd m -> m #

foldMap :: Monoid m => (a -> m) -> Posd a -> m #

foldr :: (a -> b -> b) -> b -> Posd a -> b #

foldr' :: (a -> b -> b) -> b -> Posd a -> b #

foldl :: (b -> a -> b) -> b -> Posd a -> b #

foldl' :: (b -> a -> b) -> b -> Posd a -> b #

foldr1 :: (a -> a -> a) -> Posd a -> a #

foldl1 :: (a -> a -> a) -> Posd a -> a #

toList :: Posd a -> [a] #

null :: Posd a -> Bool #

length :: Posd a -> Int #

elem :: Eq a => a -> Posd a -> Bool #

maximum :: Ord a => Posd a -> a #

minimum :: Ord a => Posd a -> a #

sum :: Num a => Posd a -> a #

product :: Num a => Posd a -> a #

Traversable Posd Source # 
Instance details

Defined in What4.ProgramLoc

Methods

traverse :: Applicative f => (a -> f b) -> Posd a -> f (Posd b) #

sequenceA :: Applicative f => Posd (f a) -> f (Posd a) #

mapM :: Monad m => (a -> m b) -> Posd a -> m (Posd b) #

sequence :: Monad m => Posd (m a) -> m (Posd a) #

Eq v => Eq (Posd v) Source # 
Instance details

Defined in What4.ProgramLoc

Methods

(==) :: Posd v -> Posd v -> Bool #

(/=) :: Posd v -> Posd v -> Bool #

Show v => Show (Posd v) Source # 
Instance details

Defined in What4.ProgramLoc

Methods

showsPrec :: Int -> Posd v -> ShowS #

show :: Posd v -> String #

showList :: [Posd v] -> ShowS #

NFData v => NFData (Posd v) Source # 
Instance details

Defined in What4.ProgramLoc

Methods

rnf :: Posd v -> () #

data ProgramLoc Source #

A very small type that contains a function and PC identifier.

initializationLoc :: ProgramLoc Source #

Location for initialization code

Objects with a program location associated.