53 status() <<
"Building error trace" <<
eom;
61 std::cout <<
"\n" <<
"Counterexample:" <<
"\n";
69 std::cout << xml <<
"\n";
81 result[
"description"]=
84 jsont &json_trace=result[
"trace"];
86 std::cout <<
",\n" << json_result;
113 std::ofstream out(graphml);
131 status() <<
"converting constraints" <<
eom;
141 status() <<
"Passing problem to " 158 status() <<
"Runtime decision procedure: " 159 << (sat_stop-sat_start) <<
"s" <<
eom;
167 result() <<
"VERIFICATION SUCCESSFUL" <<
eom;
187 std::cout <<
",\n" << json_result;
195 result() <<
"VERIFICATION FAILED" <<
eom;
215 std::cout <<
",\n" << json_result;
227 std::cout <<
"\n" <<
"Program constraints:" <<
"\n";
231 std::cout <<
"// " << step.source.pc->location_number <<
" ";
232 std::cout << step.source.pc->source_location.as_string() <<
"\n";
234 if(step.is_assignment())
236 std::string string_value;
237 languages.
from_expr(step.cond_expr, string_value);
238 std::cout <<
"(" << count <<
") " << string_value <<
"\n";
240 if(!step.guard.is_true())
242 languages.
from_expr(step.guard, string_value);
243 std::cout << std::string(std::to_string(count).size()+3,
' ');
244 std::cout <<
"guard: " << string_value <<
"\n";
249 else if(step.is_assert())
251 std::string string_value;
252 languages.
from_expr(step.cond_expr, string_value);
253 std::cout <<
"(" << count <<
") ASSERT(" 254 << string_value <<
") " <<
"\n";
256 if(!step.guard.is_true())
258 languages.
from_expr(step.guard, string_value);
259 std::cout << std::string(std::to_string(count).size()+3,
' ');
260 std::cout <<
"guard: " << string_value <<
"\n";
265 else if(step.is_assume())
267 std::string string_value;
268 languages.
from_expr(step.cond_expr, string_value);
269 std::cout <<
"(" << count <<
") ASSUME(" 270 << string_value <<
") " <<
"\n";
272 if(!step.guard.is_true())
274 languages.
from_expr(step.guard, string_value);
275 std::cout << std::string(std::to_string(count).size()+3,
' ');
276 std::cout <<
"guard: " << string_value <<
"\n";
281 else if(step.is_constraint())
283 std::string string_value;
284 languages.
from_expr(step.cond_expr, string_value);
285 std::cout <<
"(" << count <<
") CONSTRAINT(" 286 << string_value <<
") " <<
"\n";
290 else if(step.is_shared_read() || step.is_shared_write())
292 std::string string_value;
293 languages.
from_expr(step.ssa_lhs, string_value);
294 std::cout <<
"(" << count <<
") SHARED_" 295 << (step.is_shared_write()?
"WRITE":
"READ")
296 <<
"(" << string_value <<
")\n";
298 if(!step.guard.is_true())
300 languages.
from_expr(step.guard, string_value);
301 std::cout << std::string(std::to_string(count).size()+3,
' ');
302 std::cout <<
"guard: " << string_value <<
"\n";
314 std::unique_ptr<memory_model_baset> memory_model;
316 if(mm.empty() || mm==
"sc")
324 error() <<
"Invalid memory model " << mm
325 <<
" -- use one of sc, tso, pso" <<
eom;
338 status() <<
"Starting Bounded Model Checking" <<
eom;
348 symex(goto_functions);
358 catch(
const std::string &error_str)
367 catch(
const char *error_str)
376 catch(std::bad_alloc)
382 statistics() <<
"size of program expression: " 408 <<
" assignments" <<
eom;
417 <<
" assignments" <<
eom;
425 <<
" remaining after simplification" <<
eom;
430 if(!cov_out.empty() &&
433 error() <<
"Failed to write symex coverage report" <<
eom;
447 return cover(goto_functions, criteria)?
454 goto_functions, *
this,
options);
455 return fault_localization();
476 catch(std::string &error_str)
482 catch(
const char *error_str)
488 catch(std::bad_alloc)
537 error() <<
"decision procedure failed" <<
eom;
546 std::vector<std::string> unwindset_loops;
549 for(
auto &val : unwindset_loops)
551 unsigned thread_nr=0;
552 bool thread_nr_set=
false;
556 val.find(
":")!=std::string::npos)
558 std::string nr=val.substr(0, val.find(
":"));
561 val.erase(0, nr.size()+1);
564 if(val.rfind(
":")!=std::string::npos)
566 std::string
id=val.substr(0, val.rfind(
":"));
void output_graphml(resultt result, const goto_functionst &goto_functions)
outputs witnesses in graphml format
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
void slice(symex_target_equationt &equation)
const std::string & id2string(const irep_idt &d)
void convert(prop_convt &prop_conv)
void simple_slice(symex_target_equationt &equation)
unsigned int get_unsigned_int_option(const std::string &option) const
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
irep_idt mode
Language mode.
void set_unwind_loop_limit(const irep_idt &id, unsigned limit)
unsigned unsafe_string2unsigned(const std::string &str, int base)
bool from_expr(const exprt &expr, std::string &code)
languaget * new_ansi_c_language()
Slicer for matching with trace files.
virtual void report_failure()
const value_listt & get_list_option(const std::string &option) const
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
Memory models for partial order concurrency.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void set_unwind_limit(unsigned limit)
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
static mstreamt & eom(mstreamt &m)
xmlt xml(const source_locationt &location)
goto_programt::const_targett pc
virtual void setup_unwind()
json_arrayt & make_array()
virtual resultt decide(const goto_functionst &, prop_convt &)
expr_listt bmc_constraints
jsont & push_back(const jsont &json)
unsigned count_ignored_SSA_steps() const
virtual void error_trace()
virtual void do_unwind_module()
virtual resultt dec_solve()=0
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
source_locationt source_location
const std::string get_option(const std::string &option) const
bool get_bool_option(const std::string &option) const
std::list< std::string > value_listt
virtual resultt run(const goto_functionst &goto_functions)
virtual void set_message_handler(message_handlert &_message_handler)
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
#define forall_expr_list(it, expr)
virtual resultt stop_on_fail(const goto_functionst &goto_functions, prop_convt &solver)
message_handlert & get_message_handler()
Bounded Model Checking for ANSI-C + HDL.
absolute_timet current_time()
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
bool write_graphml(const graphmlt &src, std::ostream &os)
virtual void show_program()
void set_to_true(const exprt &expr)
Memory models for partial order concurrency.
Memory models for partial order concurrency.
symex_target_equationt equation
json_objectt & make_object()
virtual void report_success()
source_locationt last_source_location
int unsafe_string2int(const std::string &str, int base)
void set_unwind_thread_loop_limit(unsigned thread_nr, const irep_idt &id, unsigned limit)
Witnesses for Traces and Proofs.
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0