what4-1.5.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2014-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.ProgramLoc

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

Instances details
Show Position Source # 
Instance details

Defined in What4.ProgramLoc

NFData Position Source # 
Instance details

Defined in What4.ProgramLoc

Methods

rnf :: Position -> () #

Eq Position Source # 
Instance details

Defined in What4.ProgramLoc

Ord Position Source # 
Instance details

Defined in What4.ProgramLoc

Pretty Position Source # 
Instance details

Defined in What4.ProgramLoc

Methods

pretty :: Position -> Doc ann #

prettyList :: [Position] -> Doc ann #

data Posd v Source #

A value with a source position associated.

Constructors

Posd 

Fields

Instances

Instances details
Foldable Posd Source # 
Instance details

Defined in What4.ProgramLoc

Methods

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

foldMap :: Monoid m => (a -> m) -> Posd a -> 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) #

Functor Posd Source # 
Instance details

Defined in What4.ProgramLoc

Methods

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

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

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 -> () #

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

Defined in What4.ProgramLoc

Methods

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

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

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.