cprover
Loading...
Searching...
No Matches
goto-programs Directory Reference
Directory dependency graph for goto-programs:

Files

 
abstract_goto_model.h
 Abstract interface to eager or lazy GOTO models.
 
adjust_float_expressions.cpp
 Symbolic Execution.
 
adjust_float_expressions.h
 Symbolic Execution.
 
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.
 
elf_reader.cpp
 Read ELF.
 
elf_reader.h
 Read ELF.
 
ensure_one_backedge_per_target.cpp
 Ensure one backedge per target.
 
ensure_one_backedge_per_target.h
 Ensure one backedge per target.
 
goto_check.cpp
 GOTO Programs.
 
goto_check.h
 Checks for Errors in C and Java Programs.
 
goto_function.cpp
 Goto Function.
 
goto_function.h
 Goto Function.
 
goto_functions.cpp
 Goto Programs with Functions.
 
goto_functions.h
 Goto Programs with Functions.
 
goto_inline.cpp
 Function Inlining.
 
goto_inline.h
 Function Inlining This gives a number of different interfaces to the function inlining functionality of goto_inlinet.
 
goto_inline_class.cpp
 Function Inlining.
 
goto_inline_class.h
 Function Inlining This is a class that encapsulates the state and functionality needed to do inline multiple function calls.
 
goto_instruction_code.cpp
 Data structures representing instructions in a GOTO program.
 
goto_instruction_code.h
 
goto_model.h
 Symbol Table + CFG.
 
goto_program.cpp
 Program Transformation.
 
goto_program.h
 Concrete Goto Program.
 
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.
 
instrument_preconditions.cpp
 
instrument_preconditions.h
 
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_expr.cpp
 Expressions in JSON.
 
json_expr.h
 Expressions in JSON.
 
json_goto_trace.cpp
 Traces of GOTO Programs.
 
json_goto_trace.h
 Traces of GOTO Programs.
 
label_function_pointer_call_sites.cpp
 Label function pointer call sites across a goto model.
 
label_function_pointer_call_sites.h
 Label function pointer call sites across a goto model.
 
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.
 
name_mangler.cpp
 
name_mangler.h
 Mangle names of file-local functions to make them unique.
 
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
 
process_goto_program.cpp
 Get a Goto Program.
 
process_goto_program.h
 
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.
 
rebuild_goto_start_function.cpp
 Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m.
 
rebuild_goto_start_function.h
 Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m.
 
remove_calls_no_body.cpp
 Remove calls to functions without a body.
 
remove_calls_no_body.h
 Remove calls to functions without a body.
 
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_function_pointers.cpp
 Program Transformation.
 
remove_function_pointers.h
 Remove Indirect Function Calls.
 
remove_returns.cpp
 Replace function returns by assignments to global variables.
 
remove_returns.h
 Replace function returns by assignments to global variables.
 
remove_skip.cpp
 Program Transformation.
 
remove_skip.h
 Program Transformation.
 
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
 Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs.
 
resolve_inherited_component.cpp
 
resolve_inherited_component.h
 Given a class and a component (either field or method), find the closest parent that defines that component.
 
restrict_function_pointers.cpp
 
restrict_function_pointers.h
 Given goto functions and a list of function parameters or globals that are function pointers with lists of possible candidates, replace use of these function pointers with calls to the candidate.
 
rewrite_rw_ok.cpp
 
rewrite_rw_ok.h
 Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.
 
rewrite_union.cpp
 Symbolic Execution of ANSI-C.
 
rewrite_union.h
 Symbolic Execution.
 
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.
 
structured_trace_util.cpp
 Utilities for printing location info steps in the trace in a format agnostic way.
 
structured_trace_util.h
 Utilities for printing location info steps in the trace in a format agnostic way.
 
system_library_symbols.cpp
 Goto Programs.
 
system_library_symbols.h
 Goto Programs.
 
unwindset.cpp
 
unwindset.h
 Loop unwinding.
 
validate_code.cpp
 
validate_code.h
 
validate_goto_model.cpp
 
validate_goto_model.h
 
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_expr.cpp
 Expressions in XML.
 
xml_expr.h
 
xml_goto_trace.cpp
 Traces of GOTO Programs.
 
xml_goto_trace.h
 Traces of GOTO Programs.