Index of values

F.p_mul

F.p_mul

fold bind

fold bind

Lang.F.p_call

Wp.Lang.F.p_call

Lang.F.e_fun

Wp.Lang.F.e_fun

Lang.F.p_and

Wp.Lang.F.p_and

F.p_add

F.p_add

F.p_sub

F.p_sub

F.p_div

F.p_div

Lang.F.p_lt

Wp.Lang.F.p_lt

Lang.F.p_leq

Wp.Lang.F.p_leq

Lang.F.p_neq

Wp.Lang.F.p_neq

Lang.F.p_equal

Wp.Lang.F.p_equal

Lang.F.p_imply

Wp.Lang.F.p_imply

Lang.F.p_lt with inversed argument

Wp.Lang.F.p_lt with inversed argument

Lang.F.p_leq with inversed argument

Wp.Lang.F.p_leq with inversed argument

LabelMap.find with refined excpetion.

LabelMap.find with refined excpetion.

Same as Cfg.concat

Same as Cfg.concat

F.p_mod

F.p_mod

Lang.F.p_or

Wp.Lang.F.p_or

fun x -> p_sub 0 x

fun x -> p_sub 0 x

Constructor for { base ; offset }

Returns the base

Returns the offset in bytes from the logic offset (which is a memory cell index, actually)

Zero-offset base.

Null address.

Returns the offset

Shift: a_shift a k adds k to a.offset

add x s returns a set containing all elements of s, plus x.

add key data m returns a map containing the same bindings as m, plus a binding of key to data.

Add a new builtin.

Add a new builtin.

add_definitions sigma defs xs ps keep all definitions of variables xs from sigma that comes from defs.

Hooks are executed once at property creation

Hooks are executed once at property creation

add an invalid proof result ; can not revert a complete proof

add an invalid proof result ; can not revert a complete proof

Add a new library or update the dependencies of an existing one

Add a new library or update the dependencies of an existing one

add a value to an option (group, name)

add a value to an option (group, name)

accumulate in the proof the partial proof for this prop_id

accumulate in the proof the partial proof for this prop_id

Add the given elements to the set, in order.

Add the given bindings to the map, in order.

Equality used in the goal, simpler to prove than polymorphic equality

Set a node as temporary.

Set a node as temporary.

Must not be a builtin

Must not be a builtin

Extract the result obtained for the control point immediately after the given statement

Array lower-bound, ie `Some(0)`

Allocates new chunk for the validity of variables.

Allocates new chunk for the validity of variables.

freshen all variables

freshen all variables

Conjunction

Conjunction

append a list at the end of the current state

append a list in front of the current state

Propagate a sequent substitution inside the memory state.

Propagate a sequent substitution inside the memory state.

Relates two memory states corresponding to an assigns clause with the specified set of locations.

Relates two memory states corresponding to an assigns clause with the specified set of locations.

Computes equality

Computes equality

are_selected_names asked names checks if names of a property are selected according to asked names.

are_selected_names asked names checks if names of a property are selected according to asked names.

Returns the list of dimensions the array consists of.

Returns the list of dimensions the array consists of.

Extract the result as a table from control points to states

Make chunks equal outside of some domain.

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

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

Make chunks equal outside of some domain.

Computes the region assigned by an assigns clause.

Computes the region assigned by an assigns clause.

Computes the region assigned by a list of froms.

Computes the region assigned by a list of froms.

Computes the region assigned by a list of froms.

Computes the region assigned by a list of froms.

Represents execution traces T such that, if T contains every node points in the label-map, then the condition holds over the corresponding memory states.

Assumes a predicate in the specified section, with the specified decorations.

Represents execution traces T such that, if T contains every node points in the label-map, then the condition holds over the corresponding memory states.

Assumes a predicate in the specified section, with the specified decorations.

Array upper-bound, ie `Some(n-1)`

register a transformation applied just before close

register a transformation applied just before close

Extract the result at the entry point of the analysed function

Extract the result at the return point of the analysed function (just after the return transfer function)

Result that fits the default configuration

Result that fits the default configuration

base_addr v returns the value corresponding to the base address of v.

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

base_addr v returns the value corresponding to the base address of v.

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.

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

Trims the original name

Trims the original name

Used when generating fresh variables for a chunk.

Used when generating fresh variables for a chunk.

Extract the result obtained for the control point immediately before the given statement

bind sigma defs xs select definitions in defs targeting variables xs.

Performs the job with local context bound to local value.

Performs the job with local context bound to local value.

Return the list of all bindings of the given map.

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

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

domain, bounds included

domain, bounds included

Structurally corresponds to an if-then-else control-flow.

Construct a branch bundle, with merging of all common parts.

Structurally corresponds to an if-then-else control-flow.

Construct a branch bundle, with merging of all common parts.

build p => alpha(p) for functional dependencies verification.

build p => alpha(p) for functional dependencies verification.

Build the wto for the given automaton (No memoization, use get_wto instead)

Compute the index table from a wto

Closes the bundle and promote it into a well-formed sequence.

Closes the bundle and promote it into a well-formed sequence.

