language-boogie-0.2: Interpreter and language infrastructure for Boogie.

Safe HaskellNone



Execution state for the interpreter



data MapRepr Source

Representation of a map value


Source (Map [Value] Value)

Map that comes directly from a non-deterministic choice, possibly with some key-value pairs defined

Derived Ref (Map [Value] Value)

Map that is derived from another map by redefining values at some keys


emptyMap :: MapReprSource

Representation of an empty map

stored :: MapRepr -> Map [Value] ValueSource

Key-value pairs stored explicitly in a map representation

data Value Source

Run-time value


IntValue Integer

Integer value

BoolValue Bool

Boolean value

CustomValue Id Int

Value of a user-defined type

MapValue MapRepr

Value of a map type: consists of an optional reference to the base map (if derived from base by updating) and key-value pairs that override base

Reference Ref

Reference to a map stored in the heap


valueFromInteger :: Type -> Integer -> ValueSource

valueFromInteger t n: value of type t with an integer code n

flattenMap :: Heap Value -> Ref -> (Ref, Map [Value] Value)Source

Source reference and key-value pairs of a reference in a heap

mapSource :: Heap Value -> Ref -> RefSource

First component of flattenMap

mapValues :: Heap Value -> Ref -> Map [Value] ValueSource

Second component of flattenMap

refIdTypeName :: [Char]Source

Dummy user-defined type used to differentiate map values

ucTypeName :: [Char]Source

Dummy user-defined type used to mark entities whose definitions are currently being evaluated

deepDeref :: Heap Value -> Value -> ValueSource

deepDeref h v: Completely dereference value v given heap h (so that no references are left in v)

objectEq :: Heap Value -> Value -> Value -> Maybe BoolSource

objectEq h v1 v2: is v1 equal to v2 in the Boogie semantics? Nothing if cannot be determined.

valueDoc :: Value -> DocSource

Pretty-printed value

type Store = Map Id ValueSource

Store: stores variable values at runtime

emptyStore :: StoreSource

A store with no variables

functionConst :: [Char] -> [Char]Source

functionConst name : name of a map constant that corresponds function name (must be distinct from all global names)

userStore :: Heap Value -> Store -> StoreSource

userStore heap store : store with all reference values completely dereferenced given heap, and all auxiliary values removed

storeDoc :: Store -> DocSource

Pretty-printed store

data Memory Source

Memory: stores concrete values associated with names and references


type StoreLens = SimpleLens Memory StoreSource

Lens that selects a store from memory

emptyMemory :: MemorySource

Empty memory

visibleVariables :: Memory -> StoreSource

Visible values of all identifiers in a memory (locals shadow globals)

memoryDoc :: Bool -> Memory -> DocSource

memoryDoc debug mem : either user or debug representation of mem, depending on debug

data AbstractMemory Source

Abstract memory: stores constraints associated with names and references

data Environment m Source

Execution state

initEnv :: Context -> Generator m -> Maybe Integer -> Environment mSource

initEnv tc gen: Initial environment in a type context tc with a value generator gen