Index of values

Log complexity.

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

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.

Add a new binding.

add x y requires x >= y

add0 x d requires x >= d

add x f y requires x >= f(y)

add x f y z requires x >= f(y,z)

generic function to add an assigns property.

generic function to add a WriteAny assigns property.

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.

Add an hook which is applied each time (just before) the project library changes the local value of the state.

store the node as an irreducible loop header.

External theories

shortcut to add a loop assigns property as an hypothesis.

store the node as a loop header.

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

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.

store the edge between the two nodes (n1, n2) as a reentry edge.

new_script goal keys proof registers the script proof for goal goal and keywords keys

we want to prove this behavior: add the requires as preconditions to both prove and use as hyp,, add the assumes as hypotheses,, add the postconditions as goals.

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

Add the post condition of the whole spec as hypothesis.

add x f ys requires x >= f(ys)

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

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 the memory location of the base address of a given memory location

call the construction of the directory only once

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.

Return the list of all bindings of the given map.

Return the list of all bindings of the given map.

Same as Bytes.blit_string.

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.

Returns the type of int

Returns the type of char

Conforms to

Conforms to

Assumes the logic label only comes from normalized labels.

Returns the type of pointers

Return a copy of the argument, with the first character set to uppercase.

Return the number of elements of a set.

Return the number of bindings of a map.

Return the number of bindings of a map.

Cast a memory location into another memory location.

Set up a context for the job.

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

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

build the nodes for the stmts, connect the last one with next, and return the node of the first stmt.

If needed, clear wp table to compute Pass2.

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 binding of the given map, or raise Not_found if the map is empty.

Clear the current value.

Clear the table.

Reset the reference to its default value.

The cluster where all strings are defined.

Unique

Total ordering between sets.

Total ordering between maps.

Total ordering between maps.

The comparison function for strings, with the same specification as Pervasives.compare.

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

List of names of all kernel compilation units.

with circularity protection

To force computation

Forces computation of dynamic calls.

String.concat sep sl concatenates the list of strings sl, inserting the separator string sep between each.

String.contains s c tests if character c appears in the string s.

String.contains_from s start c tests if character c appears in s after position start.

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

Return a copy of the given string.

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

Duplicates A into B with the provided morphism.

Creates a new context with name

String.create n returns a fresh byte sequence of length n.

Graph A should be static : further nodes in A can not be indexed.

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

Directory where architecture independent files are.

for projectification

Compilation date.

2 Create a session

no redefinition ; circularity protected

The current value is defined.

Dimensions in the type (0 for non-array)

Of external theories.

Set difference.

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

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.

Before storing something at a program point, we have to process the label at that point.

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

Dump the graph into provided file.

Dot command name.

Print on output

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

e_range a b = b+1-a

node and edges relations

Return the list of all elements of the given set.

Emit a warning in current context.

The empty set.

The empty map.

The empty map.

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.

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

Return a copy of the argument, with special characters represented by escape sequences, following the lexical conventions of OCaml.

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

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

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

String.fill s start len c modifies byte sequence s in place, replacing len bytes with c, starting at start.

Linear.

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

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

Return the current binding of the given key.

Return the list of all data associated with the given key.

empty bhv_names means all (whatever ki is)

raises Not_found

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.

Computes the least fixpoint solution satifying all added requirements.

Iterate over a weak partial order.

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

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

apply the function on the node successors

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

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.

returns the list of XML elements from the given file.

raises Not_found.

Retrieves the current value of the context.

Returns empty list if there is no specified dynamic call.

String.get s n returns the character at index n in string s.

Get the referenced value.

Returns default if not found.

Select in bhv_list the behavior that has to be processed according to config and ki current statement.

Builds tables that give hypotheses and goals relative to b behavior for edges of the cfg to consider during wp computation.

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

Dynamically exported

get the node innermost loop header if any

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

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

Returns the annotations for the three edges of the loop node: loop_entry : goals for the edge entering in the loop, loop_back : goals for the edge looping to the entry point, loop_core : fix-point hypothesis for the edge starting the loop core

find the outer loop in which the stmt is.

Current model

find the behavior named name in the list

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

get the previously stored position of the node or 0 if nothing has been stored

get the previously stored position of the node if any, or None if set_pos hasn't been called already for this node.

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.

returns a unique name identifying the property.

Dynamically exported

Unique identifier of prop_id

Dynamically exported.

In some cases (goto for instance) we have to create a node before having processed if through cfg_stmt.

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

Get the edges going out a test node with the then branch first

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.

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.

wether an exit edge exists or not

howto_marshal marshal unmarshal registers a custom couple of functions (marshal, unmarshal) to be used for serialization.

size in bits

size in bytes