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

Copyright | (c) Galois Inc 2014-2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
Stability | provisional
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.ProgramLoc

Contents

- Objects with a program location associated.

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

- data Position
  - = SourcePos !Text !Int !Int
  - | BinaryPos !Text !Word64
  - | OtherPos !Text
  - | InternalPos
- sourcePos :: FilePath -> Int -> Int -> Position
- startOfFile :: FilePath -> Position
- ppNoFileName :: Position -> Doc ann
- data Posd v = Posd {
  - pos :: !Position
  - pos_val :: !v
  }
- data ProgramLoc
- mkProgramLoc :: FunctionName -> Position -> ProgramLoc
- initializationLoc :: ProgramLoc
- plFunction :: ProgramLoc -> FunctionName
- plSourceLoc :: ProgramLoc -> Position
- class HasProgramLoc v where
  - programLoc :: Lens' v ProgramLoc

# 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 Methods showsPrec :: Int -> Position -> ShowS Source # show :: Position -> String Source # showList :: [Position] -> ShowS Source #
NFData Position Source # |
Instance details Defined in What4.ProgramLoc Methods rnf :: Position -> () Source #
Eq Position Source # |
Instance details Defined in What4.ProgramLoc Methods (==) :: Position -> Position -> Bool Source # (/=) :: Position -> Position -> Bool Source #
Ord Position Source # |
Instance details Defined in What4.ProgramLoc Methods compare :: Position -> Position -> Ordering Source # (<) :: Position -> Position -> Bool Source # (<=) :: Position -> Position -> Bool Source # (>) :: Position -> Position -> Bool Source # (>=) :: Position -> Position -> Bool Source # max :: Position -> Position -> Position Source # min :: Position -> Position -> Position Source #
Pretty Position Source # |
Instance details Defined in What4.ProgramLoc Methods pretty :: Position -> Doc ann Source # prettyList :: [Position] -> Doc ann Source #

sourcePos :: FilePath -> Int -> Int -> Position Source #

startOfFile :: FilePath -> Position Source #

ppNoFileName :: Position -> Doc ann Source #

data Posd v Source #

A value with a source position associated.

Constructors

Posd |

Fields

- pos :: !Position
- pos_val :: !v

#### Instances

Instances details

Foldable Posd Source # |

Instance details

Defined in What4.ProgramLoc

Methods

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

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

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

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

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

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

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

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

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

toList :: Posd a -> [a] Source #

null :: Posd a -> Bool Source #

length :: Posd a -> Int Source #

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

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

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

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

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

Traversable Posd Source # |
Instance details Defined in What4.ProgramLoc Methods traverse :: Applicative f => (a -> f b) -> Posd a -> f (Posd b) Source # sequenceA :: Applicative f => Posd (f a) -> f (Posd a) Source # mapM :: Monad m => (a -> m b) -> Posd a -> m (Posd b) Source # sequence :: Monad m => Posd (m a) -> m (Posd a) Source #
Functor Posd Source # |
Instance details Defined in What4.ProgramLoc Methods fmap :: (a -> b) -> Posd a -> Posd b Source # (<$) :: a -> Posd b -> Posd a Source #
Show v => Show (Posd v) Source # |
Instance details Defined in What4.ProgramLoc Methods showsPrec :: Int -> Posd v -> ShowS Source # show :: Posd v -> String Source # showList :: [Posd v] -> ShowS Source #
NFData v => NFData (Posd v) Source # |
Instance details Defined in What4.ProgramLoc Methods rnf :: Posd v -> () Source #
Eq v => Eq (Posd v) Source # |
Instance details Defined in What4.ProgramLoc Methods (==) :: Posd v -> Posd v -> Bool Source # (/=) :: Posd v -> Posd v -> Bool Source #

data ProgramLoc Source #

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

#### Instances

Instances details

Show ProgramLoc Source # |
Instance details Defined in What4.ProgramLoc Methods showsPrec :: Int -> ProgramLoc -> ShowS Source # show :: ProgramLoc -> String Source # showList :: [ProgramLoc] -> ShowS Source #
Eq ProgramLoc Source # |
Instance details Defined in What4.ProgramLoc Methods (==) :: ProgramLoc -> ProgramLoc -> Bool Source # (/=) :: ProgramLoc -> ProgramLoc -> Bool Source #
Ord ProgramLoc Source # |

Instance details

Defined in What4.ProgramLoc

Methods

compare :: ProgramLoc -> ProgramLoc -> Ordering Source #

(<) :: ProgramLoc -> ProgramLoc -> Bool Source #

(<=) :: ProgramLoc -> ProgramLoc -> Bool Source #

(>) :: ProgramLoc -> ProgramLoc -> Bool Source #

(>=) :: ProgramLoc -> ProgramLoc -> Bool Source #

max :: ProgramLoc -> ProgramLoc -> ProgramLoc Source #

min :: ProgramLoc -> ProgramLoc -> ProgramLoc Source #

mkProgramLoc :: FunctionName -> Position -> ProgramLoc Source #

Make a program loc

initializationLoc :: ProgramLoc Source #

Location for initialization code

plFunction :: ProgramLoc -> FunctionName Source #

plSourceLoc :: ProgramLoc -> Position Source #

# Objects with a program location associated.

class HasProgramLoc v where Source #

Methods

programLoc :: Lens' v ProgramLoc Source #