Returns the type of int

Returns the type of int

Returns the type of char

Returns the type of char

Conforms to

Conforms to

Conforms to

Conforms to

Returns the type of pointers

Returns the type of pointers

only for true verdicts

only for true verdicts

Create call data from the callee point of view, deriving data (gamma and pools) from the current frame.

Address of a function pointer.

Create call data from the callee point of view, deriving data (gamma and pools) from the current frame.

Address of a function pointer.

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state and post-state.

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state and post-state.

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state.

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state.

Compile a predicate call.

Compile a predicate call.

less than limit

Return the number of elements of a set.

Return the number of bindings of a map.

Cast a memory location into another memory location.

Applies a pointer cast or a conversion.

Applies a pointer cast or a conversion.

Cast a memory location into another memory location.

Set up a context for the job.

Set up a context for the job.

Value of size variables

Dimension environment

Type of matrix

Check assigns inclusion.

Check assigns inclusion.

Unless specified, default is false.

Unless specified, default is false.

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.

Make the union of each sigma, choosing the minimal variable in case of conflict.

Make the union of each sigma, choosing the minimal variable in case of conflict.

Return one element of the given set, or raise Not_found if the set is empty.

Return one binding of the given map, or raise Not_found if the map is empty.

Return one element of the given set, or None if the set is empty.

Return one binding of the given map, or None if the map is empty.

Clear the current value.

Clear the current value.

Interpret a value as a location.

Interpret a value as a location.

With free variables quantified.

With free variables quantified.

The cluster where all strings are defined.

The cluster where all strings are defined.

Unique

Unique

Run the provers with the command-line interface.

Run the provers with the command-line interface.

A total ordering function over the keys.

Total ordering between sets.

Total ordering between maps.

same as Ctypes.compare but all PTR are considered the same

same as Wp.Ctypes.compare but all PTR are considered the same

with circularity protection

with circularity protection

Unless specified, default is Empty selection.

Unless specified, default is Empty selection.

To force computation

Forces computation of dynamic calls.

To force computation

Full Compilation

Full Compilation

The concatenation is the intersection of all possible collection of traces from each cfg.

List conjunction

The concatenation is the intersection of all possible collection of traces from each cfg.

List conjunction

Evaluate the conditional expression on the given memory state.

Evaluate the conditional expression on the given memory state.

Apply process, but only after proving some condition

With free variables kept.

Apply process, but only after proving some condition

With free variables kept.

Initializers to be run before using the model.

Apply global configure hooks, once per project/ast.

Initializers to be run before using the model.

Apply global configure hooks, once per project/ast.

Given an automaton, return a vertex's binder.

Given an automaton, return a vertex's binder.

Context used by pp_term, pp_pred, pp_var, ppvars for printing the term.

Context used by pp_term, pp_pred, pp_var, ppvars for printing the term.

Independent from model

Independent from model

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

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

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

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

Duplicate the environment.

Duplicate the environment.

Deep copy: no possible sharing between x and copy x.

Bundle an equation with the sigma sequence that created it

Bundle a term with the sigma sequence that created it.

Bundle an equation with the sigma sequence that created it.

Bundle an equation with the sigma sequence that created it.

Initially empty environment.

Creates a new context with name

Bundle an equation with the sigma sequence that created it

Bundle a term with the sigma sequence that created it.

Bundle an equation with the sigma sequence that created it.

Bundle an equation with the sigma sequence that created it.

Initially empty environment.

Creates a new context with name

add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name

add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name

to be used only once for one of the related prop_id

to be used only once for one of the related prop_id

Current parameters

The current memory state.

Current parameters

The current memory state.

Evaluate an abstract value.

Evaluate an abstract value.

cvar x returns the abstract value corresponding to &x.

Return the location of a C variable.

cvar x returns the abstract value corresponding to &x.

Return the location of a C variable.

For projectification.

For projectification.

Return true if and only the term is e_true.

Return true if and only the term is e_true.

"Var,Typed,Nat,Real" memory model.

all None

all None

"Var,Typed,Nat,Real" memory model.

no redefinition ; circularity protected

no redefinition ; circularity protected

The current value is defined.

The current value is defined.

Of external theories.

Of external theories.

Set difference: diff s1 s2 contains the elements of s1 that are not in s2.

Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells

Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells

Current model in "-wp-out" directory

Current model in "-wp-out" directory

Test if two sets are disjoint.

domain v returns a list of all possible concrete bases of v.

Memory footprint of a region.

Footprint of a memory environment.

Compute the set of chunks that hold the value of an object with the given C-type.

Assumes a list of predicates in a Type section on top of the bundle.

domain v returns a list of all possible concrete bases of v.

Assumes a list of predicates in a Type section on top of the bundle.

Memory footprint of a region.

Compute the set of chunks that hold the value of an object with the given C-type.

Footprint of a memory environment.

Properties that are False-if-unreachable in case the PO is valid.

Properties that are False-if-unreachable in case the PO is valid.

Dependent on model

Dependent on model

Print on output

Print on output

