Index of values

Reverse function composition

Option monad bind

Reverse function application

Reverse function application and return its argument

Returns existential free variables in a canonical order

Return the name of an action

Raises Indpred_error if an error occurs

Removes duplicates and combines boxes

assq k l raises Not_found if there is no mapping for the key k in the list l

cform_star cf1 cf2 may return None if the result is inconsistent

Raises Indpred_error if an error occurs

Check VCs without doing action inference.

Check validity of program specifications.

Make a deep copy of a command (clear lvs and actions)

Make a deep copy of a command (preserve lvs and actions)

common p1 p2 = p such that p1 => p and p2 => p.

components_equal fld1 fld2 returns a conjuction of equalities for each component that is defined in both fld1 and fld2

Returns (globals, protocols, fun_specifications, resources, res_initializers, fun_proofs)

convert_assume_exp fun_ht e returns the statements required to evaluate assume e and assume (not e).

Convert a p_expression to a exp.

convert_exp_list_se fun_ht pel stmts returns the read side-effects required for the indirections in pel and a exp list representing pel

convert_exp_se fun_ht pe stmts returns the read side-effects required for the indirections in pe and a exp representing pe

Is arithmetic program generation enabled?

entails pl pl' returns true if pl |- EX exfv(pl'). pl'.

entails_exp pl e returns true if pl |- e.

entails_exp_aggr pl e returns true if pl |- e.

Generic constructor: create a new node for each disjunct

fv e s = IdSet.filter is_existential (fv(e)) ++ s

return true if exp of the form _x

Replace existentials with gensym'd existential vars.

Replace existentials with gensym'd normal vars.

findq l e x returns the first mapping of x in l; or the default_value e, if there is none.

fv e s = fv(e) ++ s

Return the non-existential free variables of an assertion

Return the list of equalities between set expressions in the pure formula.

Returns the set of expresssions that are not equal to e in pl

If this returns true then pure1.eq == pure2.eq.

The identity function

Executes RGSep action inference.

Check VCs without doing action inference.

insert_pure_code pure_code c copies c and insert pure_code before every atomic_block exit

interfere_once prover act cp calculate the effect of applying interference act to cp.

iter f s calls f on each statement in s

Return a weaker assertion that does not have any can_returns.

Kill the variables of cp that are not directly reachable from the set s

Return a weaker assertion that does not mention the killed variables.

Check that a linearizability specification contains no loops and return its effectful & pure execution paths

make_stable env cp rely returns a cp' such that cp |- cp' and stable_under cp rely

Assumes that variables affected by the substitution are not on LHS of assignments

mark_live_vars fv_post c updates c in place by marking its live variables at each program point.

Main entry point.

Create a new set of actions: new_acts name ctx pre post

Create a new set of actions: new_acts name pure ctx pre post

Create a new node

unsafe constructor

Pretty-print a pure assertion

Pretty print the generated integer program reachable from a node

Return the existential free variables of an assertion

Return the free variables of an assertion

Number of calls to the theorem prover during abstraction

Put an edge from n1 to n2

Put an edge from n1 to n2

Add action cp_ctx | cp ~~> cq to the guarantee.

Remove syntactically identical disjuncts (and add edges to the generated arithmetic program where necessary).

Find a simpler pl3 such that pl1 |- pl3 iff pl1 |- pl2.

Return the free variables of a spatial predicate

total number of iterations for all the calls to mk_stable_single

Compute eq such that ep |- eq and stable_under ep rely

unroll a node declaration in the lhs

unroll a node declaration in the rhs