Index of values


A
accessOpToString [Ast.Expression]
add_pt [CfLazyModelChecker.Make_Lazy_Model_Checker]
addressOf [Ast.Expression]
Push all address operators to the variables.
allVarExps [Ast.Predicate]
allVarExps [Ast.Expression]
allVarExps_deep [Ast.Predicate]
alpha_convert [Ast.Predicate]
alpha_convert [Ast.Expression]
alpha_convert_lval [Ast.Expression]
assignOpToString [Ast.Expression]
assignments_of_expression [Ast.Expression]

B
binaryOpToString [Ast.Expression]
binaryOpToVanillaString [Ast.Expression]
build_proof_tree [CfLazyModelChecker.Make_Lazy_Model_Checker]

C
called_after [CfLazyModelChecker.Make_Lazy_Model_Checker]
canonicize [Ast.Predicate]
check_error [CfLazyModelChecker.Make_Lazy_Model_Checker]
clear_pts [CfLazyModelChecker.Make_Lazy_Model_Checker]
compare [Ast.Expression]
compare [Ast.Symbol]
conjoinL [Ast.Predicate]
constructEnvironmentAssumptions [Main]
constructInitialPredicates [Main]
constructInvariants [Main]
constructKillPredicates [Main]
convertDNF [Ast.Predicate]
Convert a boolean expression to DNF form.
count_tree_nodes [CfLazyModelChecker.Make_Lazy_Model_Checker]

D
deep_alpha_convert [Ast.Predicate]
substitute
deep_alpha_convert [Ast.Expression]
deep_alpha_convert f: lval -> expr where f: lval -> expr essentially f has the chlval information ...
demo_process [CfLazyModelChecker.Make_Lazy_Model_Checker]
derefedVar [Ast.Expression]
disjoinL [Ast.Predicate]
dump_trace_to_node [CfLazyModelChecker.Make_Lazy_Model_Checker]
dumppath [CfLazyModelChecker.Make_Lazy_Model_Checker]
dumptrace [CfLazyModelChecker.Make_Lazy_Model_Checker]

E
edge_to_op [CfLazyModelChecker.Make_Lazy_Model_Checker]
entry_pts_node [CfLazyModelChecker.Make_Lazy_Model_Checker]
exit_pts_node [CfLazyModelChecker.Make_Lazy_Model_Checker]
expand_path [CfLazyModelChecker.Make_Lazy_Model_Checker]
expand_path_with_old [CfLazyModelChecker.Make_Lazy_Model_Checker]
expand_summary_path [CfLazyModelChecker.Make_Lazy_Model_Checker]

F
fprintf [CfLazyModelChecker.Make_Lazy_Model_Checker]
fresh_lval [Ast.Expression]
returns a chlval that is essentially a "Fresh" version of that lval

