cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
Here is a list of all variables with links to the classes they belong to:
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
- l -
l :
arrayst::array_equalityt
,
boolbvt::quantifiert
,
literalt
l1_indices :
path_storaget
l1_types :
goto_symex_statet
l2_indices :
path_storaget
label :
build_declaration_hops_inputst
,
mini_bdd_mgrt::var_table_entryt
label_instruction :
build_declaration_hops_inputst
label_references :
statement_list_typecheckt
label_scope_index :
build_declaration_hops_inputst
labels :
goto_convertt::targetst
,
goto_programt::instructiont
labels_defined :
c_typecheck_baset
labels_in_use :
goto_program2codet
labels_used :
c_typecheck_baset
lambda_method_handle_map :
java_bytecode_parse_treet::classt
language :
language_filet
language_files :
lazy_goto_functions_mapt
,
lazy_goto_modelt
language_mode :
dfcc_contract_functionst
,
field_sensitivityt
,
goto_symex_statet
,
goto_symext
,
simplify_expr_with_value_sett
,
symex_assignt
,
value_set_dereferencet
language_options :
java_bytecode_languaget
last_declarator :
ansi_c_scopet
last_line :
parsert
last_path :
all_paths_enumeratort
last_peeked :
path_lifot
last_source_location :
container_encoding_targett
,
symex_bmct
last_write_context :
vsd_configt
last_written_locations :
write_location_contextt
latch :
dfcc_loop_nesting_graph_nodet
lazy :
arrayst::lazy_constraintt
lazy_array_constraints :
arrayst
lazy_arrays :
arrayst
lazy_method_map :
language_filest
lazy_methods_extra_entry_points :
ci_lazy_methodst
lazy_methods_mode :
java_bytecode_language_optionst
lb :
__CPROVER_contracts_car_t
,
boundst
lcnf_bv :
propt
le_set :
invariant_sett
leaf :
java_bytecode_convert_methodt::block_tree_nodet
leaf_exprs :
leaf_enumeratort
leave_set :
goto_convertt::leave_targett
,
goto_convertt::targetst
leave_stack_node :
goto_convertt::leave_targett
,
goto_convertt::targetst
leave_target :
goto_convertt::leave_targett
,
goto_convertt::targetst
left :
left_and_right_valuest
left_depth_below_common_ancestor :
ancestry_resultt
len :
string_ptrt
length :
java_bytecode_convert_methodt::holet
,
java_bytecode_convert_methodt::variablet
,
java_bytecode_parse_treet::methodt::local_variablet
length_modifier :
format_tokent
length_of_array :
array_poolt
let_id_count :
letifyt
let_symbol :
letifyt::let_count_idt
letify :
smt2_convt
level :
api_messaget
level1 :
goto_symex_statet
level2 :
goto_statet
levels :
sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >
lex :
Parser
lhs :
assignmentt
,
framet::implicationt
,
left_and_right_valuest
lib :
configt::ansi_ct
libraries :
compilet
library :
dfcc_contract_clauses_codegent
,
dfcc_contract_functionst
,
dfcc_contract_handlert
,
dfcc_instrument_loopt
,
dfcc_instrumentt
,
dfcc_is_freeablet
,
dfcc_is_fresht
,
dfcc_lift_memory_predicatest
,
dfcc_obeys_contractt
,
dfcc_pointer_equalst
,
dfcc_pointer_in_ranget
,
dfcc_spec_functionst
,
dfcc_swap_and_wrapt
,
dfcc_wrapper_programt
,
dfcct
library_paths :
compilet
lifetime :
goto_convertt
,
symbol_factoryt
lifted_parameters :
dfcc_lift_memory_predicatest
line :
invariant_failedt
,
xml_graph_nodet
line_no :
cpp_tokent
,
parsert
,
smt2_tokenizert
,
smt2_tokenizert::smt2_errort
line_number :
cscannert
,
ctokent
,
document_propertiest::linet
,
memory_snapshot_harness_generatort::entry_source_locationt
LINE_SEPARATOR :
format_specifiert
lines_covered :
coverage_recordt
lines_total :
coverage_recordt
link_allocated_caller :
dfcc_wrapper_programt
link_deallocated_contract :
dfcc_wrapper_programt
link_ptr_pred_ctx :
dfcc_wrapper_programt
linkage_spec :
cpp_declarator_convertert
linked_allocated :
__CPROVER_contracts_write_set_t
linked_deallocated :
__CPROVER_contracts_write_set_t
linked_ptr_pred_ctx :
__CPROVER_contracts_write_set_t
list :
__CPROVER_jsa_abstract_node
,
__CPROVER_jsa_concrete_node
,
__CPROVER_jsa_iterator
,
code_with_references_listt
list_count :
__CPROVER_jsa_abstract_heap
list_head_nodes :
__CPROVER_jsa_abstract_heap
list_memory_usage :
string_container_statisticst
list_only :
show_goto_functions_jsont
,
show_goto_functions_xmlt
literal_map :
boolbv_mapt::map_entryt
literals :
solver_hardnesst::sat_hardnesst
little_endian :
elf_readert
live_object_exprs :
axiomst
live_variables :
cext
liveness :
vsd_configt
loaded :
dfcc_libraryt
loading_successful :
java_bytecode_parse_treet
loc :
datat
,
object_creation_infot
,
path_nodet
,
reference_allocationt
,
symbol_factoryt
loc_infos :
local_bitvector_analysist
,
local_may_aliast
loc_map :
local_cfgt
local :
abstract_eventt
,
dfcc_loop_infot
local_bitvector_analysis :
goto_check_ct
local_fields :
shadow_memory_field_definitionst
local_map :
interpretert::stack_framet
local_may_alias :
havoc_loopst
,
k_inductiont
local_may_alias_factory :
custom_bitvector_analysist
local_objects :
framet
local_static :
goto_program2codet
local_static_set :
goto_program2codet
local_variable_table :
java_bytecode_parse_treet::methodt
locals :
function_cfg_infot
,
goto_program_cfg_infot
,
java_bytecode_parse_treet::methodt::stack_map_table_entryt
,
local_bitvector_analysist
,
local_may_aliast
,
localst
,
loop_cfg_infot
,
string_abstractiont
localsearch_limit :
satcheck_cadical_baset
location :
conversion_dependenciest
,
default_trace_stept
,
location_update_visitort
,
merge_location_update_visitort
,
symbolt
,
symex_coveraget::coverage_infot
location_map :
goto_unwindt::unwind_logt
location_number :
goto_programt::instructiont
,
memory_snapshot_harness_generatort::entry_goto_locationt
,
value_sett
log :
arrayst
,
bv_minimizet
,
bv_minimizing_dect
,
cegis_verifiert
,
code_contractst
,
compilet
,
complexity_limitert
,
counterexample_beautificationt
,
dfcc_contract_clauses_codegent
,
dfcc_contract_functionst
,
dfcc_contract_handlert
,
dfcc_instrument_loopt
,
dfcc_instrumentt
,
dfcc_is_fresht
,
dfcc_libraryt
,
dfcc_lift_memory_predicatest
,
dfcc_obeys_contractt
,
dfcc_pointer_equalst
,
dfcc_pointer_in_ranget
,
dfcc_spec_functionst
,
dfcc_swap_and_wrapt
,
dfcc_wrapper_programt
,
dfcct
,
function_name_manglert< MangleFun >
,
gdb_apit
,
goto_check_ct
,
goto_inlinet
,
goto_symext
,
goto_verifiert
,
havoc_assigns_targetst
,
incremental_goto_checkert
,
insert_final_assert_falset
,
instrument_spec_assignst
,
java_bytecode_convert_classt
,
java_bytecode_convert_methodt
,
java_class_loader_limitt
,
java_object_factoryt
,
linker_script_merget
,
loop_contracts_synthesizer_baset
,
osx_fat_readert
,
osx_mach_o_readert
,
parse_options_baset
,
parsert
,
piped_processt
,
prop_conv_solvert
,
prop_minimizet
,
propt
,
remove_const_function_pointerst
,
shadow_memoryt
,
smt2_incremental_decision_proceduret
,
smt2irept
,
smt_incremental_dry_run_solvert
,
smt_piped_solver_processt
,
symex_target_equationt
,
taint_analysist
log_map :
goto_inlinet::goto_inline_logt
logic :
smt2_convt
logical_shift_right :
smt_bit_vector_theoryt
long_cnt :
ansi_c_convert_typet
long_double_width :
configt::ansi_ct
long_int_width :
configt::ansi_ct
long_long_int_width :
configt::ansi_ct
loop :
all_paths_enumeratort
,
disjunctive_polynomial_accelerationt
,
enumerating_loop_accelerationt
,
framet::active_loop_infot
,
sat_path_enumeratort
loop_analysis :
loop_with_parent_analysis_templatet< T, C >
loop_analysis_map :
path_storaget
loop_analysist< T, C > :
loop_templatet< T, C >
loop_bound_ :
string_refinementt
loop_contract :
c_wranglert::functiont
loop_contract_config :
code_contractst
,
dfcct
loop_contracts :
functiont
loop_counter :
acceleration_utilst
,
disjunctive_polynomial_accelerationt
,
polynomial_acceleratort
,
sat_path_enumeratort
loop_entry_offsets :
cext
loop_entry_values :
cext
loop_havoc_set :
cegis_verifiert
,
code_contractst
loop_header :
all_paths_enumeratort
,
disjunctive_polynomial_accelerationt
,
enumerating_loop_accelerationt
,
sat_path_enumeratort
loop_id :
dfcc_loop_infot
loop_info_map :
dfcc_cfg_infot
loop_instructions :
loop_templatet< T, C >
loop_iterations :
framet
loop_last_stack :
goto_program2codet
loop_limit :
solver_optionst
loop_map :
goto_program2codet
,
loop_analysist< T, C >
,
unwindsett
loop_names :
code_contractst
loop_number :
goto_programt::instructiont
,
loop_idt
loop_type :
c_wranglert::loop_contract_clauset
loop_unwind_handlers :
symex_bmct
loops :
event_grapht
,
goto_program2codet
loops_info :
framet
low :
mini_bdd_mgrt::reverse_keyt
,
mini_bdd_nodet
lower :
interval_templatet< T >
lower_bound :
string_constraintt
,
widened_ranget
lower_set :
interval_templatet< T >
lowlink :
grapht< N >::tarjant
Generated by
1.17.0