| ► analyses | |
| ► variable-sensitivity | |
| abstract_aggregate_object.h | Common behaviour for abstract objects modelling aggregate values - arrays, structs, etc |
| abstract_environment.cpp | |
| abstract_environment.h | An abstract version of a program environment |
| abstract_object.cpp | |
| abstract_object.h | Abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual variables in the general non-relational domain |
| abstract_object_set.cpp | |
| abstract_object_set.h | Unordered set of value objects |
| abstract_object_statistics.h | Statistics gathering for the variable senstivity domain |
| abstract_pointer_object.cpp | |
| abstract_pointer_object.h | The base of all pointer abstractions |
| abstract_value_object.cpp | |
| abstract_value_object.h | Common behaviour for abstract objects modelling values - constants, intervals, etc |
| constant_abstract_value.cpp | |
| constant_abstract_value.h | An abstraction of a single value that just stores a constant |
| constant_pointer_abstract_object.cpp | |
| constant_pointer_abstract_object.h | An abstraction of a pointer that tracks a single pointer |
| context_abstract_object.cpp | |
| context_abstract_object.h | General implementation of a an abstract_objectt which can track side information in the form of a 'context' associated with a wrapped abstract_objectt of some other type |
| data_dependency_context.cpp | Maintain data dependencies as a context in the variable sensitivity domain |
| data_dependency_context.h | Maintain data dependencies as a context in the variable sensitivity domain |
| full_array_abstract_object.cpp | |
| full_array_abstract_object.h | An abstraction of an array value |
| full_struct_abstract_object.cpp | |
| full_struct_abstract_object.h | An abstraction of a structure that stores one abstract object per field |
| interval_abstract_value.cpp | |
| interval_abstract_value.h | An interval to represent a set of possible values |
| liveness_context.cpp | |
| liveness_context.h | Maintain a context in the variable sensitvity domain that records the liveness region for a given abstract_objectt |
| location_update_visitor.h | |
| map_visit.h | |
| three_way_merge_abstract_interpreter.cpp | An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivity domain's three-way-merge operation on returning from a function call |
| three_way_merge_abstract_interpreter.h | An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivity domain's three-way-merge operation on returning from a function call |
| two_value_array_abstract_object.h | The base type of all abstract array representations |
| two_value_pointer_abstract_object.cpp | |
| two_value_pointer_abstract_object.h | |
| two_value_struct_abstract_object.h | The base of all structure abstractions |
| two_value_union_abstract_object.h | The base of all union abstractions |
| value_set_abstract_object.cpp | Value Set Abstract Object |
| value_set_abstract_object.h | Value Set Abstract Object |
| value_set_pointer_abstract_object.cpp | Value Set of Pointer Abstract Object |
| value_set_pointer_abstract_object.h | Value Set of Pointer Abstract Object |
| variable_sensitivity_configuration.cpp | Captures the user-supplied configuration for VSD, determining which domain abstractions are used, flow sensitivity, etc |
| variable_sensitivity_configuration.h | Captures the user-supplied configuration for VSD, determining which domain abstractions are used, flow sensitivity, etc |
| variable_sensitivity_dependence_graph.cpp | |
| variable_sensitivity_dependence_graph.h | A forked and modified version of analyses/dependence_graph |
| variable_sensitivity_domain.cpp | |
| variable_sensitivity_domain.h | There are different ways of handling arrays, structures, unions and pointers |
| variable_sensitivity_object_factory.cpp | |
| variable_sensitivity_object_factory.h | Tracks the user-supplied configuration for VSD and build the correct type of abstract object when needed |
| widened_range.cpp | |
| widened_range.h | |
| write_location_context.cpp | |
| write_location_context.h | Maintain a context in the variable sensitvity domain that records write locations for a given abstract_objectt |
| write_stack.cpp | Represents a stack of write operations to an addressable memory location |
| write_stack.h | Represents a stack of write operations to an addressable memory location |
| write_stack_entry.cpp | Represents an entry in the write_stackt |
| write_stack_entry.h | Represents an entry in the write_stackt |
| ai.cpp | Abstract Interpretation |
| ai.h | Abstract Interpretation |
| ai_domain.cpp | Abstract Interpretation Domain |
| ai_domain.h | Abstract Interpretation Domain |
| ai_history.cpp | Abstract Interpretation history |
| ai_history.h | Abstract Interpretation history |
| ai_storage.h | Abstract Interpretation Storage |
| call_graph.cpp | Function Call Graphs |
| call_graph.h | Function Call Graphs |
| call_graph_helpers.cpp | Function Call Graph Helpers |
| call_graph_helpers.h | Function Call Graph Helpers |
| call_stack_history.cpp | History for tracking the call stack and performing interprocedural analysis |
| call_stack_history.h | History for tracking the call stack and performing interprocedural analysis |
| 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_rw.cpp | |
| goto_rw.h | |
| guard.h | Guard Data Structure |
| guard_bdd.cpp | Implementation of guards using BDDs |
| guard_bdd.h | Guard Data Structure Implementation using BDDs |
| guard_expr.cpp | Symbolic Execution |
| guard_expr.h | Guard Data Structure |
| interval_analysis.cpp | Interval Analysis – implements the functionality necessary for performing abstract interpretation over interval domain for goto programs |
| interval_analysis.h | Interval Analysis |
| interval_domain.cpp | Interval Domain |
| interval_domain.h | Interval Domain |
| 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 |
| lexical_loops.h | Compute lexical loops in a goto_function |
| 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_control_flow_history.cpp | Track function-local control flow for loop unwinding and path senstivity |
| local_control_flow_history.h | Track function-local control flow for loop unwinding and path senstivity |
| local_may_alias.cpp | Field-insensitive, location-sensitive may-alias analysis |
| local_may_alias.h | Field-insensitive, location-sensitive may-alias analysis |
| local_safe_pointers.cpp | Local safe pointer analysis |
| local_safe_pointers.h | Local safe pointer analysis |
| locals.cpp | Local variables |
| locals.h | Local variables whose address is taken |
| loop_analysis.h | Data structure representing a loop in a GOTO program and an interface shared by all analyses that find program loops |
| 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) |
| sese_regions.cpp | Single-entry, single-exit region analysis |
| sese_regions.h | Single-entry, single-exit region analysis |
| uncaught_exceptions_analysis.cpp | Over-approximating uncaught exceptions analysis |
| uncaught_exceptions_analysis.h | Over-approximative uncaught exceptions analysis |
| uninitialized_domain.cpp | Detection for Uninitialized Local Variables |
| uninitialized_domain.h | Detection for Uninitialized Local Variables |
| ► ansi-c | |
| ► compiler_headers | |
| arm_builtin_headers.h | |
| clang_builtin_headers.h | |
| cw_builtin_headers.h | |
| 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-5.h | |
| gcc_builtin_headers_ia32-6.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_types.h | |
| gcc_builtin_headers_ubsan.h | |
| windows_builtin_headers.h | |
| ► library | |
| converter.cpp | |
| cprover.h | CPROVER built-in declarations to perform library checks |
| cprover_contracts.c | Types and functions for dynamic frames instrumentation in contracts |
| 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_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 |
| builtin_factory.cpp | |
| builtin_factory.h | |
| c_expr.cpp | |
| c_expr.h | API to expression classes that are internal to the C frontend |
| 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_object_factory_parameters.cpp | |
| c_object_factory_parameters.h | |
| c_preprocess.cpp | |
| c_preprocess.h | |
| c_qualifiers.cpp | |
| c_qualifiers.h | |
| c_storage_spec.cpp | |
| c_storage_spec.h | |
| c_typecast.cpp | |
| c_typecast.h | |
| 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_gcc_polymorphic_builtins.cpp | ANSI-C Language Type Checking |
| c_typecheck_initializer.cpp | ANSI-C Conversion / Type Checking |
| c_typecheck_shadow_memory_builtin.cpp | |
| c_typecheck_type.cpp | C++ Language Type Checking |
| c_typecheck_typecast.cpp | |
| cprover_builtin_headers.h | |
| cprover_library.cpp | |
| cprover_library.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_types.cpp | |
| gcc_types.h | |
| gcc_version.cpp | |
| gcc_version.h | |
| goto_check_c.cpp | Checks for Errors in C/C++ Programs |
| goto_check_c.h | Program Transformation |
| merged_type.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 |
| type2name.cpp | Type Naming for C |
| type2name.h | Type Naming for C |
| typedef_type.h | |
| ► assembler | |
| assembler_parser.cpp | |
| assembler_parser.h | |
| remove_asm.cpp | Remove 'asm' statements by compiling them into suitable standard goto program instructions |
| remove_asm.h | Remove 'asm' statements by compiling them into suitable standard goto program instructions |
| ► big-int | |
| allocainc.h | |
| ► cbmc | |
| c_test_input_generator.cpp | Test Input Generator for C |
| c_test_input_generator.h | Test Input Generator for C |
| 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 |
| ► cpp | |
| ► library | |
| cprover.h | |
| 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.cpp | |
| 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 | |
| cprover_library.cpp | |
| cprover_library.h | |
| expr2cpp.cpp | |
| expr2cpp.h | |
| parse.cpp | C++ Language Parsing |
| template_map.cpp | C++ Language Type Checking |
| template_map.h | C++ Language Type Checking |
| ► cprover | |
| address_taken.cpp | Address Taken |
| address_taken.h | Address Taken |
| axioms.cpp | Axioms |
| axioms.h | Axioms |
| bv_pointers_wide.cpp | |
| bv_pointers_wide.h | |
| c_safety_checks.cpp | Checks for Errors in C/C++ Programs |
| c_safety_checks.h | Checks for Errors in C/C++ Programs |
| counterexample_found.cpp | Counterexample Found |
| counterexample_found.h | Counterexample Found |
| cprover_main.cpp | Cprover Main Module |
| cprover_parse_options.cpp | Cprover Command Line Options Processing |
| cprover_parse_options.h | Command Line Parsing |
| endianness_map_wide.cpp | |
| endianness_map_wide.h | |
| equality_propagation.cpp | Equality Propagation |
| equality_propagation.h | Equality Propagation |
| find_variables.cpp | Find Variables |
| find_variables.h | Find Variables |
| flatten_ok_expr.cpp | |
| flatten_ok_expr.h | |
| format_hooks.cpp | |
| format_hooks.h | |
| free_symbols.cpp | |
| free_symbols.h | Free Symbols |
| generalization.cpp | Generalization |
| generalization.h | Generalization |
| inductiveness.cpp | Inductiveness |
| inductiveness.h | Inductiveness |
| instrument_contracts.cpp | Instrument Contracts |
| instrument_contracts.h | Instrument Given Invariants |
| instrument_given_invariants.cpp | Instrument Given Invariants |
| instrument_given_invariants.h | Instrument Given Invariants |
| may_alias.cpp | May Alias |
| may_alias.h | May Alias |
| may_be_same_object.cpp | May Be Same Object |
| may_be_same_object.h | May Be Same Object |
| propagate.cpp | Propagate |
| propagate.h | Propagate |
| report_properties.cpp | Solver |
| report_properties.h | Property Reporting |
| report_traces.cpp | Solver |
| report_traces.h | Report Traces |
| sentinel_dll.cpp | Axioms |
| sentinel_dll.h | |
| simplify_state_expr.cpp | Simplify State Expressions |
| simplify_state_expr.h | Simplify State Expression |
| solver.cpp | Solver |
| solver.h | Equality Propagation |
| solver_progress.cpp | Solver Progress Reporting |
| solver_progress.h | Solver Progress Reporting |
| solver_types.cpp | Solver Types |
| solver_types.h | Solver |
| state.cpp | |
| state.h | |
| state_encoding.cpp | |
| state_encoding.h | State Encoding |
| state_encoding_targets.cpp | |
| state_encoding_targets.h | |
| variable_encoding.cpp | Variable Encoding |
| variable_encoding.h | Variable Encoding |
| ► crangler | |
| c_defines.cpp | C_defines |
| c_defines.h | C_defines |
| c_wrangler.cpp | C Wrangler |
| c_wrangler.h | C Wrangler |
| crangler_main.cpp | CRANGLER Main Module |
| crangler_parse_options.cpp | CRANGLER Command Line Option Processing |
| crangler_parse_options.h | CRANGLER Command Line Option Processing |
| cscanner.cpp | |
| cscanner.h | Cscanner |
| ctoken.cpp | Ctoken |
| ctoken.h | Ctoken |
| ctokenit.cpp | Ctokenit |
| ctokenit.h | Ctokenit |
| mini_c_parser.cpp | Mini C Parser |
| mini_c_parser.h | Mini C Parser |
| ► doc | |
| ADR | |
| ► API | |
| util | |
| architectural | |
| ► assets | |
| driver.h | |
| kdev_t.h | |
| modules.h | |
| doxygen-root | |
| ► goto-analyzer | |
| build_analyzer.cpp | |
| build_analyzer.h | |
| goto_analyzer_languages.cpp | Language Registration |
| 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 |
| show_on_source.cpp | |
| show_on_source.h | |
| static_show_domain.cpp | |
| static_show_domain.h | |
| static_simplifier.cpp | |
| static_simplifier.h | |
| static_verifier.cpp | |
| static_verifier.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-bmc | |
| goto_bmc_main.cpp | |
| goto_bmc_parse_options.cpp | |
| goto_bmc_parse_options.h | |
| ► goto-cc | |
| 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 |
| cl_message_handler.cpp | |
| cl_message_handler.h | |
| 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_message_handler.cpp | |
| gcc_message_handler.h | |
| 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 |
| hybrid_binary.cpp | Create hybrid binary with goto-binary section |
| hybrid_binary.h | Create hybrid binary with goto-binary section |
| 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 |
| ld_mode.cpp | LD Mode |
| ld_mode.h | Base class for command line interpretation |
| linker_script_merge.cpp | |
| linker_script_merge.h | Merge linker script-defined symbols into a goto-program |
| 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 |
| ms_cl_version.cpp | |
| ms_cl_version.h | |
| ms_link_cmdline.cpp | A special command line object for LINK options |
| ms_link_cmdline.h | A special command line object for LINK options |
| ms_link_mode.cpp | Visual Studio Link Mode |
| ms_link_mode.h | Visual Studio Link Mode |
| ► goto-checker | |
| all_properties_verifier.h | Goto Verifier for Verifying all Properties |
| all_properties_verifier_with_fault_localization.h | Goto verifier for verifying all properties that stores traces and localizes faults |
| all_properties_verifier_with_trace_storage.h | Goto verifier for verifying all properties that stores traces |
| bmc_util.cpp | Bounded Model Checking Utilities |
| bmc_util.h | Bounded Model Checking Utilities |
| counterexample_beautification.cpp | Counterexample Beautification using Incremental SAT |
| counterexample_beautification.h | Counterexample Beautification |
| cover_goals_report_util.cpp | Cover Goals Reporting Utilities |
| cover_goals_report_util.h | Cover Goals Reporting Utilities |
| cover_goals_verifier_with_trace_storage.h | Goto verifier for covering goals that stores traces |
| fault_localization_provider.h | Interface for Goto Checkers to provide Fault Localization |
| goto_symex_fault_localizer.cpp | Fault Localization for Goto Symex |
| goto_symex_fault_localizer.h | Fault Localization for Goto Symex |
| goto_symex_property_decider.cpp | Property Decider for Goto-Symex |
| goto_symex_property_decider.h | Property Decider for Goto-Symex |
| goto_trace_provider.h | Interface for returning Goto Traces from Goto Checkers |
| goto_trace_storage.cpp | Goto Trace Storage |
| goto_trace_storage.h | Goto Trace Storage |
| goto_verifier.cpp | Goto Verifier Interface |
| goto_verifier.h | Goto Verifier Interface |
| incremental_goto_checker.cpp | Incremental Goto Checker Interface |
| incremental_goto_checker.h | Incremental Goto Checker Interface |
| multi_path_symex_checker.cpp | Goto Checker using Bounded Model Checking |
| multi_path_symex_checker.h | Goto Checker using Multi-Path Symbolic Execution |
| multi_path_symex_only_checker.cpp | Goto Checker using Multi-Path Symbolic Execution only (no SAT solving) |
| multi_path_symex_only_checker.h | Goto Checker using Multi-Path Symbolic Execution only (no SAT solving) |
| properties.cpp | Properties |
| properties.h | Properties |
| report_util.cpp | Bounded Model Checking Utilities |
| report_util.h | Bounded Model Checking Utilities |
| single_loop_incremental_symex_checker.cpp | Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop |
| single_loop_incremental_symex_checker.h | Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop |
| single_path_symex_checker.cpp | Goto Checker using Single Path Symbolic Execution |
| single_path_symex_checker.h | Goto Checker using Single Path Symbolic Execution |
| single_path_symex_only_checker.cpp | Goto Checker using Single Path Symbolic Execution only |
| single_path_symex_only_checker.h | Goto Checker using Single Path Symbolic Execution only |
| solver_factory.cpp | Solver Factory |
| solver_factory.h | Solver Factory |
| stop_on_fail_verifier.h | Goto Verifier for stopping at the first failing property |
| stop_on_fail_verifier_with_fault_localization.h | Goto Verifier for stopping at the first failing property and localizing the fault |
| symex_bmc.cpp | Bounded Model Checking for ANSI-C |
| symex_bmc.h | Bounded Model Checking for ANSI-C |
| symex_bmc_incremental_one_loop.cpp | |
| symex_bmc_incremental_one_loop.h | |
| symex_coverage.cpp | Record and print code coverage of symbolic execution |
| symex_coverage.h | Record and print code coverage of symbolic execution |
| witness_provider.h | Interface for outputting GraphML Witnesses for Goto Checkers |
| ► 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_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-harness | |
| common_harness_generator_options.h | |
| function_call_harness_generator.cpp | |
| function_call_harness_generator.h | |
| function_harness_generator_options.h | |
| goto_harness_generator.cpp | |
| goto_harness_generator.h | |
| goto_harness_generator_factory.cpp | |
| goto_harness_generator_factory.h | |
| goto_harness_main.cpp | |
| goto_harness_parse_options.cpp | |
| goto_harness_parse_options.h | |
| memory_snapshot_harness_generator.cpp | |
| memory_snapshot_harness_generator.h | |
| memory_snapshot_harness_generator_options.h | |
| recursive_initialization.cpp | |
| recursive_initialization.h | |
| ► goto-inspect | |
| goto_inspect_main.cpp | |
| goto_inspect_parse_options.cpp | |
| goto_inspect_parse_options.h | |
| ► 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 |
| overflow_instrumenter.cpp | Loop Acceleration |
| overflow_instrumenter.h | Loop Acceleration |
| path.cpp | Loop Acceleration |
| path.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 |
| ► contracts | |
| ► doc | |
| developer | |
| user | |
| ► dynamic-frames | |
| dfcc.cpp | |
| dfcc.h | Main class orchestrating the the whole program transformation for function contracts with Dynamic Frame Condition Checking (DFCC) |
| dfcc_cfg_info.cpp | |
| dfcc_cfg_info.h | Class that computes CFG information about the loop structure of a GOTO function for the purpose of dynamic frame conditions checking and loop contract instrumentation |
| dfcc_check_loop_normal_form.cpp | |
| dfcc_check_loop_normal_form.h | Checks normal form properties of natural loops in a GOTO program |
| dfcc_contract_clauses_codegen.cpp | |
| dfcc_contract_clauses_codegen.h | Translates assigns and frees clauses of a function contract or loop contract into goto programs that build write sets or havoc write sets |
| dfcc_contract_functions.cpp | |
| dfcc_contract_functions.h | Translates assigns and frees clauses of a function contract into goto functions that allow to build and havoc write sets dynamically |
| dfcc_contract_handler.cpp | |
| dfcc_contract_handler.h | Specialisation of dfcc_contract_handlert for contracts |
| dfcc_contract_mode.cpp | |
| dfcc_contract_mode.h | Enum type representing the contract checking and replacement modes |
| dfcc_infer_loop_assigns.cpp | |
| dfcc_infer_loop_assigns.h | Infer a set of assigns clause targets for a natural loop |
| dfcc_instrument.cpp | |
| dfcc_instrument.h | Add instrumentation to a goto program to perform frame condition checks |
| dfcc_instrument_loop.cpp | |
| dfcc_instrument_loop.h | This class applies the loop contract transformation to a loop in a goto function |
| dfcc_is_cprover_symbol.cpp | |
| dfcc_is_cprover_symbol.h | |
| dfcc_is_freeable.cpp | |
| dfcc_is_freeable.h | Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses of contracts |
| dfcc_is_fresh.cpp | |
| dfcc_is_fresh.h | Instruments occurrences of is_fresh predicates in programs encoding requires and ensures clauses of contracts |
| dfcc_library.cpp | |
| dfcc_library.h | Dynamic frame condition checking library loading |
| dfcc_lift_memory_predicates.cpp | |
| dfcc_lift_memory_predicates.h | Collects all user-defined predicates that call functions is_fresh, pointer_in_range, obeys_contract and lifts them to function taking pointers by reference |
| dfcc_loop_contract_mode.cpp | |
| dfcc_loop_contract_mode.h | Enumeration representing the instrumentation mode for loop contracts |
| dfcc_loop_nesting_graph.cpp | |
| dfcc_loop_nesting_graph.h | Builds a graph describing how loops are nested in a GOTO program |
| dfcc_loop_tags.cpp | |
| dfcc_loop_tags.h | Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head, body, exiting, latch |
| dfcc_obeys_contract.cpp | |
| dfcc_obeys_contract.h | Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clauses of contracts |
| dfcc_pointer_in_range.cpp | |
| dfcc_pointer_in_range.h | Instruments occurrences of pointer_in_range predicates in programs encoding requires and ensures clauses of contracts |
| dfcc_root_object.cpp | |
| dfcc_root_object.h | Utility functions that compute root object expressions for assigns clause targets and LHS expressions |
| dfcc_spec_functions.cpp | |
| dfcc_spec_functions.h | Translate functions that specify assignable and freeable targets declaratively into active functions that build write sets dynamically by rewriting calls to front-end functions into calls to library functions defining their dynamic semantics |
| dfcc_swap_and_wrap.cpp | |
| dfcc_swap_and_wrap.h | Given a function_id and contract_id, swaps its body to a function with a fresh mangled name, instruments it for dynamic frame condition checking, and replaces the original function's body with instructions encoding contract checking against the mangled function, or contract replacement |
| dfcc_utils.cpp | |
| dfcc_utils.h | Dynamic frame condition checking utility functions |
| dfcc_wrapper_program.cpp | |
| dfcc_wrapper_program.h | Generates the body of a wrapper function from a contract for contract checking or contract replacement |
| cfg_info.h | Classes providing CFG-based information about symbols to guide simplifications in function and loop assigns clause checking |
| contracts.cpp | Verify and use annotated loop and function contracts |
| contracts.h | Verify and use annotated invariants and pre/post-conditions |
| contracts_wrangler.cpp | Parse and annotate contracts |
| contracts_wrangler.h | Parse and annotate contracts |
| havoc_assigns_clause_targets.cpp | Havoc multiple and possibly dependent targets simultaneously |
| havoc_assigns_clause_targets.h | Havoc function assigns clauses |
| inlining_decorator.cpp | |
| inlining_decorator.h | |
| instrument_spec_assigns.cpp | Specify write set in code contracts |
| instrument_spec_assigns.h | Specify write set in function contracts |
| memory_predicates.cpp | Predicates to specify memory footprint in function contracts |
| memory_predicates.h | Predicates to specify memory footprint in function contracts |
| utils.cpp | |
| utils.h | |
| ► 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 |
| aggressive_slicer.cpp | Aggressive program slicer |
| aggressive_slicer.h | Aggressive slicer Consider the control flow graph of the goto program and a criterion description of aggressive slicer here |
| 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 |
| 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 |
| cover_basic_blocks.cpp | Basic blocks detection for Coverage Instrumentation |
| cover_basic_blocks.h | Basic blocks detection for Coverage Instrumentation |
| cover_filter.cpp | Filters for the Coverage Instrumentation |
| cover_filter.h | Filters for the Coverage Instrumentation |
| cover_instrument.h | Coverage Instrumentation |
| cover_instrument_assume.cpp | Author: Diffblue Ltd |
| cover_instrument_branch.cpp | Coverage Instrumentation for Branches |
| cover_instrument_condition.cpp | Coverage Instrumentation for Conditions |
| cover_instrument_decision.cpp | Coverage Instrumentation for Decisions |
| cover_instrument_location.cpp | Coverage Instrumentation for Location, i.e |
| cover_instrument_mcdc.cpp | Coverage Instrumentation for MC/DC |
| cover_instrument_other.cpp | Further coverage instrumentations |
| cover_util.cpp | Coverage Instrumentation Utilities |
| cover_util.h | Coverage Instrumentation Utilities |
| 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_assigns.cpp | Compute objects assigned to in a function |
| function_assigns.h | Compute objects assigned to in a function |
| generate_function_bodies.cpp | |
| generate_function_bodies.h | |
| 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 |
| havoc_utils.cpp | Utilities for building havoc code for expressions |
| havoc_utils.h | Utilities for building havoc code for expressions |
| horn_encoding.cpp | Horn-clause Encoding |
| horn_encoding.h | Horn-clause Encoding |
| insert_final_assert_false.cpp | Insert final assert false into a function |
| insert_final_assert_false.h | Insert final assert false into a function |
| 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 | Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal variables) |
| nondet_static.h | Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal 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 | Reachability Slicer Consider the control flow graph of the goto program and a criterion, and remove the parts of the graph from which the criterion is not reachable (and possibly, depending on the parameters, keep those that can be reached from the criterion) |
| reachability_slicer.h | Slicing |
| reachability_slicer_class.h | Goto Program Slicing |
| remove_function.cpp | Remove function definition |
| remove_function.h | Remove function definition |
| replace_calls.cpp | Replace calls Replaces calls to given functions with calls to other given functions |
| replace_calls.h | Replace calls to given functions with calls to other given functions |
| 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 |
| source_lines.cpp | Set of source code lines contributing to a basic block |
| source_lines.h | Set of source code lines contributing to a basic block |
| splice_call.cpp | Prepend a nullary call to another function useful for context/ environment setting in arbitrary nodes |
| splice_call.h | Harnessing for goto functions |
| 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 |
| unwindset.cpp | |
| unwindset.h | Loop unwinding |
| value_set_fi_fp_removal.cpp | |
| value_set_fi_fp_removal.h | Flow insensitive value set function pointer removal |
| ► goto-programs | |
| abstract_goto_model.h | Abstract interface to eager or lazy GOTO models |
| adjust_float_expressions.cpp | Symbolic Execution |
| adjust_float_expressions.h | Symbolic Execution |
| allocate_objects.cpp | |
| allocate_objects.h | |
| 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 |
| destructor_tree.cpp | |
| destructor_tree.h | |
| 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 |
| format_strings.cpp | Format String Parser |
| format_strings.h | Format String Parser |
| goto_asm.cpp | Assembler -> Goto |
| goto_check.cpp | GOTO Programs |
| goto_check.h | Checks for Errors in C and Java Programs |
| 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_side_effect.cpp | Program Transformation |
| 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 |
| link_goto_model.cpp | Link Goto Programs |
| link_goto_model.h | Read 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 |
| 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 | |
| printf_formatter.cpp | Printf Formatting |
| printf_formatter.h | Printf Formatting |
| 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 |
| string_instrumentation.cpp | String Abstraction |
| string_instrumentation.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 |
| 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 |
| ► goto-symex | |
| auto_objects.cpp | Symbolic Execution of ANSI-C |
| build_goto_trace.cpp | Traces of GOTO Programs |
| build_goto_trace.h | Traces of GOTO Programs |
| call_stack.h | |
| complexity_limiter.cpp | |
| complexity_limiter.h | Symbolic Execution |
| complexity_violation.h | |
| expr_skeleton.cpp | Expression skeleton |
| expr_skeleton.h | Expression skeleton |
| field_sensitivity.cpp | |
| field_sensitivity.h | |
| frame.h | Class for stack frames |
| goto_state.cpp | |
| goto_state.h | Goto_statet class definition |
| goto_symex.cpp | Symbolic Execution |
| goto_symex.h | Symbolic Execution |
| goto_symex_can_forward_propagate.h | GOTO Symex constant propagation |
| 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 |
| path_storage.cpp | |
| path_storage.h | Storage of symbolic execution paths to resume |
| postcondition.cpp | Symbolic Execution |
| postcondition.h | Generate Equation using Symbolic Execution |
| precondition.cpp | Symbolic Execution |
| precondition.h | Generate Equation using Symbolic Execution |
| renamed.h | Class for expressions or types renamed up to a given level |
| renaming_level.cpp | Renaming levels |
| renaming_level.h | Renaming levels |
| shadow_memory.cpp | Symex Shadow Memory Instrumentation |
| shadow_memory.h | Symex Shadow Memory Instrumentation |
| shadow_memory_field_definitions.h | Symex Shadow Memory Field Definitions |
| shadow_memory_state.h | Symex Shadow Memory Instrumentation State |
| shadow_memory_util.cpp | Symex Shadow Memory Instrumentation Utilities |
| shadow_memory_util.h | Symex Shadow Memory Instrumentation Utilities |
| show_program.cpp | Output of the program (SSA) constraints |
| show_program.h | Output of the program (SSA) constraints |
| show_vcc.cpp | Output of the verification conditions (VCCs) |
| show_vcc.h | Output of the verification conditions (VCCs) |
| slice.cpp | Slicer for symex traces |
| slice.h | Slicer for symex traces |
| solver_hardness.cpp | |
| solver_hardness.h | |
| ssa_step.cpp | |
| ssa_step.h | |
| symex_assign.cpp | Symbolic Execution |
| symex_assign.h | Symbolic Execution of assignments |
| 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_complexity_limit_exceeded_action.h | |
| symex_config.h | Symbolic Execution |
| 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_set_return_value.cpp | Symbolic Execution of ANSI-C |
| 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 Implementation of functions to build SSA equation |
| symex_target_equation.h | Generate Equation using Symbolic Execution |
| symex_throw.cpp | Symbolic Execution |
| ► goto-synthesizer | |
| cegis_verifier.cpp | Verifier for Counterexample-Guided Synthesis |
| cegis_verifier.h | Verifier for Counterexample-Guided Synthesis |
| dump_loop_contracts.cpp | Dump Loop Contracts as JSON |
| dump_loop_contracts.h | Dump Loop Contracts as JSON |
| enumerative_loop_contracts_synthesizer.cpp | Enumerative Loop Contracts Synthesizer |
| enumerative_loop_contracts_synthesizer.h | Enumerative Loop Contracts Synthesizer |
| expr_enumerator.cpp | |
| expr_enumerator.h | Enumerator Interface |
| goto_synthesizer_languages.cpp | Language Registration |
| goto_synthesizer_main.cpp | Main Module |
| goto_synthesizer_parse_options.cpp | Main Module |
| goto_synthesizer_parse_options.h | Command Line Parsing |
| loop_contracts_synthesizer_base.h | Loop Contracts Synthesizer Interface |
| synthesizer_utils.cpp | |
| synthesizer_utils.h | |
| ► jbmc | |
| ► src | |
| ► janalyzer | |
| janalyzer_main.cpp | JANALYZER Main Module |
| janalyzer_parse_options.cpp | JANALYZER Command Line Option Processing |
| janalyzer_parse_options.h | JANALYZER Command Line Option Processing |
| ► java_bytecode | |
| assignments_from_json.cpp | |
| assignments_from_json.h | |
| 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 | |
| ci_lazy_methods.h | Collect methods needed to be loaded using the lazy method |
| ci_lazy_methods_needed.cpp | Context-insensitive lazy methods container |
| ci_lazy_methods_needed.h | Context-insensitive lazy methods container |
| code_with_references.cpp | |
| code_with_references.h | |
| convert_java_nondet.cpp | Convert side_effect_expr_nondett expressions |
| convert_java_nondet.h | Convert side_effect_expr_nondett expressions using java_object_factory |
| create_array_with_type_intrinsic.cpp | Implementation of CProver.createArrayWithType intrinsic |
| create_array_with_type_intrinsic.h | Implementation of CProver.createArrayWithType intrinsic |
| expr2java.cpp | |
| expr2java.h | |
| generic_parameter_specialization_map.cpp | |
| generic_parameter_specialization_map.h | |
| generic_parameter_specialization_map_keys.cpp | |
| generic_parameter_specialization_map_keys.h | Author: Diffblue Ltd |
| jar_file.cpp | |
| jar_file.h | |
| jar_pool.cpp | |
| jar_pool.h | |
| java_bmc_util.cpp | Bounded Model Checking Utils for Java |
| java_bmc_util.h | Bounded Model Checking Utils for Java |
| java_bytecode_concurrency_instrumentation.cpp | |
| java_bytecode_concurrency_instrumentation.h | |
| 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_instrument.cpp | |
| java_bytecode_instrument.h | |
| 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_class_loader.cpp | |
| java_class_loader.h | |
| java_class_loader_base.cpp | |
| java_class_loader_base.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_enum_static_init_unwind_handler.cpp | Unwind loops in static initializers |
| java_enum_static_init_unwind_handler.h | Unwind loops in static initializers |
| java_expr.h | Java-specific exprt subclasses |
| java_local_variable_table.cpp | Java local variable table processing |
| java_multi_path_symex_checker.cpp | |
| java_multi_path_symex_checker.h | Goto Checker using Bounded Model Checking for Java |
| java_multi_path_symex_only_checker.h | Goto Checker using Bounded Model Checking for Java |
| java_object_factory.cpp | |
| java_object_factory.h | This module is responsible for the synthesis of code (in the form of a sequence of codet statements) that can allocate and initialize non-deterministically both primitive Java types and objects |
| java_object_factory_parameters.cpp | |
| java_object_factory_parameters.h | |
| java_pointer_casts.cpp | JAVA Pointer Casts |
| java_pointer_casts.h | JAVA Pointer Casts |
| java_qualifiers.cpp | Java-specific type qualifiers |
| java_qualifiers.h | Java-specific type qualifiers |
| java_root_class.cpp | |
| java_root_class.h | |
| java_single_path_symex_checker.cpp | |
| java_single_path_symex_checker.h | Goto Checker using Single Path Symbolic Execution for Java |
| java_single_path_symex_only_checker.h | Goto Checker using Single Path Symbolic Execution for Java |
| java_static_initializers.cpp | |
| java_static_initializers.h | |
| java_string_library_preprocess.cpp | Java_string_libraries_preprocess, gives code for methods on strings of the java standard library |
| java_string_library_preprocess.h | Produce code for simple implementation of String Java libraries |
| java_string_literal_expr.h | Representation of a constant Java string |
| java_string_literals.cpp | |
| java_string_literals.h | |
| java_trace_validation.cpp | |
| java_trace_validation.h | |
| java_types.cpp | |
| java_types.h | |
| java_utils.cpp | |
| java_utils.h | |
| lambda_synthesis.cpp | Java lambda code synthesis |
| lambda_synthesis.h | Java lambda code synthesis |
| lazy_goto_functions_map.h | Author: Diffblue Ltd |
| lazy_goto_model.cpp | Author: Diffblue Ltd |
| lazy_goto_model.h | Author: Diffblue Ltd |
| lift_clinit_calls.cpp | |
| lift_clinit_calls.h | |
| load_method_by_regex.cpp | |
| load_method_by_regex.h | Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst |
| mz_zip_archive.cpp | |
| mz_zip_archive.h | |
| nondet.cpp | |
| nondet.h | |
| pattern.h | Pattern matching for bytecode instructions |
| remove_exceptions.cpp | Remove exception handling |
| remove_exceptions.h | Remove function exceptional returns |
| remove_instanceof.cpp | Remove Instance-of Operators |
| remove_instanceof.h | Remove Instance-of Operators |
| remove_java_new.cpp | Remove Java New Operators |
| remove_java_new.h | Remove Java New Operators |
| replace_java_nondet.cpp | Replace Java Nondet expressions |
| replace_java_nondet.h | Replace Java Nondet expressions |
| select_pointer_type.cpp | Handle selection of correct pointer type (for example changing abstract classes to concrete versions) |
| select_pointer_type.h | Handle selection of correct pointer type (for example changing abstract classes to concrete versions) |
| simple_method_stubbing.cpp | Java simple opaque stub generation |
| simple_method_stubbing.h | Java simple opaque stub generation |
| synthetic_methods_map.h | Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types |
| ► jbmc | |
| jbmc_main.cpp | CBMC Main Module |
| jbmc_parse_options.cpp | JBMC Command Line Option Processing |
| jbmc_parse_options.h | JBMC Command Line Option Processing |
| ► jdiff | |
| java_syntactic_diff.cpp | Syntactic GOTO-DIFF for Java |
| java_syntactic_diff.h | Syntactic GOTO-DIFF for Java |
| jdiff_languages.cpp | Language Registration |
| jdiff_main.cpp | JDIFF Main Module |
| jdiff_parse_options.cpp | JDIFF Command Line Option Processing |
| jdiff_parse_options.h | JDIFF Command Line Option Processing |
| ► miniz | |
| miniz.cpp | |
| miniz.h | |
| ► unit | |
| ► java-testing-utils | |
| load_java_class.cpp | |
| load_java_class.h | Utility for loading and parsing a specified java class file, returning the symbol table generated by this |
| require_goto_statements.cpp | |
| require_goto_statements.h | Utilties for inspecting goto functions |
| require_parse_tree.cpp | |
| require_parse_tree.h | Utilties for inspecting java_parse_treet |
| require_type.cpp | |
| require_type.h | Helper functions for requiring specific types If the type is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression |
| ► 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_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 |
| ► json | |
| json_interface.cpp | JSON Commandline Interface |
| json_interface.h | JSON Commandline Interface |
| json_parser.cpp | |
| json_parser.h | |
| ► json-symtab-language | |
| json_symbol.cpp | |
| json_symbol.h | |
| json_symbol_table.cpp | |
| json_symbol_table.h | |
| json_symtab_language.cpp | |
| json_symtab_language.h | |
| ► langapi | |
| language.cpp | Abstract interface to support a programming language |
| language.h | Abstract interface to support a programming language |
| language_file.cpp | |
| language_file.h | |
| language_util.cpp | |
| language_util.h | |
| mode.cpp | |
| mode.h | |
| ► libcprover-cpp | |
| api.cpp | |
| api.h | |
| api_options.cpp | |
| api_options.h | |
| verification_result.cpp | Interface for the various verification engines providing results |
| verification_result.h | Interface for the various verification engines providing results |
| ► libcprover-rust | |
| ► include | |
| c_api.h | |
| c_errors.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 | |
| ► memory-analyzer | |
| analyze_symbol.cpp | |
| analyze_symbol.h | High-level interface to gdb |
| gdb_api.cpp | Low-level interface to gdb |
| gdb_api.h | Low-level interface to gdb |
| memory_analyzer_main.cpp | Memory analyzer interface |
| memory_analyzer_parse_options.cpp | Commandline parser for the memory analyzer executing main work |
| memory_analyzer_parse_options.h | This code does the command line parsing for the memory-analyzer tool |
| nonstd | |
| ► pointer-analysis | |
| add_failed_symbols.cpp | Pointer Dereferencing |
| add_failed_symbols.h | 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 | Object Numbering |
| 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_dereference.cpp | Symbolic Execution of ANSI-C |
| value_set_dereference.h | Pointer Dereferencing |
| 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_fi.cpp | Value Set (Flow Insensitive, Sharing) |
| value_set_fi.h | Value Set (Flow Insensitive, Sharing) |
| value_sets.h | Value Set Propagation |
| ► solvers | |
| ► bdd | |
| ► 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 |
| bdd.h | Choice between the different interface to BDD libraries |
| bdd_cudd.h | Interface to Cudd BDD functions that are used in CBMC BDD functions should only be accessed through this header file |
| bdd_miniBDD.h | Interface to miniBDD functions that are used in CBMC BDD functions should only be accessed through this header file |
| ► 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_bitreverse.cpp | |
| boolbv_bitwise.cpp | |
| boolbv_bswap.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_mod_rem.cpp | |
| boolbv_floatbv_op.cpp | |
| boolbv_get.cpp | |
| boolbv_ieee_float_rel.cpp | |
| boolbv_if.cpp | |
| boolbv_index.cpp | |
| boolbv_let.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_width.cpp | |
| boolbv_width.h | |
| boolbv_with.cpp | |
| bv_dimacs.cpp | Writing DIMACS Files |
| bv_dimacs.h | Writing DIMACS Files |
| 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 | |
| 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 | |
| ► lowering | |
| functions.cpp | |
| functions.h | Uninterpreted Functions |
| ► prop | |
| 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 | |
| prop.cpp | |
| prop.h | |
| prop_conv.cpp | |
| prop_conv.h | |
| prop_conv_solver.cpp | |
| prop_conv_solver.h | |
| prop_minimize.cpp | Minimize some target function incrementally |
| prop_minimize.h | SAT Minimizer |
| solver_resource_limits.h | Solver capability to set resource limits |
| ► 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 | |
| ► 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 | |
| external_sat.cpp | Allows call an external SAT solver to allow faster integration of newer SAT solvers |
| external_sat.h | Allows calling an external SAT solver to allow faster integration of newer SAT solvers |
| pbs_dimacs_cnf.cpp | |
| pbs_dimacs_cnf.h | |
| resolution_proof.cpp | |
| resolution_proof.h | |
| satcheck.h | |
| satcheck_booleforce.cpp | |
| satcheck_booleforce.h | |
| satcheck_cadical.cpp | |
| satcheck_cadical.h | |
| satcheck_core.h | |
| satcheck_glucose.cpp | |
| satcheck_glucose.h | |
| satcheck_ipasir.cpp | |
| satcheck_ipasir.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_zchaff.cpp | |
| satcheck_zchaff.h | |
| satcheck_zcore.cpp | |
| satcheck_zcore.h | |
| ► smt2 | |
| letify.cpp | Introduce LET for common subexpressions |
| letify.h | |
| smt2_conv.cpp | SMT Backend |
| smt2_conv.h | |
| smt2_dec.cpp | |
| smt2_dec.h | |
| smt2_format.cpp | |
| smt2_format.h | |
| smt2_parser.cpp | |
| smt2_parser.h | |
| smt2_solver.cpp | |
| smt2_tokenizer.cpp | |
| smt2_tokenizer.h | |
| smt2irep.cpp | |
| smt2irep.h | |
| ► smt2_incremental | |
| ► ast | |
| smt_commands.cpp | |
| smt_commands.h | |
| smt_index.cpp | |
| smt_index.h | |
| smt_logics.cpp | |
| smt_logics.h | |
| smt_options.cpp | |
| smt_options.h | |
| smt_responses.cpp | |
| smt_responses.h | |
| smt_sorts.cpp | |
| smt_sorts.h | Data structure for smt sorts |
| smt_terms.cpp | |
| smt_terms.h | |
| ► encoding | |
| enum_encoding.cpp | |
| enum_encoding.h | |
| nondet_padding.cpp | |
| nondet_padding.h | Expressions for use in incremental SMT2 decision procedure |
| struct_encoding.cpp | |
| struct_encoding.h | |
| ► theories | |
| smt_array_theory.cpp | |
| smt_array_theory.h | |
| smt_bit_vector_theory.cpp | |
| smt_bit_vector_theory.h | |
| smt_core_theory.cpp | |
| smt_core_theory.h | |
| construct_value_expr_from_smt.cpp | |
| construct_value_expr_from_smt.h | |
| convert_expr_to_smt.cpp | |
| convert_expr_to_smt.h | |
| object_tracking.cpp | |
| object_tracking.h | Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the objects which pointers point to |
| response_or_error.h | |
| smt2_incremental_decision_procedure.cpp | |
| smt2_incremental_decision_procedure.h | Decision procedure with incremental SMT2 solving |
| smt_is_dynamic_object.cpp | |
| smt_is_dynamic_object.h | |
| smt_object_size.cpp | |
| smt_object_size.h | |
| smt_response_validation.cpp | Validation of smt response parse trees to produce either a strongly typed smt_responset representation, or a set of error messages |
| smt_response_validation.h | |
| smt_solver_process.cpp | |
| smt_solver_process.h | |
| smt_to_smt2_string.cpp | |
| smt_to_smt2_string.h | Streaming SMT data structures to a string based output stream |
| type_size_mapping.cpp | |
| type_size_mapping.h | Utilities for making a map of types to associated sizes |
| type_traits.h | Back ports of utilities available in the <type_traits> library for C++14 or C++17 to C++11 |
| ► strings | |
| array_pool.cpp | |
| array_pool.h | Associates arrays and length to pointers, so that the string refinement can transform builtin function calls with pointer arguments to formulas over arrays |
| equation_symbol_mapping.cpp | |
| equation_symbol_mapping.h | |
| format_specifier.cpp | Format specifiers for String.format |
| format_specifier.h | Format specifiers for String.format |
| string_builtin_function.cpp | |
| string_builtin_function.h | |
| string_concatenation_builtin_function.cpp | Builtin functions for string concatenations |
| string_concatenation_builtin_function.h | Builtin functions for string concatenations |
| string_constraint.cpp | |
| 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_constants.cpp | Generates string constraints for constant strings |
| string_constraint_generator_float.cpp | Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool |
| string_constraint_generator_indexof.cpp | Generates string constraints for the family of indexOf and lastIndexOf 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_constraint_instantiation.cpp | Defines related function for string constraints |
| string_constraint_instantiation.h | Defines related function for string constraints |
| string_dependencies.cpp | |
| string_dependencies.h | Keeps track of dependencies between strings |
| string_format_builtin_function.cpp | Built-in function for String.format |
| string_format_builtin_function.h | Built-in function for String.format |
| string_insertion_builtin_function.cpp | |
| string_insertion_builtin_function.h | |
| 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 |
| string_refinement_invariant.h | |
| string_refinement_util.cpp | |
| string_refinement_util.h | |
| conflict_provider.h | Capability to check whether an expression is a reason for the solver returning UNSAT |
| decision_procedure.cpp | Decision Procedure Interface |
| decision_procedure.h | Decision Procedure Interface |
| hardness_collector.h | Capability to collect the statistics of the complexity of individual solver queries |
| stack_decision_procedure.h | Decision procedure with incremental solving with contexts and assumptions |
| ► statement-list | |
| ► converters | |
| convert_bool_literal.cpp | Statement List Language Conversion |
| convert_bool_literal.h | Statement List Language Conversion |
| convert_dint_literal.cpp | Statement List Language Conversion |
| convert_dint_literal.h | Statement List Language Conversion |
| convert_int_literal.cpp | Statement List Language Conversion |
| convert_int_literal.h | Statement List Language Conversion |
| convert_real_literal.cpp | Statement List Language Conversion |
| convert_real_literal.h | Statement List Language Conversion |
| convert_string_value.cpp | Statement List Language Conversion |
| convert_string_value.h | Statement List Language Conversion |
| expr2statement_list.cpp | |
| expr2statement_list.h | |
| statement_list_types.cpp | Statement List Type Helper |
| statement_list_types.h | Statement List Type Helper |
| statement_list_entry_point.cpp | Statement List Language Entry Point |
| statement_list_entry_point.h | Statement List Language Entry Point |
| statement_list_language.cpp | Statement List Language Interface |
| statement_list_language.h | Statement List Language Interface |
| statement_list_parse_tree.cpp | Statement List Language Parse Tree |
| statement_list_parse_tree.h | Statement List Language Parse Tree |
| statement_list_parse_tree_io.cpp | Statement List Language Parse Tree Output |
| statement_list_parse_tree_io.h | Statement List Language Parse Tree Output |
| statement_list_parser.cpp | Statement List Language Parser |
| statement_list_parser.h | Statement List Language Parser |
| statement_list_typecheck.cpp | Statement List Language Type Checking |
| statement_list_typecheck.h | Statement List Language Type Checking |
| ► symtab2gb | |
| symtab2gb_main.cpp | Symtab2gb Main Module |
| symtab2gb_parse_options.cpp | |
| symtab2gb_parse_options.h | |
| ► unit | |
| ► testing-utils | |
| call_graph_test_utils.cpp | |
| call_graph_test_utils.h | |
| expr_query.h | Helper class for querying expressions Throw CATCH exceptions when the query fails |
| free_form_cmdline.cpp | |
| free_form_cmdline.h | |
| get_goto_model_from_c.cpp | |
| get_goto_model_from_c.h | |
| invariant.cpp | |
| invariant.h | |
| message.cpp | Global instance of null_message_handlert |
| message.h | |
| require_expr.cpp | Helper functions for requiring specific expressions If the expression is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression |
| require_expr.h | Helper functions for requiring specific expressions If the expression is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression |
| require_symbol.cpp | |
| require_symbol.h | Helper functions for getting symbols from the symbol table during unit tests |
| require_vectors_equal_unordered.h | |
| run_test_with_compilers.cpp | |
| run_test_with_compilers.h | Utility for running a test with different compilers |
| smt2irep.cpp | |
| smt2irep.h | |
| use_catch.h | |
| ► util | |
| arith_tools.cpp | |
| arith_tools.h | |
| array_element_from_pointer.cpp | |
| array_element_from_pointer.h | |
| array_name.cpp | Misc Utilities |
| array_name.h | Misc Utilities |
| as_const.h | |
| base_exceptions.h | Generic exception types primarily designed for use with invariants |
| bitvector_expr.cpp | |
| bitvector_expr.h | API to expression classes for bitvectors |
| bitvector_types.cpp | Pre-defined bitvector types |
| bitvector_types.h | Pre-defined bitvector types |
| bv_arithmetic.cpp | |
| bv_arithmetic.h | |
| byte_operators.cpp | |
| byte_operators.h | Expression classes for byte-level operators |
| c_types.cpp | |
| c_types.h | |
| c_types_util.h | This file contains functions, that should support test for underlying c types, in cases where this is required for analysis purpose |
| cmdline.cpp | |
| cmdline.h | |
| config.cpp | |
| config.h | |
| console.cpp | |
| console.h | Console |
| constructor_of.h | |
| container_utils.h | |
| cout_message.cpp | |
| cout_message.h | |
| cow.h | |
| cprover_prefix.h | |
| dense_integer_map.h | Dense integer map |
| deprecate.h | |
| dstring.cpp | Container for C-Strings |
| dstring.h | Container for C-Strings |
| edit_distance.cpp | |
| edit_distance.h | |
| endianness_map.cpp | |
| endianness_map.h | |
| exception_utils.cpp | |
| exception_utils.h | |
| exit_codes.h | Document and give macros for the exit codes of CPROVER binaries |
| expanding_vector.h | |
| expr.cpp | Expression Representation |
| expr.h | |
| expr_cast.h | Templated functions to cast to specific exprt-derived classes |
| expr_initializer.cpp | Expression Initialization |
| expr_initializer.h | Expression Initialization |
| expr_iterator.h | Forward depth-first search iterators These iterators' copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator |
| 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 | |
| fixed_keys_map_wrapper.h | A wrapper for maps that gives read-write access to elements but without allowing addition or removal of elements |
| fixedbv.cpp | |
| fixedbv.h | |
| floatbv_expr.cpp | |
| floatbv_expr.h | API to expression classes for floating-point arithmetic |
| format.h | |
| format_constant.cpp | |
| format_constant.h | |
| format_expr.cpp | Expression Pretty Printing |
| format_expr.h | |
| format_number_range.cpp | Format vector of numbers into a compressed range |
| format_number_range.h | Format vector of numbers into a compressed range |
| format_spec.h | |
| format_type.cpp | |
| format_type.h | |
| forward_list_as_map.h | |
| freer.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.h | A Template Class for Graphs |
| help_formatter.cpp | |
| help_formatter.h | Help Formatter |
| identifier.cpp | |
| identifier.h | |
| ieee_float.cpp | |
| ieee_float.h | |
| infix.h | String infix shorthand |
| integer_interval.h | |
| interval.cpp | |
| interval.h | |
| interval_constraint.cpp | |
| interval_constraint.h | |
| interval_template.h | |
| interval_union.cpp | |
| interval_union.h | Union of intervals |
| invariant.cpp | |
| invariant.h | |
| invariant_utils.cpp | Invariant helper utilities |
| invariant_utils.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 |
| journalling_symbol_table.h | Author: Diffblue Ltd |
| json.cpp | |
| json.h | |
| json_irep.cpp | Util |
| json_irep.h | Util |
| json_stream.cpp | |
| json_stream.h | |
| lazy.h | |
| lispexpr.cpp | |
| lispexpr.h | |
| lispirep.cpp | |
| lispirep.h | |
| lower_byte_operators.cpp | |
| magic.h | Magic numbers used throughout the codebase |
| make_unique.h | |
| mathematical_expr.cpp | |
| mathematical_expr.h | API to expression classes for 'mathematical' expressions |
| mathematical_types.cpp | Mathematical types |
| mathematical_types.h | Mathematical types |
| memory_info.cpp | |
| memory_info.h | |
| memory_units.cpp | |
| memory_units.h | |
| merge_irep.cpp | |
| merge_irep.h | |
| message.cpp | |
| message.h | |
| mp_arith.cpp | |
| mp_arith.h | |
| namespace.cpp | Namespace |
| namespace.h | |
| narrow.h | |
| nfa.h | |
| nodiscard.h | |
| nondet_bool.h | Nondeterministic boolean helper |
| numbering.h | |
| object_factory_parameters.cpp | |
| object_factory_parameters.h | |
| optional.h | |
| optional_utils.h | |
| options.cpp | Options |
| options.h | Options |
| parse_options.cpp | |
| parse_options.h | |
| parser.cpp | |
| parser.h | Parser utilities |
| piped_process.cpp | Subprocess communication with pipes |
| piped_process.h | Subprocess communication with pipes |
| pointer_expr.cpp | |
| pointer_expr.h | API to expression classes for Pointers |
| pointer_offset_size.cpp | Pointer Logic |
| pointer_offset_size.h | Pointer Logic |
| pointer_offset_sum.cpp | Pointer Analysis |
| pointer_offset_sum.h | Pointer Dereferencing |
| pointer_predicates.cpp | Various predicates over pointers in programs |
| pointer_predicates.h | Various predicates over pointers in programs |
| prefix.h | |
| prefix_filter.cpp | Prefix Filtering |
| prefix_filter.h | Prefix Filtering |
| preprocessor.h | Preprocessing Base Class |
| range.h | Ranges: pair of begin and end iterators, which can be initialized from containers, provide useful methods such as map, filter and concat which only manipulate iterators, and can be used with ranged-for |
| 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 |
| 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 |
| 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 | |
| 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_if.cpp | |
| simplify_expr_int.cpp | |
| simplify_expr_pointer.cpp | |
| simplify_expr_struct.cpp | |
| simplify_utils.cpp | |
| simplify_utils.h | |
| small_map.h | Small map |
| small_shared_n_way_ptr.h | |
| small_shared_ptr.h | |
| source_location.cpp | |
| source_location.h | |
| sparse_vector.h | Sparse Vectors |
| ssa_expr.cpp | |
| ssa_expr.h | |
| std_code.cpp | Data structure representing different types of statements in a program |
| std_code.h | |
| std_code_base.h | |
| std_expr.cpp | |
| std_expr.h | API to expression classes |
| std_types.cpp | Pre-defined types |
| std_types.h | Pre-defined types |
| string2int.cpp | |
| string2int.h | |
| string_constant.cpp | |
| string_constant.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 | |
| structured_data.cpp | |
| structured_data.h | |
| substitute_symbols.cpp | Free Symbols |
| substitute_symbols.h | Symbol Substitution |
| suffix.h | |
| symbol.cpp | |
| symbol.h | Symbol table entry |
| symbol_table.cpp | |
| symbol_table.h | Author: Diffblue Ltd |
| symbol_table_base.cpp | |
| symbol_table_base.h | Author: Diffblue Ltd |
| symbol_table_builder.h | |
| tempdir.cpp | |
| tempdir.h | |
| tempfile.cpp | |
| tempfile.h | |
| threeval.cpp | |
| threeval.h | |
| timestamper.cpp | |
| timestamper.h | Emit timestamps |
| type.cpp | Implementations of some functions of typet |
| type.h | Defines typet, type_with_subtypet and type_with_subtypest |
| typecheck.cpp | |
| typecheck.h | |
| ui_message.cpp | |
| ui_message.h | |
| unicode.cpp | |
| unicode.h | |
| union_find.cpp | |
| union_find.h | |
| union_find_replace.cpp | |
| union_find_replace.h | |
| validate.h | |
| validate_expressions.cpp | |
| validate_expressions.h | |
| validate_helpers.h | |
| validate_types.cpp | |
| validate_types.h | |
| validation_interface.h | |
| validation_mode.h | |
| version.h | |
| xml.cpp | |
| xml.h | |
| xml_irep.cpp | |
| xml_irep.h | |
| ► xmllang | |
| graphml.cpp | Read/write graphs as GraphML |
| graphml.h | Read/write graphs as GraphML |
| xml_interface.cpp | XML Interface |
| xml_interface.h | XML Interface |
| xml_parse_tree.cpp | |
| xml_parse_tree.h | |
| xml_parser.cpp | |
| xml_parser.h | |
1.11.0