53 status() <<
"Building error trace" <<
eom;
81 json_result[
"property"] =
83 json_result[
"description"] =
87 json_result.push_back_stream_array(
"trace");
88 convert<json_stream_arrayt>(
ns, goto_trace, json_trace,
trace_options());
113 std::ofstream out(graphml);
132 status() <<
"Passing problem to " 137 auto solver_start = std::chrono::steady_clock::now();
146 auto solver_stop = std::chrono::steady_clock::now();
147 status() <<
"Runtime decision procedure: " 148 << std::chrono::duration<double>(solver_stop-solver_start).count()
181 log.
result() << json_result;
213 log.
result() << json_result;
223 if(mm.empty() || mm==
"sc")
232 "invalid parameter " + mm,
"--mm",
"try values of sc, tso, pso");
246 status() <<
"Starting Bounded Model Checking" <<
eom;
259 auto get_goto_function = [&goto_model](
const irep_idt &id) ->
295 statistics() <<
"size of program expression: " 303 if(!cov_out.empty() &&
306 error() <<
"Failed to write symex coverage report" <<
eom;
318 return cover(goto_functions)?
325 goto_functions, *
this,
options);
326 return fault_localization();
353 catch(
const std::string &error_str)
362 catch(
const char *error_str)
371 catch(
const std::bad_alloc &)
401 <<
" assignments"<<
eom;
410 <<
" assignments"<<
eom;
416 <<
" remaining after simplification" <<
eom;
420 <<
" new VCC(s) along current path segment" <<
eom;
484 error() <<
"decision procedure failed" <<
eom;
508 std::function<
bool(
void)> callback_after_symex)
514 std::unique_ptr<path_storaget> worklist;
515 std::string strategy = opts.
get_option(
"exploration-strategy");
518 "Front-end passed us invalid path strategy '" + strategy +
"'");
519 worklist = path_strategy_chooser.
get(strategy);
528 std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
531 bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex);
532 if(driver_configure_bmc)
533 driver_configure_bmc(bmc, symbol_table);
534 tmp_result = bmc.
run(model);
545 final_result = tmp_result;
549 "the worklist should be empty after doing full-program " 550 "model checking, but the worklist contains " +
568 while(!worklist->empty())
575 std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
587 callback_after_symex);
588 if(driver_configure_bmc)
589 driver_configure_bmc(pe, symbol_table);
590 tmp_result = pe.
run(model);
601 final_result &= tmp_result;
605 catch(
const char *error_msg)
607 message.
error() << error_msg << message.
eom;
610 catch(
const std::string &error_msg)
612 message.
error() << error_msg << message.
eom;
615 catch(std::runtime_error &e)
617 message.
error() << e.what() << message.
eom;
651 "Branch points were saved even though we should have been " 652 "executing the entire program and merging paths");
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
Abstract interface to eager or lazy GOTO models.
ui_message_handlert & ui_message_handler
virtual void symex_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
static const commandt bold
render text with bold font
Output of the verification conditions (VCCs)
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
void simple_slice(symex_target_equationt &equation)
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
irep_idt mode
Language mode.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Provides methods for streaming JSON objects.
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Slicer for matching with trace files.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
path_storaget & path_storage
virtual void report_failure()
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
const value_listt & get_list_option(const std::string &option) const
Memory models for partial order concurrency.
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation, symbol_tablet &new_symbol_table)
Performs symbolic execution using a state and equation that have already been used to symex part of t...
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
xmlt xml(const source_locationt &location)
static const commandt reset
return to default formatting, as defined by the terminal
void validate(const namespacet &ns, const validation_modet vm) const
goto_programt::const_targett pc
symex_target_equationt equation
virtual resultt decide(const goto_functionst &, prop_convt &)
virtual const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id)=0
Get a GOTO function by name, or throw if no such function exists.
Factory and information for path_storaget.
json_stream_arrayt & get_json_stream()
const goto_symex_statet & saved_state
virtual void error_trace()
virtual resultt dec_solve()=0
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Some safety properties were violated.
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override
Resume symbolic execution from saved branch point.
source_locationt source_location
const std::string get_option(const std::string &option) const
Safety is unknown due to an error during safety checking.
#define INITIALIZE_FUNCTION
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
bool get_bool_option(const std::string &option) const
Provides methods for streaming JSON arrays.
::goto_functiont goto_functiont
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
Symbolic execution from a saved branch point.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
A collection of goto functions.
virtual void set_message_handler(message_handlert &_message_handler)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
No safety properties were violated.
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
void parse_unwindset(const std::string &unwindset)
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
std::unique_ptr< path_storaget > get(const std::string strategy) const
Factory for a path_storaget.
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand)...
message_handlert & get_message_handler()
Bounded Model Checking for ANSI-C + HDL.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & result() const
mstreamt & status() const
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
safety_checkert::resultt execute(abstract_goto_modelt &)
bool should_pause_symex
Have states been pushed onto the workqueue?
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
virtual resultt run(const goto_functionst &goto_functions)
bool write_graphml(const graphmlt &src, std::ostream &os)
virtual resultt stop_on_fail(prop_convt &solver)
Output of the program (SSA) constraints.
#define UNREACHABLE
This should be used to mark dead code.
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
Information saved at a conditional goto to resume execution.
bool empty() const
Is this storage empty?
Bounded model checking or path exploration for goto-programs.
unsigned get_total_vccs()
std::unique_ptr< memory_model_baset > memory_model
symex_target_equationt equation
std::size_t count_ignored_SSA_steps() const
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
std::function< bool(void)> driver_callback_after_symex
Optional callback, to be run after symex but before handing the resulting equation to the solver...
virtual void report_success()
source_locationt last_source_location
void parse_unwind(const std::string &unwind)
trace_optionst trace_options()
virtual void freeze_program_variables()
Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added t...
mstreamt & statistics() const
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
unsigned get_remaining_vccs()
virtual std::unique_ptr< solvert > get_solver()
void output_graphml(resultt result)
outputs witnesses in graphml format
Witnesses for Traces and Proofs.
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0