A | |
| a_expression [Parsetree] |
without the impure cases
|
| a_invariant [Parsetree] | |
| a_proposition [Parsetree] | |
| abs_options [Abstraction] | |
| abstraction [Genarith] |
Interface provided by the abstraction module:
uform_abs is the analogue of prop_abs for formulas with no boxes.
See below.
The boolean argument tells whether the abstraction should be aggressive
(disregard sentinel values).
, uform_join is the analogue of prop_join for formulas with no boxes.
See below.
, prop_abs cp returns a cp' belonging to a smaller domain such that
cp |- cp'
, prop_join cp1a cp1b cp2 assumes that cp1a <==> cp1b and returns
(cpa,cpb,cp2') such that cpa <==> cpb
and cp1a |- cpa and cp2' |- cpa
and (cp1b \/ cp2) ==> cpb
and cpb ==> (cp1b \/ cp2')
, set_abs returns a substitution that abstracts set values in the assertion
, list_abs returns a substitution that abstract list values in the assertion
|
| act [Assertions] |
Type of RGSep actions used for interference calculations
|
| actual_params [Parsetree] | |
C | |
| can_cmd [Commands] |
Canonical command: sequence of statements
|
| can_entailment [Commands] |
Canonical entailments
|
| can_goto [Commands] |
Kind of branches
|
| can_isemp [Assertions] | |
| can_spatial [Assertions] |
Star-conjunction of heap predicates
|
| can_spred [Assertions] |
Canonical heap predicate.
|
| can_st_desc [Commands] |
Statement descriptor
|
| can_stmt [Commands] |
Canonical statement
|
| cas_memory_order [Commands] | |
| cform [Assertions] |
Canonical formulas with boxes
|
| component [Misc] | |
| cprop [Assertions] |
Canonical proposition: disjunction of canonical formulas
|
D | |
| dlink_kind [Parsetree] | |
E | |
| eform [Genarith] | |
| eprop [Genarith] | |
| escrow_item [Tycheck] | |
| exp [Exp] |
Canonical expressions
|
F | |
| fld_assignments [Commands] |
Field assignments
|
| fun_info [Commands] |
Information about function declarations
|
| fun_info_ht [Convert] | |
G | |
| ga_node [Genarith] |
Nodes
|
| global_env [Symbsimp] | |
| guar_env [Actions] | |
I | |
| id_internal1 [Exp] | |
| id_internal2 [Exp] | |
| id_internal3 [Exp] | |
| idpool [Exp] | |
| ie_list [Exp] | |
| ip_decl [Indpreds] |
Internal representation of inductive predicates
|
L | |
| link_kind [Assertions] |
Kind of link for linked lists
|
M | |
| myaction [Actions] |
action name, context pure, context spatial, action pre, action post
|
P | |
| p_action [Parsetree] | |
| p_cas_memory_order [Parsetree] | |
| p_expression [Parsetree] | |
| p_expression_desc [Parsetree] | |
| p_item [Parsetree] | |
| p_program [Parsetree] | |
| p_protocol_state [Parsetree] | |
| p_read_memory_order [Parsetree] | |
| p_state_after [Parsetree] | |
| p_statement [Parsetree] | |
| p_statement_desc [Parsetree] | |
| p_type [Parsetree] | |
| p_vars [Parsetree] | |
| p_write_memory_order [Parsetree] | |
| plist [Misc] | |
| protocol_item [Tycheck] | |
| protocol_state [Tycheck] | |
| prover [Assertions] |
Interface provided by the theorem provers:
find_ptsto and expose_ptsto: used by symbolic execution, but should
be removed.
, nf_cprop sl_context eq cp = cp' where cp' is a normal form
of cp.
, nf_cform cf returns cprop_false if cf is inconsistent,
or cp' such that cf <==> cp' and
nf_cprop [] empty_eq cp' = cp'
, entails_cprop cp cp' returns inst if cp * inst |- cp'
, find_frame_cprop fr cp1 cp2 returns res such that cp1 |- cp2 * res
in context fr
(i.e. for all R, (fr /\ R) * cp1 |- (fr /\ R) * cp2 * res)
or raises No_frame_found
|
| pstate [Assertions] | |
R | |
| read_memory_order [Commands] |
Kind of memory orders
|
| res_init [Commands] |
Resource initialization
|
S | |
| sfn [Exp] |
Built-in functions with a variable number of arguments
|
| sfn1 [Exp] |
Built-in functions with one argument
|
| sfn2 [Exp] |
Built-in functions with two arguments
|
| sfn_grp [Exp] | |
| stab_env [Actions] | |
| state_predecessor [Tycheck] | |
| subst [Exp] |
Substitutions
|
T | |
| t [Pure] |
The type of non-disjunctive pure formulae
|
| t [Location] | |
| t [Exp.Fld] |
Finite map from components to expressions
|
| t [Exp.Dset] | |
| t [Exp.Id] | |
| tag [Assertions] |
Tags for spatial predicates.
|
| tag2 [Assertions] | |
U | |
| udom [Genarith] |
Abstract domain corresponding to a disjunction of
uforms for
calculating fix-points.
|
| uform [Assertions] |
Canonical formulas without boxes
|
W | |
| write_memory_order [Commands] |