CBMC
goto-programs Directory Reference
+ Directory dependency graph for goto-programs:

Files

file  abstract_goto_model.h [code]
 Abstract interface to eager or lazy GOTO models.
 
file  adjust_float_expressions.cpp [code]
 Symbolic Execution.
 
file  adjust_float_expressions.h [code]
 Symbolic Execution.
 
file  cfg.h [code]
 Control Flow Graph.
 
file  class_hierarchy.cpp [code]
 Class Hierarchy.
 
file  class_hierarchy.h [code]
 Class Hierarchy.
 
file  class_identifier.cpp [code]
 Extract class identifier.
 
file  class_identifier.h [code]
 Extract class identifier.
 
file  compute_called_functions.cpp [code]
 Query Called Functions.
 
file  compute_called_functions.h [code]
 Query Called Functions.
 
file  elf_reader.cpp [code]
 Read ELF.
 
file  elf_reader.h [code]
 Read ELF.
 
file  ensure_one_backedge_per_target.cpp [code]
 Ensure one backedge per target.
 
file  ensure_one_backedge_per_target.h [code]
 Ensure one backedge per target.
 
file  goto_check.cpp [code]
 GOTO Programs.
 
file  goto_check.h [code]
 Checks for Errors in C and Java Programs.
 
file  goto_function.cpp [code]
 Goto Function.
 
file  goto_function.h [code]
 Goto Function.
 
file  goto_functions.cpp [code]
 Goto Programs with Functions.
 
file  goto_functions.h [code]
 Goto Programs with Functions.
 
file  goto_inline.cpp [code]
 Function Inlining.
 
file  goto_inline.h [code]
 Function Inlining This gives a number of different interfaces to the function inlining functionality of goto_inlinet.
 
file  goto_inline_class.cpp [code]
 Function Inlining.
 
file  goto_inline_class.h [code]
 Function Inlining This is a class that encapsulates the state and functionality needed to do inline multiple function calls.
 
file  goto_instruction_code.cpp [code]
 Data structures representing instructions in a GOTO program.
 
file  goto_instruction_code.h [code]
 
file  goto_model.h [code]
 Symbol Table + CFG.
 
file  goto_program.cpp [code]
 Program Transformation.
 
file  goto_program.h [code]
 Concrete Goto Program.
 
file  goto_trace.cpp [code]
 Traces of GOTO Programs.
 
file  goto_trace.h [code]
 Traces of GOTO Programs.
 
file  graphml_witness.cpp [code]
 Witnesses for Traces and Proofs.
 
file  graphml_witness.h [code]
 Witnesses for Traces and Proofs.
 
file  initialize_goto_model.cpp [code]
 Get a Goto Program.
 
file  initialize_goto_model.h [code]
 Initialize a Goto Program.
 
file  instrument_preconditions.cpp [code]
 
file  instrument_preconditions.h [code]
 
file  interpreter.cpp [code]
 Interpreter for GOTO Programs.
 
file  interpreter.h [code]
 Interpreter for GOTO Programs.
 
file  interpreter_class.h [code]
 Interpreter for GOTO Programs.
 
file  interpreter_evaluate.cpp [code]
 Interpreter for GOTO Programs.
 
file  json_expr.cpp [code]
 Expressions in JSON.
 
file  json_expr.h [code]
 Expressions in JSON.
 
file  json_goto_trace.cpp [code]
 Traces of GOTO Programs.
 
file  json_goto_trace.h [code]
 Traces of GOTO Programs.
 
file  label_function_pointer_call_sites.cpp [code]
 Label function pointer call sites across a goto model.
 
file  label_function_pointer_call_sites.h [code]
 Label function pointer call sites across a goto model.
 
 
 
file  loop_ids.cpp [code]
 Loop IDs.
 
file  loop_ids.h [code]
 Loop IDs.
 
file  mm_io.cpp [code]
 Perform Memory-mapped I/O instrumentation.
 
file  mm_io.h [code]
 Perform Memory-mapped I/O instrumentation.
 
file  name_mangler.cpp [code]
 
file  name_mangler.h [code]
 Mangle names of file-local functions to make them unique.
 
file  osx_fat_reader.cpp [code]
 Read Mach-O.
 
file  osx_fat_reader.h [code]
 Read OS X Fat Binaries.
 
file  parameter_assignments.cpp [code]
 Add parameter assignments.
 
file  parameter_assignments.h [code]
 Add parameter assignments.
 
file  pointer_arithmetic.cpp [code]
 
file  pointer_arithmetic.h [code]
 
file  process_goto_program.cpp [code]
 Get a Goto Program.
 
file  process_goto_program.h [code]
 
file  read_bin_goto_object.cpp [code]
 Read goto object files.
 
file  read_bin_goto_object.h [code]
 Read goto object files.
 
file  read_goto_binary.cpp [code]
 Read Goto Programs.
 
