|
CBMC
|
#include "jbmc_parse_options.h"#include <util/config.h>#include <util/exit_codes.h>#include <util/invariant.h>#include <util/make_unique.h>#include <util/version.h>#include <util/xml.h>#include <goto-programs/adjust_float_expressions.h>#include <goto-programs/goto_check.h>#include <goto-programs/goto_convert_functions.h>#include <goto-programs/instrument_preconditions.h>#include <goto-programs/loop_ids.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/set_properties.h>#include <goto-programs/show_goto_functions.h>#include <goto-programs/show_properties.h>#include <goto-programs/show_symbol_table.h>#include <ansi-c/ansi_c_language.h>#include <goto-checker/all_properties_verifier.h>#include <goto-checker/all_properties_verifier_with_fault_localization.h>#include <goto-checker/all_properties_verifier_with_trace_storage.h>#include <goto-checker/stop_on_fail_verifier.h>#include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>#include <goto-instrument/full_slicer.h>#include <goto-instrument/nondet_static.h>#include <goto-instrument/reachability_slicer.h>#include <goto-symex/path_storage.h>#include <java_bytecode/convert_java_nondet.h>#include <java_bytecode/java_bytecode_language.h>#include <java_bytecode/java_multi_path_symex_checker.h>#include <java_bytecode/java_multi_path_symex_only_checker.h>#include <java_bytecode/java_single_path_symex_checker.h>#include <java_bytecode/java_single_path_symex_only_checker.h>#include <java_bytecode/lazy_goto_model.h>#include <java_bytecode/remove_exceptions.h>#include <java_bytecode/remove_instanceof.h>#include <java_bytecode/remove_java_new.h>#include <java_bytecode/replace_java_nondet.h>#include <java_bytecode/simple_method_stubbing.h>#include <langapi/language.h>#include <langapi/mode.h>#include <linking/static_lifetime_init.h>#include <pointer-analysis/add_failed_symbols.h>#include <cstdlib>#include <iostream>#include <memory>
Include dependency graph for jbmc_parse_options.cpp:Go to the source code of this file.
JBMC Command Line Option Processing
Definition in file jbmc_parse_options.cpp.