Closes all specified binders

Closes all specified binders

Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default).

Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default).

e_range a b = b+1-a

e_range a b = b+1-a

uses current pool

uses current pool

Sorted

Sorted

Represents all execution trace T such that, if T contains node a, then T also contains b with the given effect on corresponding memory states.

Represents all execution trace T such that, if T contains node a, then T also contains b with the given effect on corresponding memory states.

Structurally corresponds to an arbitrary choice among the different possible executions.

Construct a disjunction bundle, with merging of all common parts.

Structurally corresponds to an arbitrary choice among the different possible executions.

Construct a disjunction bundle, with merging of all common parts.

Return the list of all elements of the given set.

Emit a warning in current context.

Emit a warning in current context.

Same as Chunk.Set.empty

empty sequence, equivalent to true assumption

empty sequence, equivalent to true assumption

Same as Chunk.Set.empty

The empty set.

The empty map.

Returns a new environment where the current memory state is moved to to the corresponding label.

Returns a new environment where the current memory state is moved to to the corresponding label.

Same as ==

Same as ==

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

equal cmp m1 m2 tests whether the maps m1 and m2 are equal, that is, contain equal keys and associate them with equal data.

Same as equal_typ with an object type.

Same as equal_typ with an object type.

Computes the value of (a==b) provided both a and b are values with the given type.

Computes the value of (a==b) provided both a and b are values with the given type.

Same as are_equal is Yes

Same as are_equal is Yes

Same as e_leq is e_true

Same as e_leq is e_true

Same as e_lt is e_true

Same as e_lt is e_true

Same as are_equal is No

Same as are_equal is No

Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.

Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.

exists f s checks if at least one element of the set satisfies the predicate f.

exists f m checks if at least one binding of the map satisfies the predicate f.

Is there some element satisfying the given predicate?

Extract an exit strategy from a component, i.e.

Extract an exit strategy from a component, i.e.

Evaluate the expression on the given memory state.

Evaluate the expression on the given memory state.

Register and returns the tactical

Register and returns the tactical

balance just give a default when link is not specified

balance just give a default when link is not specified

Computes a formulae equivalent to the bundle.

Computes a formulae equivalent to the bundle.

Physical address

All bit-test functions

size in bits

All bit-test functions

size in bits

All except f_bit_positive

All except f_bit_positive

size in bytes

size in bytes

Physical address

memoized, not-projectified

memoized, not-projectified

field v fd returns the value obtained by access to field fd from v.

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

field v fd returns the value obtained by access to field fd from v.

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

filter f s returns the set of all elements in s that satisfy predicate f.

filter f m returns the map with all the bindings in m that satisfy predicate p.

filter_map f s returns the set of all v such that f x = Some v for some element x of s.

filter_map f m applies the function f to every binding of m, and builds a map from the results.

find x s returns the element of s equal to x (according to Ord.compare), or raise Not_found if no such element exists.

find x m returns the current value of x in m, or raises Not_found if no binding for x exists.

Search a given key in the map.

find_first f s, where f is a monotonically increasing function, returns the lowest element e of s such that f e, or raises Not_found if no such element exists.

find_first f m, where f is a monotonically increasing function, returns the binding of m with the lowest key k such that f k, or raises Not_found if no such key exists.

find_first_opt f s, where f is a monotonically increasing function, returns an option containing the lowest element e of s such that f e, or None if no such element exists.

find_first_opt f m, where f is a monotonically increasing function, returns an option containing the binding of m with the lowest key k such that f k, or None if no such key exists.

find_last f s, where f is a monotonically decreasing function, returns the highest element e of s such that f e, or raises Not_found if no such element exists.

find_last f m, where f is a monotonically decreasing function, returns the binding of m with the highest key k such that f k, or raises Not_found if no such key exists.

find_last_opt f s, where f is a monotonically decreasing function, returns an option containing the highest element e of s such that f e, or None if no such element exists.

find_last_opt f m, where f is a monotonically decreasing function, returns an option containing the binding of m with the highest key k such that f k, or None if no such key exists.

find a file in the includes of the current drivers

find a file in the includes of the current drivers

find_opt x s returns the element of s equal to x (according to Ord.compare), or None if no such element exists.

find_opt x m returns Some v if the current value of x in m is v, or None if no binding for x exists.

Returns a string literal in decimal notation (without suffix) that reparses to the same value (when added suffix).

Returns a string literal in decimal notation (without suffix) that reparses to the same value (when added suffix).

type of floats

type of floats

fold f s init computes (f xN ... (f x2 (f x1 init))...), where x1 ... xN are the elements of s, in increasing order.

fold f m init computes (f kN dN ... (f k1 d1 init)...), where k1 ... kN are the keys of all bindings in m (in increasing order), and d1 ... dN are the associated data.

for_all f s checks if all elements of the set satisfy the predicate f.

for_all f m checks if all the bindings of the map satisfy the predicate f.

Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively.

Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively.

Make a fresh frame with the given function.

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

Make a fresh frame with the given function.

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

Performs the job with local context cleared.

Performs the job with local context cleared.