file  read_goto_binary.h [code]
 Read Goto Programs.
 
file  rebuild_goto_start_function.cpp [code]
 Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m.
 
file  rebuild_goto_start_function.h [code]
 Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m.
 
file  remove_calls_no_body.cpp [code]
 Remove calls to functions without a body.
 
file  remove_calls_no_body.h [code]
 Remove calls to functions without a body.
 
file  remove_complex.cpp [code]
 Remove 'complex' data type.
 
file  remove_complex.h [code]
 Remove the 'complex' data type by compilation into structs.
 
file  remove_const_function_pointers.cpp [code]
 Goto Programs.
 
file  remove_const_function_pointers.h [code]
 Goto Programs.
 
file  remove_function_pointers.cpp [code]
 Program Transformation.
 
file  remove_function_pointers.h [code]
 Remove Indirect Function Calls.
 
file  remove_returns.cpp [code]
 Replace function returns by assignments to global variables.
 
file  remove_returns.h [code]
 Replace function returns by assignments to global variables.
 
file  remove_skip.cpp [code]
 Program Transformation.
 
file  remove_skip.h [code]
 Program Transformation.
 
file  remove_unreachable.cpp [code]
 Program Transformation.
 
file  remove_unreachable.h [code]
 Program Transformation.
 
file  remove_unused_functions.cpp [code]
 Unused function removal.
 
file  remove_unused_functions.h [code]
 Unused function removal.
 
file  remove_vector.cpp [code]
 Remove 'vector' data type.
 
file  remove_vector.h [code]
 Remove the 'vector' data type by compilation into arrays.
 
file  remove_virtual_functions.cpp [code]
 Remove Virtual Function (Method) Calls.
 
file  remove_virtual_functions.h [code]
 Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs.
 
file  resolve_inherited_component.cpp [code]
 
file  resolve_inherited_component.h [code]
 Given a class and a component (either field or method), find the closest parent that defines that component.
 
file  restrict_function_pointers.cpp [code]
 
file  restrict_function_pointers.h [code]
 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.
 
file  rewrite_rw_ok.cpp [code]
 
file  rewrite_rw_ok.h [code]
 Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.
 
file  rewrite_union.cpp [code]
 Symbolic Execution of ANSI-C.
 
file  rewrite_union.h [code]
 Symbolic Execution.
 
file  safety_checker.cpp [code]
 Safety Checker Interface.
 
file  safety_checker.h [code]
 Safety Checker Interface.
 
file  set_properties.cpp [code]
 Set Properties.
 
file  set_properties.h [code]
 Set the properties to check.
 
file  show_goto_functions.cpp [code]
 Show goto functions.
 
file  show_goto_functions.h [code]
 Show the goto functions.
 
file  show_goto_functions_json.cpp [code]
 Goto Program.
 
file  show_goto_functions_json.h [code]
 Goto Program.
 
file  show_goto_functions_xml.cpp [code]
 Goto Program.
 
file  show_goto_functions_xml.h [code]
 Goto Program.
 
file  show_properties.cpp [code]
 Show Claims.
 
file  show_properties.h [code]
 Show the properties.
 
file  show_symbol_table.cpp [code]
 Show the symbol table.
 
file  show_symbol_table.h [code]
 Show the symbol table.
 
file  slice_global_inits.cpp [code]
 Remove initializations of unused global variables.
 
file  slice_global_inits.h [code]
 Remove initializations of unused global variables.
 
file  string_abstraction.cpp [code]
 String Abstraction.
 
file  string_abstraction.h [code]
 String Abstraction.
 
file  structured_trace_util.cpp [code]
 Utilities for printing location info steps in the trace in a format agnostic way.
 
file  structured_trace_util.h [code]
 Utilities for printing location info steps in the trace in a format agnostic way.
 
file  system_library_symbols.cpp [code]
 Goto Programs.
 
file  system_library_symbols.h [code]
 Goto Programs.
 
file  validate_code.cpp [code]
 
file  validate_code.h [code]
 
file  validate_goto_model.cpp [code]
 
file  validate_goto_model.h [code]
 
file  vcd_goto_trace.cpp [code]
 Traces of GOTO Programs in VCD (Value Change Dump) Format.
 
file  vcd_goto_trace.h [code]
 Traces of GOTO Programs in VCD (Value Change Dump) Format.
 
file  wp.cpp [code]
 Weakest Preconditions.
 
file  wp.h [code]
 Weakest Preconditions.
 
file  write_goto_binary.cpp [code]
 Write GOTO binaries.
 
file  write_goto_binary.h [code]
 Write GOTO binaries.
 
file  xml_expr.cpp [code]
 Expressions in XML.
 
file  xml_expr.h [code]
 
file  xml_goto_trace.cpp [code]
 Traces of GOTO Programs.
 
file  xml_goto_trace.h [code]
 Traces of GOTO Programs.