G
getAtoms [Ast.Predicate]
getParents [Ast.Expression]
get_children [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_edge_op [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_entry [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_exit [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_global_var_phi [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_id [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_kind [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_marking [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_marking_data [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_node_data [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_op [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_outgoing [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_parent [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_parent_edge [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_pts [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_region [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_region_opt [CfLazyModelChecker.Make_Lazy_Model_Checker]
get_time_stamp [CfLazyModelChecker.Make_Lazy_Model_Checker]
global_lock_asm_table [CfLazyModelChecker.Make_Lazy_Model_Checker]
global_variable_table [CfLazyModelChecker.Make_Lazy_Model_Checker]

H
has_pt [CfLazyModelChecker.Make_Lazy_Model_Checker]

I
iff [Ast.Predicate]
implies [Ast.Predicate]
inputCustomAbs [Main]
interactive [Main]
isDeref [Ast.Expression]
isRelOp [Ast.Expression]
is_entry [CfLazyModelChecker.Make_Lazy_Model_Checker]
iter_global_variables [CfLazyModelChecker.Make_Lazy_Model_Checker]
iter_pts [CfLazyModelChecker.Make_Lazy_Model_Checker]

L
lvalToString [Ast.Expression]

M
main [Main]
map [Ast.Predicate]
map sym_f expr_f p ==> p' Return a predicate with the same structure, and sym_f applied to each bound* symbol at the place where it is bound, and expr_f applied to each expression.
max [CfLazyModelChecker.Make_Lazy_Model_Checker]
min [CfLazyModelChecker.Make_Lazy_Model_Checker]
modelCheck [Main]
model_check [CfLazyModelChecker.Make_Lazy_Model_Checker]

N
negate [Ast.Predicate]
negateAtom [Ast.Predicate]
negateRel [Ast.Expression]
nmap_add [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_choose [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_empty [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_filter [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_fold [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_isEmpty [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_iter [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_join [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_map [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_mem [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_remove [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_size [CfLazyModelChecker.Make_Lazy_Model_Checker]
nmap_to_list [CfLazyModelChecker.Make_Lazy_Model_Checker]
node_equal [CfLazyModelChecker.Make_Lazy_Model_Checker]
normalize [Ast.Predicate]
Various useful normalizations : e.g., And [...; False; ...] -> False etc
nset_add [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_choose [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_empty [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_filter [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_fold [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_iter [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_join [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_map [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_mem [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_remove [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_size [CfLazyModelChecker.Make_Lazy_Model_Checker]
nset_to_list [CfLazyModelChecker.Make_Lazy_Model_Checker]

P
parent_edge [CfLazyModelChecker.Make_Lazy_Model_Checker]
path_to_root [CfLazyModelChecker.Make_Lazy_Model_Checker]
print [Ast.Predicate]
print [Ast.Expression]
print [Ast.Symbol]
print_lval [Ast.Expression]
print_marking [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_marking_data [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_marking_short [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_node [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_node_data [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_option [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_phis [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_phis [LazyModelChecker.Make_Lazy_Model_Checker]
print_proof_tree [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_stats [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_stats [LazyModelChecker.Make_Lazy_Model_Checker]
print_summaries [CfLazyModelChecker.Make_Lazy_Model_Checker]
print_tree_node [CfLazyModelChecker.Make_Lazy_Model_Checker]
process_env_assumptions [CfLazyModelChecker.Make_Lazy_Model_Checker]
process_env_assumptions [LazyModelChecker.Make_Lazy_Model_Checker]
push_deref [Ast.Expression]

R
refine_path [CfLazyModelChecker.Make_Lazy_Model_Checker]
remove_pt [CfLazyModelChecker.Make_Lazy_Model_Checker]
replaceChlvals [Ast.Expression]
replace all occurrences of a Chlval by corresponding Lval
reset_stats [CfLazyModelChecker.Make_Lazy_Model_Checker]

S
single_child [CfLazyModelChecker.Make_Lazy_Model_Checker]
single_child_edge [CfLazyModelChecker.Make_Lazy_Model_Checker]
stats_nb_created_nodes [CfLazyModelChecker.Make_Lazy_Model_Checker]
stats_nb_deleted_nodes [CfLazyModelChecker.Make_Lazy_Model_Checker]
stats_nb_iterations [CfLazyModelChecker.Make_Lazy_Model_Checker]
stats_nb_iterations_of_outer_loop [CfLazyModelChecker.Make_Lazy_Model_Checker]
stats_nb_proof_tree_covered_nodes [CfLazyModelChecker.Make_Lazy_Model_Checker]
stats_nb_proof_tree_nodes [CfLazyModelChecker.Make_Lazy_Model_Checker]
stats_nb_refined_nodes [CfLazyModelChecker.Make_Lazy_Model_Checker]
stats_nb_refinment_processes [CfLazyModelChecker.Make_Lazy_Model_Checker]
substitute [Ast.Predicate]
substituteExpression [Ast.Expression]

T
testModelCheck [Main]
tlSafe [CfLazyModelChecker.Make_Lazy_Model_Checker]
toString [Ast.Predicate]
toString [Ast.Expression]
toString [Ast.Constant]
toString [Ast.Symbol]
to_dnf [Ast.Predicate]
tree_node_table [CfLazyModelChecker.Make_Lazy_Model_Checker]

U
unaryOpToString [Ast.Expression]
unaryOpToVanillaString [Ast.Expression]
a vanilla string is a string over the alphabet [a-zA-Z0-9] ; it is useful because the theorem provers/other backend tools dislike expressions like "|".
update_caller [CfLazyModelChecker.Make_Lazy_Model_Checker]
update_tree_after_refinment [CfLazyModelChecker.Make_Lazy_Model_Checker]

V
valOf [CfLazyModelChecker.Make_Lazy_Model_Checker]