CBMC
goto_instrument_parse_options.cpp File Reference

Main Module. More...

#include "goto_instrument_parse_options.h"
#include <util/exception_utils.h>
#include <util/exit_codes.h>
#include <util/help_formatter.h>
#include <util/json.h>
#include <util/options.h>
#include <util/string2int.h>
#include <util/string_utils.h>
#include <util/unicode.h>
#include <util/version.h>
#include <goto-programs/class_hierarchy.h>
#include <goto-programs/ensure_one_backedge_per_target.h>
#include <goto-programs/goto_check.h>
#include <goto-programs/goto_inline.h>
#include <goto-programs/interpreter.h>
#include <goto-programs/label_function_pointer_call_sites.h>
#include <goto-programs/loop_ids.h>
#include <goto-programs/mm_io.h>
#include <goto-programs/parameter_assignments.h>
#include <goto-programs/read_goto_binary.h>
#include <goto-programs/remove_calls_no_body.h>
#include <goto-programs/remove_function_pointers.h>
#include <goto-programs/remove_returns.h>
#include <goto-programs/remove_skip.h>
#include <goto-programs/remove_unused_functions.h>
#include <goto-programs/remove_virtual_functions.h>
#include <goto-programs/restrict_function_pointers.h>
#include <goto-programs/rewrite_rw_ok.h>
#include <goto-programs/rewrite_union.h>
#include <goto-programs/set_properties.h>
#include <goto-programs/show_properties.h>
#include <goto-programs/show_symbol_table.h>
#include <goto-programs/slice_global_inits.h>
#include <goto-programs/string_abstraction.h>
#include <goto-programs/write_goto_binary.h>
#include <analyses/call_graph.h>
#include <analyses/constant_propagator.h>
#include <analyses/custom_bitvector_analysis.h>
#include <analyses/dependence_graph.h>
#include <analyses/escape_analysis.h>
#include <analyses/global_may_alias.h>
#include <analyses/guard.h>
#include <analyses/interval_analysis.h>
#include <analyses/interval_domain.h>
#include <analyses/is_threaded.h>
#include <analyses/lexical_loops.h>
#include <analyses/local_bitvector_analysis.h>
#include <analyses/local_safe_pointers.h>
#include <analyses/natural_loops.h>
#include <analyses/reaching_definitions.h>
#include <analyses/sese_regions.h>
#include <ansi-c/ansi_c_language.h>
#include <ansi-c/c_object_factory_parameters.h>
#include <ansi-c/cprover_library.h>
#include <ansi-c/gcc_version.h>
#include <ansi-c/goto-conversion/link_to_library.h>
#include <assembler/remove_asm.h>
#include <cpp/cprover_library.h>
#include <pointer-analysis/add_failed_symbols.h>
#include <pointer-analysis/show_value_sets.h>
#include <pointer-analysis/value_set_analysis.h>
#include "alignment_checks.h"
#include "branch.h"
#include "call_sequences.h"
#include "concurrency.h"
#include "dot.h"
#include "full_slicer.h"
#include "function.h"
#include "havoc_loops.h"
#include "horn_encoding.h"
#include "insert_final_assert_false.h"
#include "interrupt.h"
#include "k_induction.h"
#include "mmio.h"
#include "model_argc_argv.h"
#include "nondet_static.h"
#include "nondet_volatile.h"
#include "points_to.h"
#include "race_check.h"
#include "remove_function.h"
#include "rw_set.h"
#include "show_locations.h"
#include "skip_loops.h"
#include "splice_call.h"
#include "stack_depth.h"
#include "thread_instrumentation.h"
#include "undefined_functions.h"
#include "unwind.h"
#include "value_set_fi_fp_removal.h"
#include <fstream>
#include <iostream>
#include <memory>
#include "accelerate/accelerate.h"

Go to the source code of this file.

Detailed Description

Main Module.

Definition in file goto_instrument_parse_options.cpp.