► analyses | |
ai.cpp | Abstract Interpretation |
ai.h | Abstract Interpretation |
call_graph.cpp | Function Call Graphs |
call_graph.h | Function Call Graphs |
cfg_dominators.h | Compute dominators for CFG of goto_function |
constant_propagator.cpp | Constant Propagation |
constant_propagator.h | Constant propagation |
custom_bitvector_analysis.cpp | Field-insensitive, location-sensitive bitvector analysis |
custom_bitvector_analysis.h | Field-insensitive, location-sensitive bitvector analysis |
dependence_graph.cpp | Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010 |
dependence_graph.h | Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010 |
dirty.cpp | Local variables whose address is taken |
dirty.h | Variables whose address is taken |
does_remove_const.cpp | Analyses |
does_remove_const.h | Analyses |
escape_analysis.cpp | Field-insensitive, location-sensitive escape analysis |
escape_analysis.h | Field-insensitive, location-sensitive, over-approximative escape analysis |
flow_insensitive_analysis.cpp | Flow Insensitive Static Analysis |
flow_insensitive_analysis.h | Flow Insensitive Static Analysis |
global_may_alias.cpp | Field-insensitive, location-sensitive global may alias analysis |
global_may_alias.h | Field-insensitive, location-sensitive, over-approximative escape analysis |
goto_check.cpp | GOTO Programs |
goto_check.h | Program Transformation |
goto_rw.cpp | |
goto_rw.h | |
interval_analysis.cpp | Interval Analysis |
interval_analysis.h | Interval Analysis |
interval_domain.cpp | Interval Domain |
interval_domain.h | Interval Domain |
interval_template.h | |
invariant_propagation.cpp | Invariant Propagation |
invariant_propagation.h | Invariant Propagation |
invariant_set.cpp | Invariant Set |
invariant_set.h | Value Set |
invariant_set_domain.cpp | Invariant Set Domain |
invariant_set_domain.h | Value Set |
is_threaded.cpp | Over-approximate Concurrency for Threaded Goto Programs |
is_threaded.h | Over-approximate Concurrency for Threaded Goto Programs |
local_bitvector_analysis.cpp | Field-insensitive, location-sensitive may-alias analysis |
local_bitvector_analysis.h | Field-insensitive, location-sensitive bitvector analysis |
local_cfg.cpp | CFG for One Function |
local_cfg.h | CFG for One Function |
local_may_alias.cpp | Field-insensitive, location-sensitive may-alias analysis |
local_may_alias.h | Field-insensitive, location-sensitive may-alias analysis |
locals.cpp | Local variables |
locals.h | Local variables whose address is taken |
natural_loops.cpp | Dominators |
natural_loops.h | Compute natural loops in a goto_function |
reaching_definitions.cpp | Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010) |
reaching_definitions.h | Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010) |
replace_symbol_ext.cpp | Modified expression replacement for constant propagator |
replace_symbol_ext.h | Modified expression replacement for constant propagator |
static_analysis.cpp | Value Set Propagation |
static_analysis.h | Static Analysis |
uninitialized_domain.cpp | Detection for Uninitialized Local Variables |
uninitialized_domain.h | Detection for Uninitialized Local Variables |
► ansi-c | |
► library | |
converter.cpp | |
cprover.h | |
jsa.h | Counterexample-Guided Inductive Synthesis |
► literals | |
convert_character_literal.cpp | C Language Conversion |
convert_character_literal.h | C++ Language Conversion |
convert_float_literal.cpp | C++ Language Conversion |
convert_float_literal.h | C Language Conversion |
convert_integer_literal.cpp | C++ Language Conversion |
convert_integer_literal.h | C++ Language Conversion |
convert_string_literal.cpp | C/C++ Language Conversion |
convert_string_literal.h | C/C++ Language Conversion |
parse_float.cpp | Conversion of Expressions |
parse_float.h | ANSI-C Conversion / Type Checking |
unescape_string.cpp | ANSI-C Language Conversion |
unescape_string.h | ANSI-C Language Conversion |
anonymous_member.cpp | ANSI-C Language Type Checking |
anonymous_member.h | C Language Type Checking |
ansi_c_convert_type.cpp | SpecC Language Conversion |
ansi_c_convert_type.h | ANSI-C Language Conversion |
ansi_c_declaration.cpp | ANSI-C Language Type Checking |
ansi_c_declaration.h | ANSI-CC Language Type Checking |
ansi_c_entry_point.cpp | |
ansi_c_entry_point.h | |
ansi_c_internal_additions.cpp | |
ansi_c_internal_additions.h | |
ansi_c_language.cpp | |
ansi_c_language.h | |
ansi_c_lex.yy.cpp | |
ansi_c_parse_tree.cpp | |
ansi_c_parse_tree.h | |
ansi_c_parser.cpp | |
ansi_c_parser.h | |
ansi_c_scope.cpp | |
ansi_c_scope.h | |
ansi_c_typecheck.cpp | ANSI-C Language Type Checking |
ansi_c_typecheck.h | ANSI-C Language Type Checking |
ansi_c_y.tab.cpp | |
ansi_c_y.tab.h | |
arm_builtin_headers.h | |
c_misc.cpp | ANSI-C Misc Utilities |
c_misc.h | ANSI-C Misc Utilities |
c_nondet_symbol_factory.cpp | C Nondet Symbol Factory |
c_nondet_symbol_factory.h | C Nondet Symbol Factory |
c_preprocess.cpp | |
c_preprocess.h | |
c_qualifiers.cpp | |
c_qualifiers.h | |
c_sizeof.cpp | Conversion of sizeof Expressions |
c_sizeof.h | |
c_storage_spec.cpp | |
c_storage_spec.h | |
c_typecast.cpp | |
c_typecast.h | |
c_typecheck_argc_argv.cpp | ANSI-C Conversion / Type Checking |
c_typecheck_base.cpp | ANSI-C Conversion / Type Checking |
c_typecheck_base.h | ANSI-C Language Type Checking |
c_typecheck_code.cpp | C Language Type Checking |
c_typecheck_expr.cpp | ANSI-C Language Type Checking |
c_typecheck_initializer.cpp | ANSI-C Conversion / Type Checking |
c_typecheck_type.cpp | C++ Language Type Checking |
c_typecheck_typecast.cpp | |
clang_builtin_headers.h | |
cprover_library.cpp | |
cprover_library.h | |
cw_builtin_headers.h | |
designator.cpp | ANSI-C Language Type Checking |
designator.h | ANSI-C Language Type Checking |
expr2c.cpp | |
expr2c.h | |
expr2c_class.h | |
file_converter.cpp | Convert file contents to C strings |
gcc_builtin_headers_alpha.h | |
gcc_builtin_headers_arm.h | |
gcc_builtin_headers_generic.h | |
gcc_builtin_headers_ia32-2.h | |
gcc_builtin_headers_ia32-3.h | |
gcc_builtin_headers_ia32-4.h | |
gcc_builtin_headers_ia32.h | |
gcc_builtin_headers_math.h | |
gcc_builtin_headers_mem_string.h | |
gcc_builtin_headers_mips.h | |
gcc_builtin_headers_omp.h | |
gcc_builtin_headers_power.h | |
gcc_builtin_headers_tm.h | |
gcc_builtin_headers_ubsan.h | |
padding.cpp | C++ Language Type Checking |
padding.h | ANSI-C Language Type Checking |
preprocessor_line.cpp | ANSI-C Language Conversion |
preprocessor_line.h | ANSI-C Language Conversion |
printf_formatter.cpp | Printf Formatting |
printf_formatter.h | Printf Formatting |
string_constant.cpp | |
string_constant.h | |
type2name.cpp | Type Naming for C |
type2name.h | Type Naming for C |
► assembler | |
assembler_lex.yy.cpp | |
assembler_parser.cpp | |
assembler_parser.h | |
► big-int | |
allocainc.h | |
► cbmc | |
all_properties.cpp | Symbolic Execution of ANSI-C |
all_properties_class.h | Symbolic Execution of ANSI-C |
bmc.cpp | Symbolic Execution of ANSI-C |
bmc.h | Bounded Model Checking for ANSI-C + HDL |
bmc_cover.cpp | Test-Suite Generation with BMC |
bv_cbmc.cpp | |
bv_cbmc.h | |
cbmc_dimacs.cpp | Writing DIMACS Files |
cbmc_dimacs.h | Writing DIMACS Files |
cbmc_languages.cpp | Language Registration |
cbmc_main.cpp | CBMC Main Module |
cbmc_parse_options.cpp | CBMC Command Line Option Processing |
cbmc_parse_options.h | CBMC Command Line Option Processing |
cbmc_solvers.cpp | Solvers for VCs Generated by Symbolic Execution of ANSI-C |
cbmc_solvers.h | Bounded Model Checking for ANSI-C + HDL |
counterexample_beautification.cpp | Counterexample Beautification using Incremental SAT |
counterexample_beautification.h | Counterexample Beautification |
fault_localization.cpp | Fault Localization |
fault_localization.h | Fault Localization |
show_vcc.cpp | Symbolic Execution of ANSI-C |
symex_bmc.cpp | Bounded Model Checking for ANSI-C |
symex_bmc.h | Bounded Model Checking for ANSI-C |
symex_coverage.cpp | Record and print code coverage of symbolic execution |
symex_coverage.h | Record and print code coverage of symbolic execution |
version.h | |
xml_interface.cpp | XML Interface |
xml_interface.h | XML Interface |
► clobber | |
clobber_main.cpp | Symex Main Module |
clobber_parse_options.cpp | Symex Command Line Options Processing |
clobber_parse_options.h | Command Line Parsing |
► cpp | |
cpp_constructor.cpp | C++ Language Type Checking |
cpp_convert_type.cpp | C++ Language Type Conversion |
cpp_convert_type.h | C++ Language Conversion |
cpp_declaration.cpp | C++ Language Type Checking |
cpp_declaration.h | C++ Language Type Checking |
cpp_declarator.cpp | C++ Language Type Checking |
cpp_declarator.h | C++ Language Type Checking |
cpp_declarator_converter.cpp | C++ Language Type Checking |
cpp_declarator_converter.h | C++ Language Type Checking |
cpp_destructor.cpp | C++ Language Type Checking |
cpp_enum_type.cpp | C++ Language Type Checking |
cpp_enum_type.h | C++ Language Type Checking |
cpp_exception_id.cpp | C++ Language Type Checking |
cpp_exception_id.h | C++ Language Type Checking |
cpp_id.cpp | C++ Language Type Checking |
cpp_id.h | C++ Language Type Checking |
cpp_instantiate_template.cpp | C++ Language Type Checking |
cpp_internal_additions.cpp | |
cpp_internal_additions.h | |
cpp_is_pod.cpp | C++ Language Type Checking |
cpp_item.h | C++ Language Type Checking |
cpp_language.cpp | C++ Language Module |
cpp_language.h | C++ Language Module |
cpp_linkage_spec.h | C++ Language Type Checking |
cpp_member_spec.h | |
cpp_name.cpp | C++ Language Type Checking |
cpp_name.h | |
cpp_namespace_spec.cpp | C++ Language Type Checking |
cpp_namespace_spec.h | C++ Language Type Checking |
cpp_parse_tree.cpp | C++ Parser |
cpp_parse_tree.h | C++ Parser |
cpp_parser.cpp | C++ Parser |
cpp_parser.h | C++ Parser |
cpp_scope.cpp | C++ Language Type Checking |
cpp_scope.h | C++ Language Type Checking |
cpp_scopes.cpp | C++ Language Type Checking |
cpp_scopes.h | C++ Language Type Checking |
cpp_static_assert.h | C++ Language Type Checking |
cpp_storage_spec.h | |
cpp_template_args.h | C++ Language Type Checking |
cpp_template_parameter.h | |
cpp_template_type.h | |
cpp_token.h | C++ Parser: Token |
cpp_token_buffer.cpp | C++ Parser: Token Buffer |
cpp_token_buffer.h | C++ Parser: Token Buffer |
cpp_type2name.cpp | C++ Language Module |
cpp_type2name.h | C++ Language Module |
cpp_typecast.h | |
cpp_typecheck.cpp | C++ Language Type Checking |
cpp_typecheck.h | C++ Language Type Checking |
cpp_typecheck_bases.cpp | C++ Language Type Checking |
cpp_typecheck_code.cpp | C++ Language Type Checking |
cpp_typecheck_compound_type.cpp | C++ Language Type Checking |
cpp_typecheck_constructor.cpp | C++ Language Type Checking |
cpp_typecheck_conversions.cpp | C++ Language Type Checking |
cpp_typecheck_declaration.cpp | C++ Language Type Checking |
cpp_typecheck_destructor.cpp | C++ Language Type Checking |
cpp_typecheck_enum_type.cpp | C++ Language Type Checking |
cpp_typecheck_expr.cpp | C++ Language Type Checking |
cpp_typecheck_fargs.cpp | C++ Language Type Checking |
cpp_typecheck_fargs.h | C++ Language Type Checking |
cpp_typecheck_function.cpp | C++ Language Type Checking |
cpp_typecheck_initializer.cpp | C++ Language Type Checking |
cpp_typecheck_linkage_spec.cpp | C++ Language Type Checking |
cpp_typecheck_method_bodies.cpp | C++ Language Type Checking |
cpp_typecheck_namespace.cpp | C++ Language Type Checking |
cpp_typecheck_resolve.cpp | C++ Language Type Checking |
cpp_typecheck_resolve.h | C++ Language Type Checking |
cpp_typecheck_static_assert.cpp | C++ Language Type Checking |
cpp_typecheck_template.cpp | C++ Language Type Checking |
cpp_typecheck_type.cpp | C++ Language Type Checking |
cpp_typecheck_using.cpp | C++ Language Type Checking |
cpp_typecheck_virtual_table.cpp | C++ Language Type Checking |
cpp_using.h | C++ Language Type Checking |
cpp_util.cpp | |
cpp_util.h | |
expr2cpp.cpp | |
expr2cpp.h | |
parse.cpp | C++ Language Parsing |
recursion_counter.h | C++ Language Type Checking |
template_map.cpp | C++ Language Type Checking |
template_map.h | C++ Language Type Checking |
► doc | |
► assets | |
driver.h | |
kdev_t.h | |
modules.h | |
► goto-analyzer | |
goto_analyzer_main.cpp | Goto-Analyser Main Module |
goto_analyzer_parse_options.cpp | Goto-Analyser Command Line Option Processing |
goto_analyzer_parse_options.h | Goto-Analyser Command Line Option Processing |
static_analyzer.cpp | |
static_analyzer.h | |
taint_analysis.cpp | Taint Analysis |
taint_analysis.h | Taint Analysis |
taint_parser.cpp | Taint Parser |
taint_parser.h | Taint Parser |
unreachable_instructions.cpp | List all unreachable instructions |
unreachable_instructions.h | List all unreachable instructions |
► goto-cc | |
► xml_binaries | |
read_goto_object.cpp | Read goto object files |
read_goto_object.h | Read goto object files |
xml_goto_function.cpp | Convert goto functions to xml structures and back |
xml_goto_function.h | Convert goto functions into xml structures and back |
xml_goto_function_hashing.cpp | Convert goto functions to xml structures and back (with irep hashing) |
xml_goto_function_hashing.h | Convert goto functions into xml structures and back (with irep hashing) |
xml_goto_program.cpp | Convert goto programs to xml structures and back |
xml_goto_program.h | Convert goto programs into xml structures and back |
xml_goto_program_hashing.cpp | Convert goto programs to xml structures and back (with irep hashing) |
xml_goto_program_hashing.h | Convert goto programs into xml structures and back (with irep hashing) |
xml_irep_hashing.cpp | XML-irep conversions with hashing |
xml_irep_hashing.h | XML-irep conversions with hashing |
xml_symbol.cpp | Compile and link source and object files |
xml_symbol.h | Converts symbols to xml structures and back |
xml_symbol_hashing.cpp | XML-symbol conversions with irep hashing |
xml_symbol_hashing.h | XML-symbol conversions with irep hashing |
armcc_cmdline.cpp | A special command line object to mimic ARM's armcc |
armcc_cmdline.h | A special command line object to mimic ARM's armcc |
armcc_mode.cpp | Command line option container |
armcc_mode.h | Base class for command line interpretation for CL |
as86_cmdline.cpp | A special command line object for as86 (of Bruce's C Compiler) |
as86_cmdline.h | A special command line object for as86 (of Bruce's C Compiler) Author: Michael Tautschnig Date: July 2016 |
as_cmdline.cpp | A special command line object for GNU Assembler |
as_cmdline.h | A special command line object for GNU Assembler Author: Michael Tautschnig Date: July 2016 |
as_mode.cpp | Assembler Mode |
as_mode.h | Assembler Mode |
bcc_cmdline.cpp | A special command line object for Bruce's C Compiler |
bcc_cmdline.h | A special command line object for Bruce's C Compiler Author: Michael Tautschnig Date: July 2016 |
compile.cpp | Compile and link source and object files |
compile.h | Compile and link source and object files |
cw_mode.cpp | Command line option container |
cw_mode.h | Base class for command line interpretation |
gcc_cmdline.cpp | A special command line object for the gcc-like options |
gcc_cmdline.h | A special command line object for the gcc-like options |
gcc_mode.cpp | GCC Mode |
gcc_mode.h | Base class for command line interpretation |
goto_cc_cmdline.cpp | Command line interpretation for goto-cc |
goto_cc_cmdline.h | Command line interpretation for goto-cc |
goto_cc_languages.cpp | Language Registration |
goto_cc_main.cpp | GOTO-CC Main Module |
goto_cc_mode.cpp | Command line option container |
goto_cc_mode.h | Command line interpretation for goto-cc |
ld_cmdline.cpp | A special command line object for the ld-like options |
ld_cmdline.h | A special command line object for the ld-like options |
ms_cl_cmdline.cpp | A special command line object for the CL options |
ms_cl_cmdline.h | A special command line object for the gcc-like options |
ms_cl_mode.cpp | Visual Studio CL Mode |
ms_cl_mode.h | Visual Studio CL Mode |
► goto-diff | |
change_impact.cpp | Data and control-dependencies of syntactic diff |
change_impact.h | Data and control-dependencies of syntactic diff |
goto_diff.h | GOTO-DIFF Base Class |
goto_diff_base.cpp | GOTO-DIFF Base Class |
goto_diff_languages.cpp | Language Registration |
goto_diff_languages.h | GOTO-DIFF Languages |
goto_diff_main.cpp | GOTO-DIFF Main Module |
goto_diff_parse_options.cpp | GOTO-DIFF Command Line Option Processing |
goto_diff_parse_options.h | GOTO-DIFF Command Line Option Processing |
syntactic_diff.cpp | Syntactic GOTO-DIFF |
syntactic_diff.h | Syntactic GOTO-DIFF |
unified_diff.cpp | Unified diff (using LCSS) of goto functions |
unified_diff.h | Unified diff (using LCSS) of goto functions |
► goto-instrument | |
► accelerate | |
accelerate.cpp | Loop Acceleration |
accelerate.h | Loop Acceleration |
acceleration_utils.cpp | Loop Acceleration |
acceleration_utils.h | Loop Acceleration |
accelerator.h | Loop Acceleration |
all_paths_enumerator.cpp | Loop Acceleration |
all_paths_enumerator.h | Loop Acceleration |
cone_of_influence.cpp | Loop Acceleration |
cone_of_influence.h | Loop Acceleration |
disjunctive_polynomial_acceleration.cpp | Loop Acceleration |
disjunctive_polynomial_acceleration.h | Loop Acceleration |
enumerating_loop_acceleration.cpp | Loop Acceleration |
enumerating_loop_acceleration.h | Loop Acceleration |
linearize.cpp | Loop Acceleration |
linearize.h | Loop Acceleration |
loop_acceleration.h | Loop Acceleration |
overflow_instrumenter.cpp | Loop Acceleration |
overflow_instrumenter.h | Loop Acceleration |
path.cpp | Loop Acceleration |
path.h | Loop Acceleration |
path_acceleration.h | Loop Acceleration |
path_enumerator.h | Loop Acceleration |
polynomial.cpp | Loop Acceleration |
polynomial.h | Loop Acceleration |
polynomial_accelerator.cpp | Loop Acceleration |
polynomial_accelerator.h | Loop Acceleration |
sat_path_enumerator.cpp | Loop Acceleration |
sat_path_enumerator.h | Loop Acceleration |
scratch_program.cpp | Loop Acceleration |
scratch_program.h | Loop Acceleration |
subsumed.h | Loop Acceleration |
trace_automaton.cpp | Loop Acceleration |
trace_automaton.h | Loop Acceleration |
util.cpp | Loop Acceleration |
util.h | Loop Acceleration |
► wmm | |
abstract_event.cpp | Abstract events |
abstract_event.h | Abstract events |
cycle_collection.cpp | Collection of cycles in graph of abstract events |
data_dp.cpp | Data dependencies |
data_dp.h | Data dependencies |
event_graph.cpp | Graph of abstract events |
event_graph.h | Graph of abstract events |
fence.cpp | Fences for instrumentation |
fence.h | Fences for instrumentation |
goto2graph.cpp | Turns a goto-program into an abstract event graph |
goto2graph.h | Instrumenter |
instrumenter_pensieve.h | Instrumenter |
instrumenter_strategies.cpp | Strategies for picking the abstract events to instrument |
pair_collection.cpp | Collection of pairs (for Pensieve's static delay-set analysis) in graph of abstract events |
shared_buffers.cpp | |
shared_buffers.h | |
weak_memory.cpp | Weak Memory Instrumentation for Threaded Goto Programs |
weak_memory.h | Weak Memory Instrumentation for Threaded Goto Programs |
wmm.h | Memory models |
alignment_checks.cpp | Alignment Checks |
alignment_checks.h | Alignment Checks |
branch.cpp | Branch Instrumentation |
branch.h | Branch Instrumentation |
call_sequences.cpp | Printing function call sequences for Ofer |
call_sequences.h | Memory-mapped I/O Instrumentation for Goto Programs |
code_contracts.cpp | Verify and use annotated invariants and pre/post-conditions |
code_contracts.h | Verify and use annotated invariants and pre/post-conditions |
concurrency.cpp | Encoding for Threaded Goto Programs |
concurrency.h | Encoding for Threaded Goto Programs |
count_eloc.cpp | Count effective lines of code |
count_eloc.h | Count effective lines of code |
cover.cpp | Coverage Instrumentation |
cover.h | Coverage Instrumentation |
document_properties.cpp | Subgoal Documentation |
document_properties.h | Documentation of Properties |
dot.cpp | Dump Goto-Program as DOT Graph |
dot.h | Dump Goto-Program as DOT Graph |
dump_c.cpp | Dump Goto-Program as C/C++ Source |
dump_c.h | Dump C from Goto Program |
dump_c_class.h | Dump Goto-Program as C/C++ Source |
full_slicer.cpp | Slicing |
full_slicer.h | Slicing |
full_slicer_class.h | Goto Program Slicing |
function.cpp | Function Entering and Exiting |
function.h | Function Entering and Exiting |
function_modifies.cpp | Modifies |
function_modifies.h | Modifies |
goto_instrument_languages.cpp | Language Registration |
goto_instrument_main.cpp | Main Module |
goto_instrument_parse_options.cpp | Main Module |
goto_instrument_parse_options.h | Command Line Parsing |
goto_program2code.cpp | Dump Goto-Program as C/C++ Source |
goto_program2code.h | Dump Goto-Program as C/C++ Source |
havoc_loops.cpp | Havoc Loops |
havoc_loops.h | Havoc Loops |
horn_encoding.cpp | Horn-clause Encoding |
horn_encoding.h | Horn-clause Encoding |
interrupt.cpp | Interrupt Instrumentation |
interrupt.h | Interrupt Instrumentation for Goto Programs |
k_induction.cpp | K-induction |
k_induction.h | K-induction |
loop_utils.cpp | Helper functions for k-induction and loop invariants |
loop_utils.h | Helper functions for k-induction and loop invariants |
mmio.cpp | Memory-mapped I/O Instrumentation for Goto Programs |
mmio.h | Memory-mapped I/O Instrumentation for Goto Programs |
model_argc_argv.cpp | Initialize command line arguments |
model_argc_argv.h | Initialize command line arguments |
nondet_static.cpp | Nondeterministic initialization of certain global scope variables |
nondet_static.h | Nondeterministic initialization of certain global scope variables |
nondet_volatile.cpp | Volatile Variables |
nondet_volatile.h | Volatile Variables |
object_id.cpp | Object Identifiers |
object_id.h | Object Identifiers |
points_to.cpp | Field-sensitive, location-insensitive points-to analysis |
points_to.h | Field-sensitive, location-insensitive points-to analysis |
race_check.cpp | Race Detection for Threaded Goto Programs |
race_check.h | Race Detection for Threaded Goto Programs |
reachability_slicer.cpp | Slicer |
reachability_slicer.h | Slicing |
reachability_slicer_class.h | Goto Program Slicing |
remove_function.cpp | Remove function definition |
remove_function.h | Remove function definition |
rw_set.cpp | Race Detection for Threaded Goto Programs |
rw_set.h | Race Detection for Threaded Goto Programs |
show_locations.cpp | Show program locations |
show_locations.h | Show program locations |
skip_loops.cpp | Skip over selected loops by adding gotos |
skip_loops.h | Skip over selected loops by adding gotos |
stack_depth.cpp | Stack depth checks |
stack_depth.h | Stack depth checks |
thread_instrumentation.cpp | |
thread_instrumentation.h | |
undefined_functions.cpp | Handling of functions without body |
undefined_functions.h | Handling of functions without body |
uninitialized.cpp | Detection for Uninitialized Local Variables |
uninitialized.h | Detection for Uninitialized Local Variables |
unwind.cpp | Loop unwinding |
unwind.h | Loop unwinding |
► goto-programs | |
basic_blocks.cpp | Group Basic Blocks in Goto Program |
basic_blocks.h | Group Basic Blocks in Goto Program |
builtin_functions.cpp | Program Transformation |
cfg.h | Control Flow Graph |
class_hierarchy.cpp | Class Hierarchy |
class_hierarchy.h | Class Hierarchy |
class_identifier.cpp | Extract class identifier |
class_identifier.h | Extract class identifier |
compute_called_functions.cpp | Query Called Functions |
compute_called_functions.h | Query Called Functions |
destructor.cpp | Destructor Calls |
destructor.h | Destructor Calls |
elf_reader.cpp | Read ELF |
elf_reader.h | Read ELF |
format_strings.cpp | Format String Parser |
format_strings.h | Format String Parser |
goto_asm.cpp | Assembler -> Goto |
goto_clean_expr.cpp | Program Transformation |
goto_convert.cpp | Program Transformation |
goto_convert.h | Program Transformation |
goto_convert_class.h | Program Transformation |
goto_convert_exceptions.cpp | Program Transformation |
goto_convert_function_call.cpp | Program Transformation |
goto_convert_functions.cpp | |
goto_convert_functions.h | Goto Programs with Functions |
goto_convert_new_switch_case.cpp | Program Transformation |
goto_convert_side_effect.cpp | Program Transformation |
goto_functions.cpp | Goto Programs with Functions |
goto_functions.h | Goto Programs with Functions |
goto_functions_template.h | Goto Programs with Functions |
goto_inline.cpp | Function Inlining |
goto_inline.h | Function Inlining |
goto_inline_class.cpp | Function Inlining |
goto_inline_class.h | |
goto_model.h | Symbol Table + CFG |
goto_program.cpp | Program Transformation |
goto_program.h | Concrete Goto Program |
goto_program_irep.cpp | Goto_programt -> irep conversion |
goto_program_irep.h | Goto_programt -> irep conversion |
goto_program_template.cpp | Goto Program Template |
goto_program_template.h | Goto Program Template |
goto_trace.cpp | Traces of GOTO Programs |
goto_trace.h | Traces of GOTO Programs |
graphml_witness.cpp | Witnesses for Traces and Proofs |
graphml_witness.h | Witnesses for Traces and Proofs |
initialize_goto_model.cpp | Get a Goto Program |
initialize_goto_model.h | Initialize a Goto Program |
interpreter.cpp | Interpreter for GOTO Programs |
interpreter.h | Interpreter for GOTO Programs |
interpreter_class.h | Interpreter for GOTO Programs |
interpreter_evaluate.cpp | Interpreter for GOTO Programs |
json_goto_trace.cpp | Traces of GOTO Programs |
json_goto_trace.h | Traces of GOTO Programs |
link_to_library.cpp | Library Linking |
link_to_library.h | Library Linking |
loop_ids.cpp | Loop IDs |
loop_ids.h | Loop IDs |
mm_io.cpp | Perform Memory-mapped I/O instrumentation |
mm_io.h | Perform Memory-mapped I/O instrumentation |
osx_fat_reader.cpp | Read Mach-O |
osx_fat_reader.h | Read OS X Fat Binaries |
parameter_assignments.cpp | Add parameter assignments |
parameter_assignments.h | Add parameter assignments |
pointer_arithmetic.cpp | |
pointer_arithmetic.h | |
property_checker.cpp | Property Checker Interface |
property_checker.h | Property Checker Interface |
read_bin_goto_object.cpp | Read goto object files |
read_bin_goto_object.h | Read goto object files |
read_goto_binary.cpp | Read Goto Programs |
read_goto_binary.h | Read Goto Programs |
remove_asm.cpp | Remove 'asm' statements by compiling into suitable standard code |
remove_asm.h | Remove 'asm' statements by compiling into suitable standard code |
remove_complex.cpp | Remove 'complex' data type |
remove_complex.h | Remove the 'complex' data type by compilation into structs |
remove_const_function_pointers.cpp | Goto Programs |
remove_const_function_pointers.h | Goto Programs |
remove_exceptions.cpp | Remove exception handling |
remove_exceptions.h | Remove function exceptional returns |
remove_function_pointers.cpp | Program Transformation |
remove_function_pointers.h | Remove Indirect Function Calls |
remove_instanceof.cpp | Remove Instance-of Operators |
remove_instanceof.h | Remove Instance-of Operators |
remove_returns.cpp | Remove function return values |
remove_returns.h | Remove function returns |
remove_skip.cpp | Program Transformation |
remove_skip.h | Program Transformation |
remove_static_init_loops.cpp | Unwind loops in static initializers |
remove_static_init_loops.h | Unwind loops in static initializers |
remove_unreachable.cpp | Program Transformation |
remove_unreachable.h | Program Transformation |
remove_unused_functions.cpp | Unused function removal |
remove_unused_functions.h | Unused function removal |
remove_vector.cpp | Remove 'vector' data type |
remove_vector.h | Remove the 'vector' data type by compilation into arrays |
remove_virtual_functions.cpp | Remove Virtual Function (Method) Calls |
remove_virtual_functions.h | Remove Virtual Function (Method) Calls |
safety_checker.cpp | Safety Checker Interface |
safety_checker.h | Safety Checker Interface |
set_properties.cpp | Set Properties |
set_properties.h | Set the properties to check |
show_goto_functions.cpp | Show goto functions |
show_goto_functions.h | Show the goto functions |
show_goto_functions_json.cpp | Goto Program |
show_goto_functions_json.h | Goto Program |
show_goto_functions_xml.cpp | Goto Program |
show_goto_functions_xml.h | Goto Program |
show_properties.cpp | Show Claims |
show_properties.h | Show the properties |
show_symbol_table.cpp | Show the symbol table |
show_symbol_table.h | Show the symbol table |
slice_global_inits.cpp | Remove initializations of unused global variables |
slice_global_inits.h | Remove initializations of unused global variables |
string_abstraction.cpp | String Abstraction |
string_abstraction.h | String Abstraction |
string_instrumentation.cpp | String Abstraction |
string_instrumentation.h | String Abstraction |
vcd_goto_trace.cpp | Traces of GOTO Programs in VCD (Value Change Dump) Format |
vcd_goto_trace.h | Traces of GOTO Programs in VCD (Value Change Dump) Format |
wp.cpp | Weakest Preconditions |
wp.h | Weakest Preconditions |
write_goto_binary.cpp | Write GOTO binaries |
write_goto_binary.h | Write GOTO binaries |
xml_goto_trace.cpp | Traces of GOTO Programs |
xml_goto_trace.h | Traces of GOTO Programs |
► goto-symex | |
adjust_float_expressions.cpp | Symbolic Execution |
adjust_float_expressions.h | Symbolic Execution |
auto_objects.cpp | Symbolic Execution of ANSI-C |
build_goto_trace.cpp | Traces of GOTO Programs |
build_goto_trace.h | Traces of GOTO Programs |
goto_symex.cpp | Symbolic Execution |
goto_symex.h | Symbolic Execution |
goto_symex_state.cpp | Symbolic Execution |
goto_symex_state.h | Symbolic Execution |
memory_model.cpp | Memory model for partial order concurrency |
memory_model.h | Memory models for partial order concurrency |
memory_model_pso.cpp | Memory model for partial order concurrency |
memory_model_pso.h | Memory models for partial order concurrency |
memory_model_sc.cpp | Memory model for partial order concurrency |
memory_model_sc.h | Memory models for partial order concurrency |
memory_model_tso.cpp | Memory model for partial order concurrency |
memory_model_tso.h | Memory models for partial order concurrency |
partial_order_concurrency.cpp | Add constraints to equation encoding partial orders on events |
partial_order_concurrency.h | Add constraints to equation encoding partial orders on events |
postcondition.cpp | Symbolic Execution |
postcondition.h | Generate Equation using Symbolic Execution |
precondition.cpp | Symbolic Execution |
precondition.h | Generate Equation using Symbolic Execution |
rewrite_union.cpp | Symbolic Execution of ANSI-C |
rewrite_union.h | Symbolic Execution |
slice.cpp | Slicer for symex traces |
slice.h | Slicer for symex traces |
slice_by_trace.cpp | Slicer for symex traces |
slice_by_trace.h | Slicer for matching with trace files |
symex_assign.cpp | Symbolic Execution |
symex_atomic_section.cpp | Symbolic Execution |
symex_builtin_functions.cpp | Symbolic Execution of ANSI-C |
symex_catch.cpp | Symbolic Execution |
symex_clean_expr.cpp | Symbolic Execution of ANSI-C |
symex_dead.cpp | Symbolic Execution |
symex_decl.cpp | Symbolic Execution |
symex_dereference.cpp | Symbolic Execution of ANSI-C |
symex_dereference_state.cpp | Symbolic Execution of ANSI-C |
symex_dereference_state.h | Symbolic Execution of ANSI-C |
symex_function_call.cpp | Symbolic Execution of ANSI-C |
symex_goto.cpp | Symbolic Execution |
symex_main.cpp | Symbolic Execution |
symex_other.cpp | Symbolic Execution |
symex_slice_class.h | Slicer for symex traces |
symex_start_thread.cpp | Symbolic Execution |
symex_target.cpp | Symbolic Execution |
symex_target.h | Generate Equation using Symbolic Execution |
symex_target_equation.cpp | Symbolic Execution |
symex_target_equation.h | Generate Equation using Symbolic Execution |
symex_throw.cpp | Symbolic Execution |
► java_bytecode | |
bytecode_info.cpp | |
bytecode_info.h | |
character_refine_preprocess.cpp | Preprocess a goto-programs so that calls to the java Character library are replaced by simple expressions |
character_refine_preprocess.h | Preprocess a goto-programs so that calls to the java Character library are replaced by simple expressions |
ci_lazy_methods.cpp | Context-insensitive lazy methods container |
ci_lazy_methods.h | Context-insensitive lazy methods container |
expr2java.cpp | |
expr2java.h | |
jar_file.cpp | |
jar_file.h | JAR File Reading |
java_bytecode_convert_class.cpp | JAVA Bytecode Language Conversion |
java_bytecode_convert_class.h | JAVA Bytecode Language Conversion |
java_bytecode_convert_method.cpp | JAVA Bytecode Language Conversion |
java_bytecode_convert_method.h | JAVA Bytecode Language Conversion |
java_bytecode_convert_method_class.h | JAVA Bytecode Language Conversion |
java_bytecode_internal_additions.cpp | |
java_bytecode_internal_additions.h | |
java_bytecode_language.cpp | |
java_bytecode_language.h | |
java_bytecode_parse_tree.cpp | |
java_bytecode_parse_tree.h | |
java_bytecode_parser.cpp | |
java_bytecode_parser.h | |
java_bytecode_typecheck.cpp | JAVA Bytecode Conversion / Type Checking |
java_bytecode_typecheck.h | JAVA Bytecode Language Type Checking |
java_bytecode_typecheck_code.cpp | JAVA Bytecode Conversion / Type Checking |
java_bytecode_typecheck_expr.cpp | JAVA Bytecode Conversion / Type Checking |
java_bytecode_typecheck_type.cpp | JAVA Bytecode Conversion / Type Checking |
java_bytecode_vtable.cpp | |
java_bytecode_vtable.h | |
java_class_loader.cpp | |
java_class_loader.h | |
java_class_loader_limit.cpp | Limit class path loading |
java_class_loader_limit.h | Limit class path loading |
java_entry_point.cpp | |
java_entry_point.h | |
java_local_variable_table.cpp | Java local variable table processing |
java_object_factory.cpp | |
java_object_factory.h | |
java_pointer_casts.cpp | JAVA Pointer Casts |
java_pointer_casts.h | JAVA Pointer Casts |
java_root_class.cpp | |
java_root_class.h | |
java_types.cpp | |
java_types.h | |
java_utils.cpp | |
java_utils.h | |
► jsil | |
expr2jsil.cpp | Jsil Language |
expr2jsil.h | Jsil Language |
jsil_convert.cpp | Jsil Language Conversion |
jsil_convert.h | Jsil Language Conversion |
jsil_entry_point.cpp | Jsil Language |
jsil_entry_point.h | Jsil Language |
jsil_internal_additions.cpp | Jsil Language |
jsil_internal_additions.h | Jsil Language |
jsil_language.cpp | Jsil Language |
jsil_language.h | Jsil Language |
jsil_lex.yy.cpp | |
jsil_parse_tree.cpp | Jsil Language |
jsil_parse_tree.h | Jsil Language |
jsil_parser.cpp | Jsil Language |
jsil_parser.h | Jsil Language |
jsil_typecheck.cpp | Jsil Language |
jsil_typecheck.h | Jsil Language |
jsil_types.cpp | Jsil Language |
jsil_types.h | Jsil Language |
jsil_y.tab.cpp | |
jsil_y.tab.h | |
► json | |
json_lex.yy.cpp | |
json_parser.cpp | |
json_parser.h | |
json_y.tab.cpp | |
json_y.tab.h | |
► langapi | |
language_ui.cpp | |
language_ui.h | |
language_util.cpp | |
language_util.h | |
languages.cpp | |
languages.h | |
mode.cpp | |
mode.h | |
► linking | |
linking.cpp | ANSI-C Linking |
linking.h | ANSI-C Linking |
linking_class.h | ANSI-C Linking |
remove_internal_symbols.cpp | Remove symbols that are internal only |
remove_internal_symbols.h | Remove symbols that are internal only |
static_lifetime_init.cpp | |
static_lifetime_init.h | |
zero_initializer.cpp | Linking: Zero Initialization |
zero_initializer.h | Linking: Zero Initialization |
► memory-models | |
mm2cpp.cpp | |
mm2cpp.h | |
mm_parser.cpp | |
mm_parser.h | |
mmcc_main.cpp | Mmcc Main Module |
mmcc_parse_options.cpp | Mmcc Command Line Option Processing |
mmcc_parse_options.h | Mmcc Command Line Option Processing |
► miniz | |
miniz.cpp | |
miniz.h | |
► musketeer | |
cycles_visitor.cpp | Cycles visitor for computing edges involved for fencing |
cycles_visitor.h | Cycles visitor for computing edges involved for fencing |
fence_assert.cpp | ILP construction for cycles affecting user-assertions and resolution |
fence_assert.h | ILP construction for cycles affecting user-assertions and resolution |
fence_inserter.cpp | ILP construction for all cycles and resolution |
fence_inserter.h | ILP construction for all cycles and resolution |
fence_shared.cpp | |
fence_shared.h | (naive) Fence insertion |
fence_user_def.cpp | ILP construction for cycles affecting user-assertions and resolution |
fence_user_def.h | ILP construction for cycles containing user-placed fences and resolution |
fencer.cpp | Fence inference: Main |
fencer.h | Fence inference |
graph_visitor.cpp | Graph visitor for computing edges involved for fencing |
graph_visitor.h | Graph visitor for computing edges involved for fencing |
ilp.h | ILP structure |
infer_mode.h | |
languages.cpp | Language Registration |
musketeer_main.cpp | Main Module |
musketeer_parse_options.cpp | Main Module |
musketeer_parse_options.h | Command Line Parsing |
pensieve.cpp | |
pensieve.h | Fence insertion following criteria of Pensieve (PPoPP'05) |
propagate_const_function_pointers.cpp | Constant Function Pointer Propagation |
propagate_const_function_pointers.h | Constant Function Pointer Propagation |
replace_async.h | |
version.h | |
► path-symex | |
build_goto_trace.cpp | Build Goto Trace from State History |
build_goto_trace.h | Build Goto Trace from Path Symex History |
loc_ref.h | Program Locations |
locs.cpp | Program Locations |
locs.h | CFG made of Program Locations, built from goto_functionst |
path_replay.cpp | Dense Data Structure for Path Replay |
path_replay.h | Dense Data Structure for Path Replay |
path_symex.cpp | Concrete Symbolic Transformer |
path_symex.h | Concrete Symbolic Transformer |
path_symex_class.h | Concrete Symbolic Transformer |
path_symex_history.cpp | History of path-based symbolic simulator |
path_symex_history.h | History for path-based symbolic simulator |
path_symex_state.cpp | State of path-based symbolic simulator |
path_symex_state.h | State of path-based symbolic simulator |
path_symex_state_read.cpp | State of path-based symbolic simulator |
var_map.cpp | Variable Numbering |
var_map.h | Variable Numbering |
► pointer-analysis | |
add_failed_symbols.cpp | Pointer Dereferencing |
add_failed_symbols.h | Pointer Dereferencing |
dereference.cpp | Symbolic Execution of ANSI-C |
dereference.h | Pointer Dereferencing |
dereference_callback.cpp | Pointer Dereferencing |
dereference_callback.h | Pointer Dereferencing |
goto_program_dereference.cpp | Dereferencing Operations on GOTO Programs |
goto_program_dereference.h | Value Set |
object_numbering.h | Value Set |
pointer_offset_sum.cpp | Pointer Analysis |
pointer_offset_sum.h | Pointer Dereferencing |
rewrite_index.cpp | Pointer Dereferencing |
rewrite_index.h | Pointer Dereferencing |
show_value_sets.cpp | Show Value Sets |
show_value_sets.h | Show Value Sets |
value_set.cpp | Value Set |
value_set.h | Value Set |
value_set_analysis.cpp | Value Set Propagation |
value_set_analysis.h | Value Set Propagation |
value_set_analysis_fi.cpp | Value Set Propagation (Flow Insensitive) |
value_set_analysis_fi.h | Value Set Propagation (flow insensitive) |
value_set_analysis_fivr.cpp | Value Set Propagation (Flow Insensitive) |
value_set_analysis_fivr.h | Value Set Propagation |
value_set_analysis_fivrns.cpp | Value Set Propagation (Flow Insensitive, Validity Regions) |
value_set_analysis_fivrns.h | Value Set Analysis (Flow Insensitive, Validity Regions) |
value_set_dereference.cpp | Symbolic Execution of ANSI-C |
value_set_dereference.h | Pointer Dereferencing |
value_set_domain.cpp | Value Set |
value_set_domain.h | Value Set |
value_set_domain_fi.cpp | Value Set Domain (Flow Insensitive) |
value_set_domain_fi.h | Value Set (Flow Insensitive) |
value_set_domain_fivr.cpp | Value Set Domain (Flow Insensitive, Sharing, Validity Regions) |
value_set_domain_fivr.h | Value Set (Flow Insensitive, Sharing, Validity Regions) |
value_set_domain_fivrns.cpp | Value Set Domain (Flow Insensitive, Validity Regions) |
value_set_domain_fivrns.h | Value Set Domain (Flow Insensitive, Validity Regions) |
value_set_fi.cpp | Value Set (Flow Insensitive, Sharing) |
value_set_fi.h | Value Set (Flow Insensitive, Sharing) |
value_set_fivr.cpp | Value Set (Flow Insensitive, Sharing, Validity Regions) |
value_set_fivr.h | Value Set (Flow Insensitive, Sharing, Validity Regions) |
value_set_fivrns.cpp | Value Set (Flow Insensitive, Validity Regions) |
value_set_fivrns.h | Value Set (Flow Insensitive, Validity Regions) |
value_sets.h | Value Set Propagation |
► solvers | |
► cvc | |
cvc_conv.cpp | |
cvc_conv.h | |
cvc_dec.cpp | |
cvc_dec.h | |
cvc_prop.cpp | |
cvc_prop.h | |
► dplib | |
dplib_conv.cpp | |
dplib_conv.h | |
dplib_dec.cpp | |
dplib_dec.h | |
dplib_prop.cpp | |
dplib_prop.h | |
► flattening | |
arrays.cpp | |
arrays.h | Theory of Arrays with Extensionality |
boolbv.cpp | |
boolbv.h | |
boolbv_abs.cpp | |
boolbv_add_sub.cpp | |
boolbv_array.cpp | |
boolbv_array_of.cpp | |
boolbv_bitwise.cpp | |
boolbv_bv_rel.cpp | |
boolbv_byte_extract.cpp | |
boolbv_byte_update.cpp | |
boolbv_case.cpp | |
boolbv_complex.cpp | |
boolbv_concatenation.cpp | |
boolbv_cond.cpp | |
boolbv_constant.cpp | |
boolbv_constraint_select_one.cpp | |
boolbv_div.cpp | |
boolbv_equality.cpp | |
boolbv_extractbit.cpp | |
boolbv_extractbits.cpp | |
boolbv_floatbv_op.cpp | |
boolbv_get.cpp | |
boolbv_ieee_float_rel.cpp | |
boolbv_if.cpp | |
boolbv_index.cpp | |
boolbv_map.cpp | |
boolbv_map.h | |
boolbv_member.cpp | |
boolbv_mod.cpp | |
boolbv_mult.cpp | |
boolbv_not.cpp | |
boolbv_onehot.cpp | |
boolbv_overflow.cpp | |
boolbv_power.cpp | |
boolbv_quantifier.cpp | |
boolbv_reduction.cpp | |
boolbv_replication.cpp | |
boolbv_shift.cpp | |
boolbv_struct.cpp | |
boolbv_type.cpp | |
boolbv_type.h | |
boolbv_typecast.cpp | |
boolbv_unary_minus.cpp | |
boolbv_union.cpp | |
boolbv_update.cpp | |
boolbv_vector.cpp | |
boolbv_width.cpp | |
boolbv_width.h | |
boolbv_with.cpp | |
bv_minimize.cpp | |
bv_minimize.h | SAT-optimizer for minimizing expressions |
bv_pointers.cpp | |
bv_pointers.h | |
bv_utils.cpp | |
bv_utils.h | |
c_bit_field_replacement_type.cpp | |
c_bit_field_replacement_type.h | |
equality.cpp | |
equality.h | |
flatten_byte_operators.cpp | |
flatten_byte_operators.h | |
functions.cpp | |
functions.h | Uninterpreted Functions |
pointer_logic.cpp | Pointer Logic |
pointer_logic.h | Pointer Logic |
► floatbv | |
float_approximation.cpp | |
float_approximation.h | Floating Point with under/over-approximation |
float_bv.cpp | |
float_bv.h | |
float_utils.cpp | |
float_utils.h | |
► miniBDD | |
example.cpp | A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes |
miniBDD.cpp | A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes |
miniBDD.h | A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes |
► prop | |
aig.cpp | |
aig.h | AND-Inverter Graph |
aig_prop.cpp | |
aig_prop.h | |
bdd_expr.cpp | Conversion between exprt and miniBDD |
bdd_expr.h | Conversion between exprt and miniBDD |
cover_goals.cpp | Cover a set of goals incrementally |
cover_goals.h | Cover a set of goals incrementally |
literal.cpp | Literals |
literal.h | |
literal_expr.h | |
minimize.cpp | Minimize some target function incrementally |
minimize.h | SAT Minimizer |
prop.cpp | |
prop.h | |
prop_assignment.cpp | |
prop_assignment.h | |
prop_conv.cpp | |
prop_conv.h | |
prop_conv_store.cpp | |
prop_conv_store.h | |
prop_wrapper.h | |
► qbf | |
qbf_bdd_core.cpp | |
qbf_bdd_core.h | |
qbf_core.h | |
qbf_quantor.cpp | |
qbf_quantor.h | |
qbf_qube.cpp | |
qbf_qube.h | |
qbf_qube_core.cpp | |
qbf_qube_core.h | |
qbf_skizzo.cpp | |
qbf_skizzo.h | |
qbf_skizzo_core.cpp | |
qbf_skizzo_core.h | |
qbf_squolem.cpp | Squolem Backend |
qbf_squolem.h | Squolem Backend |
qbf_squolem_core.cpp | Squolem Backend (with proofs) |
qbf_squolem_core.h | Squolem Backend (with Proofs) |
qdimacs_cnf.cpp | |
qdimacs_cnf.h | |
qdimacs_core.cpp | |
qdimacs_core.h | |
► refinement | |
bv_refinement.h | Abstraction Refinement Loop |
bv_refinement_loop.cpp | |
refine_arithmetic.cpp | |
refine_arrays.cpp | |
refined_string_type.cpp | Type for string expressions used by the string solver |
refined_string_type.h | Type for string expressions used by the string solver |
string_constraint.h | Defines string constraints |
string_constraint_generator.h | Generates string constraints to link results from string functions with their arguments |
string_constraint_generator_code_points.cpp | Generates string constraints for Java functions dealing with code points |
string_constraint_generator_comparison.cpp | Generates string constraints for function comparing strings, such as: equals, equalsIgnoreCase, compareTo, hashCode, intern |
string_constraint_generator_concat.cpp | Generates string constraints for functions adding content add the end of strings |
string_constraint_generator_constants.cpp | Generates string constraints for constant strings |
string_constraint_generator_indexof.cpp | Generates string constraints for the family of indexOf and lastIndexOf java functions |
string_constraint_generator_insert.cpp | Generates string constraints for the family of insert Java functions |
string_constraint_generator_main.cpp | Generates string constraints to link results from string functions with their arguments |
string_constraint_generator_testing.cpp | Generates string constraints for string functions that return Boolean values |
string_constraint_generator_transformation.cpp | Generates string constraints for string transformations, that is, functions taking one string and returning another |
string_constraint_generator_valueof.cpp | Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool |
string_refinement.cpp | String support via creating string constraints and progressively instantiating the universal constraints as needed |
string_refinement.h | String support via creating string constraints and progressively instantiating the universal constraints as needed |
► sat | |
cnf.cpp | CNF Generation, via Tseitin |
cnf.h | CNF Generation, via Tseitin |
cnf_clause_list.cpp | CNF Generation |
cnf_clause_list.h | CNF Generation |
dimacs_cnf.cpp | |
dimacs_cnf.h | |
pbs_dimacs_cnf.cpp | |
pbs_dimacs_cnf.h | |
read_dimacs_cnf.cpp | Reading DIMACS CNF |
read_dimacs_cnf.h | Reading DIMACS CNF |
resolution_proof.cpp | |
resolution_proof.h | |
satcheck.cpp | |
satcheck.h | |
satcheck_booleforce.cpp | |
satcheck_booleforce.h | |
satcheck_core.h | |
satcheck_glucose.cpp | |
satcheck_glucose.h | |
satcheck_limmat.cpp | |
satcheck_limmat.h | |
satcheck_lingeling.cpp | |
satcheck_lingeling.h | |
satcheck_minisat.cpp | |
satcheck_minisat.h | |
satcheck_minisat2.cpp | |
satcheck_minisat2.h | |
satcheck_picosat.cpp | |
satcheck_picosat.h | |
satcheck_precosat.cpp | |
satcheck_precosat.h | |
satcheck_smvsat.cpp | |
satcheck_smvsat.h | |
satcheck_zchaff.cpp | |
satcheck_zchaff.h | |
satcheck_zcore.cpp | |
satcheck_zcore.h | |
► smt1 | |
smt1_conv.cpp | SMT Version 1 Backend |
smt1_conv.h | SMT Version 1 Backend |
smt1_dec.cpp | |
smt1_dec.h | |
smt1_prop.cpp | |
smt1_prop.h | |
► smt2 | |
smt2_conv.cpp | SMT Backend |
smt2_conv.h | |
smt2_dec.cpp | |
smt2_dec.h | |
smt2_parser.cpp | |
smt2_parser.h | |
smt2_prop.cpp | |
smt2_prop.h | |
smt2irep.cpp | |
smt2irep.h | |
► symex | |
path_search.cpp | Path-based Symbolic Execution |
path_search.h | Path-based Symbolic Execution |
symex_cover.cpp | Symex Test Suite Generation |
symex_main.cpp | Symex Main Module |
symex_parse_options.cpp | Symex Command Line Options Processing |
symex_parse_options.h | Command Line Parsing |
► util | |
arith_tools.cpp | |
arith_tools.h | |
array_name.cpp | Misc Utilities |
array_name.h | Misc Utilities |
base_exceptions.h | Generic exception types primarily designed for use with invariants |
base_type.cpp | Base Type Computation |
base_type.h | Base Type Computation |
bv_arithmetic.cpp | |
bv_arithmetic.h | |
byte_operators.cpp | |
byte_operators.h | Expression classes for byte-level operators |
c_types.cpp | |
c_types.h | |
cmdline.cpp | |
cmdline.h | |
config.cpp | |
config.h | |
cout_message.cpp | |
cout_message.h | |
cprover_prefix.h | |
decision_procedure.cpp | Decision Procedure Interface |
decision_procedure.h | Decision Procedure Interface |
dstring.cpp | Container for C-Strings |
dstring.h | Container for C-Strings |
endianness_map.cpp | |
endianness_map.h | |
error.h | |
expanding_vector.h | |
expr.cpp | Expression Representation |
expr.h | |
expr_util.cpp | |
expr_util.h | Deprecated expression utility functions |
file_util.cpp | File Utilities |
file_util.h | |
find_macros.cpp | |
find_macros.h | |
find_symbols.cpp | |
find_symbols.h | |
fixedbv.cpp | |
fixedbv.h | |
format_constant.cpp | |
format_constant.h | |
format_spec.h | |
fresh_symbol.cpp | Fresh auxiliary symbol creation |
fresh_symbol.h | Fresh auxiliary symbol creation |
get_base_name.cpp | |
get_base_name.h | |
get_module.cpp | Find module symbol using name |
get_module.h | Find module symbol using name |
graph.cpp | A Template Class for Graphs |
graph.h | A Template Class for Graphs |
guard.cpp | Symbolic Execution |
guard.h | Guard Data Structure |
identifier.cpp | |
identifier.h | |
ieee_float.cpp | |
ieee_float.h | |
infix.h | String infix shorthand |
invariant.cpp | |
invariant.h | |
irep.cpp | Internal Representation |
irep.h | |
irep_hash.cpp | Irep hash functions |
irep_hash.h | Irep hash functions |
irep_hash_container.cpp | Hashing IREPs |
irep_hash_container.h | IREP Hash Container |
irep_ids.cpp | Internal Representation |
irep_ids.h | Util |
irep_serialization.cpp | Binary irep conversions with hashing |
irep_serialization.h | Binary irep conversions with hashing |
json.cpp | |
json.h | |
json_expr.cpp | Expressions in JSON |
json_expr.h | Expressions in JSON |
json_irep.cpp | Util |
json_irep.h | Util |
language.cpp | Abstract interface to support a programming language |
language.h | Abstract interface to support a programming language |
language_file.cpp | |
language_file.h | |
lispexpr.cpp | |
lispexpr.h | |
lispirep.cpp | |
lispirep.h | |
memory_info.cpp | |
memory_info.h | |
merge_irep.cpp | |
merge_irep.h | |
message.cpp | |
message.h | |
mp_arith.cpp | |
mp_arith.h | |
namespace.cpp | Namespace |
namespace.h | |
numbering.h | |
options.cpp | Options |
options.h | Options |
parse_options.cpp | |
parse_options.h | |
parser.cpp | |
parser.h | Parser utilities |
pipe_stream.cpp | A stdin/stdout pipe as STL stream |
pipe_stream.h | A stdin/stdout pipe as STL stream |
pointer_offset_size.cpp | Pointer Logic |
pointer_offset_size.h | Pointer Logic |
pointer_predicates.cpp | Various predicates over pointers in programs |
pointer_predicates.h | Various predicates over pointers in programs |
prefix.h | |
preprocessor.h | Preprocessing Base Class |
rational.cpp | Rational Numbers |
rational.h | |
rational_tools.cpp | Rational Numbers |
rational_tools.h | |
ref_expr_set.cpp | Value Set |
ref_expr_set.h | Value Set |
reference_counting.h | Reference Counting |
rename.cpp | |
rename.h | |
rename_symbol.cpp | |
rename_symbol.h | |
replace_expr.cpp | |
replace_expr.h | |
replace_symbol.cpp | |
replace_symbol.h | |
run.cpp | |
run.h | |
safe_pointer.h | Simple checked pointers |
sharing_map.h | Sharing map |
sharing_node.h | Sharing node |
signal_catcher.cpp | |
signal_catcher.h | |
simplify_expr.cpp | |
simplify_expr.h | |
simplify_expr_array.cpp | |
simplify_expr_boolean.cpp | |
simplify_expr_class.h | |
simplify_expr_floatbv.cpp | |
simplify_expr_int.cpp | |
simplify_expr_pointer.cpp | |
simplify_expr_struct.cpp | |
simplify_utils.cpp | |
simplify_utils.h | |
sorted_vector.h | |
source_location.cpp | |
source_location.h | |
ssa_expr.cpp | |
ssa_expr.h | |
std_code.cpp | |
std_code.h | |
std_expr.cpp | |
std_expr.h | API to expression classes |
std_types.cpp | |
std_types.h | API to type classes |
string2int.cpp | |
string2int.h | |
string_container.cpp | Container for C-Strings |
string_container.h | Container for C-Strings |
string_expr.h | String expressions for the string solver |
string_hash.cpp | String hashing |
string_hash.h | String hashing |
string_utils.cpp | |
string_utils.h | |
substitute.cpp | |
substitute.h | |
suffix.h | |
symbol.cpp | |
symbol.h | Symbol table entry |
symbol_table.cpp | |
symbol_table.h | Symbol table |
tempdir.cpp | |
tempdir.h | |
tempfile.cpp | |
tempfile.h | |
threeval.cpp | |
threeval.h | |
time_stopping.cpp | Time Stopping |
time_stopping.h | Time Stopping |
timer.cpp | Time Stopping |
timer.h | Time Stopping |
type.cpp | |
type.h | |
type_eq.cpp | Type Checking |
type_eq.h | |
typecheck.cpp | |
typecheck.h | |
ui_message.cpp | |
ui_message.h | |
unicode.cpp | |
unicode.h | |
union_find.cpp | |
union_find.h | |
xml.cpp | |
xml.h | |
xml_expr.cpp | Expressions in XML |
xml_expr.h | |
xml_irep.cpp | |
xml_irep.h | |
► xmllang | |
graphml.cpp | Read/write graphs as GraphML |
graphml.h | Read/write graphs as GraphML |
xml_lex.yy.cpp | |
xml_parse_tree.cpp | |
xml_parse_tree.h | |
xml_parser.cpp | |
xml_parser.h | |
xml_y.tab.cpp | |
xml_y.tab.h | |