Index of values

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

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

generic function to add an assigns property.

generic function to add a WriteAny assigns property.

Add a new builtin.

Add a new builtin.

short cut to add a dynamic call

shortcut to add a call assigns property as an hypothesis.

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 a new library or update the dependencies of an existing one

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

shortcut to add a loop assigns property as an hypothesis.

add_node_annots cfg annots v (before, (after, exits)) add the annotations for the node :

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

generic function to add a predicate property after normalisation.

Add a postcondition of a called function.

Add the preconditions of the behavior : if impl_assumes, add b_assumes => b_requires else add both the b_requires and the b_assumes

Add the predicate as a function precondition.

Add all the b_requires.

Add the predicate as a stmt precondition.

Add the predicate as a stmt precondition.

Process the stmt spec precondition as an hypothesis for external properties.

new_script goal keys proof qed registers the script proof terminated by qed for goal goal and keywords keys

shortcut to add a stmt spec assigns property as an hypothesis.

Size of dimensions in the type (0 for unknown size)

Size of dimensions in the type (0 for unknown size)

append a list at the end of the current state

append a list in front of the current state

Returns the list of dimensions the array consists of.

Returns the list of dimensions the array consists of.

None if the po is trivial

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

equal chunks outside domain

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

equal chunks outside domain

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

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

Trims the original name

Trims the original name

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.

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

brackets_typ typ returns the numbre of brackets of the type typ.

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

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

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

Assumes the logic label only comes from normalized labels.

Assumes the logic label only comes from normalized labels.

Returns the type of pointers

Returns the type of pointers

Return the number of bindings of a map.

Return the number of bindings of a map.

Cast a memory location into another memory location.

Cast a memory location into another memory location.

Set up a context for the job.

Set up a context for the job.

Number of cells in the type (raise NoSize for unknown size)

Number of cells in the type (raise NoSize for unknown size)

returns true is this CFG is degenerated (no code available)

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

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

Clear the current value.

Clear the current value.

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 maps.

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

To force computation

Forces computation of dynamic calls.

To force computation

With free variables kept.

With free variables kept.

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

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

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

Create a new driver.

Creates a new context with name

Create a new driver.

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

Return the location of a C variable

Return the location of a C variable

for projectification

for projectification

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

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

no redefinition ; circularity protected

no redefinition ; circularity protected

The current value is defined.

The current value is defined.

Dimensions in the type (0 for non-array)

Dimensions in the type (0 for non-array)

Of external theories.

Of external theories.

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

dispatch_cvar v returns the var_kind associated to the C variable v according the current optimisations activated.

dispatch_lvar v returns the var_kind associated to the logic variable v according the current optimisations activated.

Give the set of chunk where an object of the given type at the given location is stored.

Give the set of chunk where an object of the given type at the given location is stored.

Print on output

Print on output

dump_scripts f saves all scripts from the database into file f.

e_range a b = b+1-a

e_range a b = b+1-a

Sorted

Sorted

node and edges relations

Emit a warning in current context.

Emit a warning in current context.

The empty map.

The empty map.

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

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

Is there some element satisfying the given predicate?

exists p m checks if at least one binding of the map satisfy the predicate p.

exists p m checks if at least one binding of the map satisfy the predicate p.

balance just give a default when link is not specified

balance just give a default when link is not specified

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

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

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

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

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

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

raises Not_found

raises Not_found

find a file in the includes of the current drivers

find a file in the includes of the current drivers

Retrieve script file for one specific goal.

Retrieve matchable script files for w.r.t provided required and hints keywords.

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

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

apply f_normal on the Normal postconditions, f_exits on the Exits postconditions, and warn on the others.

iterators

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

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

Performs the job with local context cleared.

Performs the job with local context cleared.

returns the list of XML elements from the given file.

Retrieves the current value of the context.

Returns empty list if there is no specified dynamic call.

Retrieves the current value of the context.

To be used as hypotheses arround a call, (the pre are in get_call_pre_goal)

similar to succ_e g v but gives the edge to VcallOut first and the edge to Vexit second.

Preconditions of a called function to be considered as hyp and goal (similar to get_both_hyp_goals).

Properties for assigns of kf

