Initializers to be run before using the model. Typically push Context values and returns a function to rollback.

Given an automaton, return a vertex's binder. Currently used by the automata compiler to bind current vertex. See StmtSemantics.

For projectification. Must be unique among models.

Computes the memory model partitionning of the memory locations. This function typically adds new elements to the partition received in input (that can be empty).

Memory model chunks.

Chunks Sets and Maps.

Model Environments.

Representation of the memory location in the model.

Internal (private) memory state description for later reversing the model.

Returns a memory state description from a memory environement.

Try to interpret a term as an in-memory operation located at this program point. Only best-effort shall be performed, otherwise return Mvalue.

Recognized Cil patterns:

• Mvar x,[Mindex 0] is rendered as *x when x has a pointer type
• Mmem p,[Mfield f;...] is rendered as p->f... like in Cil
• Mmem p,[Mindex k;...] is rendered as p[k]... to catch Cil Mem(AddPI(p,k)),...

Try to interpret a sequence of states into updates.

The result shall be exhaustive with respect to values that are printed as Sigs.mval values at post label via the lookup function. Otherwise, those values would not be pretty-printed to the user.

Propagate a sequent substitution inside the memory state.

Debug

pretty printing of memory location

Return the logic variables from which the given location depend on.

Test if a location depend on a given logic variable

Return the location of the null pointer

Return the memory location of a constant string, the id is a unique identifier.

Return the location of a C variable.

Interpret an address value (a pointer) as an abstract location. Might fail on memory models not supporting pointers.

Return the adress value (a pointer) of an abstract location. Might fail on memory models not capable of representing pointers.

Return the memory location obtained by field access from a given memory location.

Return the memory location obtained by array access at an index represented by the given term. The element of the array are of the given c_object type.

Return the memory location of the base address of a given memory location.

Return the offset of the location, in bytes, from its base_addr.

Returns the length (in bytes) of the allocated block containing the given location.

Cast a memory location into another memory location. For cast ty loc the cast is done from ty.pre to ty.post. Might fail on memory models not supporting pointer casts.

Cast a term representing an absolute memory address (to some c_object) given as an integer, into an abstract memory location.

Cast a memory location into its absolute memory address, given as an integer with the given C-type.

Compute the set of chunks that hold the value of an object with the given C-type. It is safe to retun an over-approximation of the chunks involved.

Provides the constraint corresponding to the kind of data stored by all chunks in sigma.

Return the value of the object of the given type at the given location in the given memory state.

Return the initialization status at the given location in the given memory state.

Return a set of equations that express a copy between two memory state.

copied sigma ty loc1 loc2 returns a set of formula expressing that the content for an object ty is the same in sigma.pre at loc1 and in sigma.post at loc2.

Return a set of equations that express a copy of an initialized state between two memory state.

copied sigma ty loc1 loc2 returns a set of formula expressing that the initialization status for an object ty is the same in sigma.pre at loc1 and in sigma.post at loc2.

Return a set of formula that express a modification between two memory state.

stored sigma ty loc t returns a set of formula expressing that sigma.pre and sigma.post are identical except for an object ty at location loc which is represented by t in sigma.post.

Return a set of formula that express a modification of the initialization status between two memory state.

stored_init sigma ty loc t returns a set of formula expressing that sigma.pre and sigma.post are identical except for an object ty at location loc which has a new init represented by t in sigma.post.

Return a set of formula that express that two memory state are the same except at the given set of memory location.

This function can over-approximate the set of given memory location (e.g it can return true as if the all set of memory location was given).

Return the formula that check if a given location is null

Memory location comparisons

Compute the length in bytes between two memory locations

Return the formula that tests if a memory state is valid (according to acs) in the given memory state at the given segment.

Assert the memory is a proper heap state preceeding the function entry point.

Allocates new chunk for the validity of variables.

Return the formula that tests if a memory state is initialized (according to acs) in the given memory state at the given segment.

Returns the formula that tests if the entire memory is invalid for write access.

Manage the scope of variables. Returns the updated memory model and hypotheses modeling the new validity-scope of the variables.

Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis. This means separated from the formals and locals of the function.

Return the formula that tests if two segment are included

Return the formula that tests if two segment are separated