Go to the documentation of this file.
53 status() <<
"Building error trace" <<
eom;
81 json_result[
"property"] =
83 json_result[
"description"] =
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");
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.
void show_program(const namespacet &ns, const symex_target_equationt &equation)
virtual resultt decide(const goto_functionst &, prop_convt &)
std::unique_ptr< path_storaget > get(const std::string strategy) const
Factory for a path_storaget.
void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override
Resume symbolic execution from saved branch point.
virtual resultt run(const goto_functionst &goto_functions)
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
bool empty() const
Is this storage empty?
trace_optionst trace_options()
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
Bounded model checking or path exploration for goto-programs.
static const commandt reset
return to default formatting, as defined by the terminal
patht & peek()
Reference to the next path to resume.
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
virtual void report_success()
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)
void output_graphml(resultt result)
outputs witnesses in graphml format
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
unsigned get_total_vccs()
const std::string get_option(const std::string &option) const
@ PAUSED
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
mstreamt & status() const
@ SAFE
No safety properties were violated.
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...
std::unique_ptr< memory_model_baset > memory_model
void parse_unwindset(const std::string &unwindset)
xmlt xml(const source_locationt &location)
void simple_slice(symex_target_equationt &equation)
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
void pop()
Remove the next path to resume from the storage.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
#define UNREACHABLE
This should be used to mark dead code.
path_storaget & path_storage
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
void parse_unwind(const std::string &unwind)
virtual void error_trace()
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
ui_message_handlert & ui_message_handler
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
symex_target_equationt equation
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
virtual std::unique_ptr< solvert > get_solver()
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
irep_idt mode
Language mode.
mstreamt & result() const
static const commandt bold
render text with bold font
Symbolic execution from a saved branch point.
source_locationt source_location
json_stream_arrayt & get_json_stream()
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
virtual resultt stop_on_fail(prop_convt &solver)
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
Provides methods for streaming JSON arrays.
virtual resultt dec_solve()=0
goto_programt::const_targett pc
#define INITIALIZE_FUNCTION
virtual void set_message_handler(message_handlert &_message_handler)
virtual void clear()=0
Clear all saved paths.
safety_checkert::resultt execute(abstract_goto_modelt &)
@ ERROR
Safety is unknown due to an error during safety checking.
Information saved at a conditional goto to resume execution.
unsigned get_remaining_vccs()
@ UNSAFE
Some safety properties were violated.
const goto_symex_statet & saved_state
::goto_functiont goto_functiont
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
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).
virtual std::string decision_procedure_text() const =0
Provides methods for streaming JSON objects.
std::size_t count_ignored_SSA_steps() const
A collection of goto functions.
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
message_handlert & get_message_handler()
std::function< bool(void)> driver_callback_after_symex
Optional callback, to be run after symex but before handing the resulting equation to the solver.
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
void validate(const namespacet &ns, const validation_modet vm) const
bool write_graphml(const graphmlt &src, std::ostream &os)
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
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.
bool get_bool_option(const std::string &option) const
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
symex_target_equationt equation
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Factory and information for path_storaget.
virtual void report_failure()
virtual void freeze_program_variables()
Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added t...
Abstract interface to eager or lazy GOTO models.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
virtual std::size_t size() const =0
How many paths does this storage contain?
source_locationt last_source_location
const value_listt & get_list_option(const std::string &option) const
prop_convt & prop_conv() const
mstreamt & statistics() const
bool should_pause_symex
Have states been pushed onto the workqueue?