the bool in get_cut results says if the property has to be considered as a both goal and hyp (goal=true, or hyp only (goal=false)

Find the edges e that goes to the Vexit node inside the statement begining at node n

only filename, might not exists

only filename, might not exists

returns the given argument only if it is a valid function name (see Parameter_customize.get_c_ified_functions for more information), and abort otherwise.

Dynamically exported

Quite don't understand what is going on here...

Given an inductive phi{...A...}.

Given an inductive phi{...A...}.

Find the edges e of the statement node n postcondition and the set of edges that are inside the statement (e excluded).

only file name, might not exists

only file name, might not exists

only file name, might not exists

only file name, might not exists

Current model

Current model

return the values of option (group, name), return the empty list if not set

return the values of option (group, name), return the empty list if not set

always return the argument, even if the argument is not a function name.

What are the acceptable values for this parameter.

Find the edges where the postconditions of the node statement have to be checked.

Get the label to be used for the Post state of the node contract if any.

Find the edges where the precondition of the node statement have to be checked.

Dynamically exported

Unique identifier of prop_id

Unique identifier of prop_id

What is the possible range of values for this parameter.

Dynamically exported.

similar to succ_e g v but give the switch cases and the default edge

similar to succ_e g v but tests the branch to return (then-edge, else-edge)

get_time T t returns k such that T[k-1] <= t <= T[k], T is extended with T[-1]=0 and T[N]=+oo.

Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis.

Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis.

All POs related to a given property.

Handle the error and emit a warning with specified severity and effect if a context has been set.

Handle the error and emit a warning with specified severity and effect if a context has been set.

wether an exit edge exists or not

size in bits

size in bits

size in bytes

size in bytes

unique w.r.t equal

Return the formula that tests if two segment are included

Return the formula that tests if two segment are included

Increment the integer.

same information for all the provers

same information for all the provers

Reset the context to a newly created driver

Reset the context to a newly created driver

the (entire) variable has its initial value

the (entire) variable has its initial value

init_range env lv t_elt a b wp : put default values of type t_elt in lvk with a <= k < b

init_range env lv t_elt a b wp : put default values of type t_elt in lvk with a <= k < b

init_value env lv t v_opt wp: put value of type t (or default if None) in lv

init_value env lv t v_opt wp: put value of type t (or default if None) in lv

Cast a memory location into an integer of the given type

Cast a memory location into an integer of the given type

True if the variable is global, not extern, with a "const" qualifier type.

True if both options -const-readonly and -wp-init are positionned, and the variable is global, not extern, with a "const" type (see hasConstAttribute).

Raises Not_found if not.

Raises Not_found if not.

Remove the is_cint in formulas that are redondant with other conditions.

Remove the is_cint in formulas that are redondant with other conditions.

whether a proof needs several lemma to be complete

Test whether a map is empty or not.

Test whether a map is empty or not.

p ? 0 : 1

Whether the Chunk is local to a function.

Whether the Chunk is local to a function.

The function is the main entry point AND it is not a lib entry

Return the formula that check if a given location is null

Return the formula that check if a given location is null

wether all partial proofs have been accumulated or not

is_to_scope v returns true if v has to been scoped into the inner memory model : cvar of ref

p ? 1 : 0

Returns true if the clause is degenerated.

Returns true if the clause is degenerated.

is_user_formal_in_builtins lv tests if the address of the by-reference formal lv of user definition is an argument of (one or more) ACSL builtin predicate(s) or function : valid and family, separated, block_length, initialized

true if the result is valid.

iter f m applies f to all bindings in map m.

iter f m applies f to all bindings in map m.

Dynamically exported.

pairwise equal

pairwise equal

get the 'kind' information.

get the 'kind' information.

Short description of the kind of PO

Short description of the kind of PO

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

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

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

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

Memoized loading of drivers according to current WP options.

Load scripts from -wp-script f.

Compute the length in bytes between two memory locations

Compute the length in bytes between two memory locations

Memory location comparisons

Memory location comparisons

Cast a term representing a pointer to a c_object into a memory location

Cast a term representing a pointer to a c_object into a memory location

lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.

lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.

map f m returns a map with same domain as m, where the associated value a of all bindings of m has been replaced by the result of the application of f to a.

map f m returns a map with same domain as m, where the associated value a of all bindings of m has been replaced by the result of the application of f to a.

Same as Map.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.

Same as FCMap.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.

Same as Map.S.min_binding, but returns the largest binding of the given map.

Same as FCMap.S.min_binding, but returns the largest binding of the given map.

Same as , but returns the largest element of the given set.

Does the given element belong to the set?

mem x m returns true if m contains a binding for x, and false otherwise.

mem x m returns true if m contains a binding for x, and false otherwise.

memo tbl k f returns the binding of k in tbl.

with circularity protection

with circularity protection

merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.

merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.

Return the smallest binding of the given map (with respect to the Ord.compare ordering), or raise Not_found if the map is empty.

Return the smallest binding of the given map (with respect to the Ord.compare ordering), or raise Not_found if the map is empty.

Return the smallest element of the given set (with respect to the Ord.compare ordering), or raise Not_found if the set is empty.

\from property of function or statement behavior assigns.

\from property of function or statement behavior assigns.

mk_call_pre_id called_kf s_call called_pre

mk_call_pre_id called_kf s_call called_pre

complete behaviors property.

complete behaviors property.

disjoint behaviors property.

disjoint behaviors property.

Invariant establishment

Invariant establishment

function assigns

function assigns

\from property of function behavior assigns.

\from property of function behavior assigns.

Invariant used as hypothesis

Invariant used as hypothesis

axiom identification

axiom identification

create a virtual label to a statement (it can have no label)

create a virtual label to a statement (it can have no label)

\from property of loop assigns.

\from property of loop assigns.

mk_part pid (k, n) build the identification for the k/n part of pid.

mk_part pid (k, n) build the identification for the k/n part of pid.

Invariant preservation

Invariant preservation

Variant decrease

Variant decrease

Variant positive

Variant positive

name for elements in NATURAL

nearest_elt_ge v s returns the smallest element of s that is bigger or equal to v.

nearest_elt_le v s returns the largest element of s that is smaller or equal to v.

optionally init env with user logic variables

optionally init env with user logic variables