cprover
bmc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "bmc.h"
13 
14 #include <chrono>
15 #include <iostream>
16 
17 #include <util/exit_codes.h>
18 
19 #include <langapi/language_util.h>
20 
24 
27 #include <goto-symex/slice.h>
29 
31 
32 #include "cbmc_solvers.h"
34 #include "fault_localization.h"
35 
43 {
44  // this is a hook for cegis
45 }
46 
48 {
49  status() << "Building error trace" << eom;
50 
52  build_goto_trace(equation, prop_conv, ns, goto_trace);
53 
54  switch(ui)
55  {
57  result() << "Counterexample:" << eom;
58  show_goto_trace(result(), ns, goto_trace);
59  result() << eom;
60  break;
61 
63  {
64  xmlt xml;
65  convert(ns, goto_trace, xml);
66  status() << xml;
67  }
68  break;
69 
71  {
72  json_stream_objectt &json_result =
74  const goto_trace_stept &step=goto_trace.steps.back();
75  json_result["property"] =
76  json_stringt(step.pc->source_location.get_property_id());
77  json_result["description"] =
78  json_stringt(step.pc->source_location.get_comment());
79  json_result["status"]=json_stringt("failed");
80  json_stream_arrayt &json_trace =
81  json_result.push_back_stream_array("trace");
82  convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options());
83  }
84  break;
85  }
86 }
87 
90 {
91  const std::string graphml=options.get_option("graphml-witness");
92  if(graphml.empty())
93  return;
94 
95  graphml_witnesst graphml_witness(ns);
97  graphml_witness(safety_checkert::error_trace);
98  else if(result==resultt::SAFE)
99  graphml_witness(equation);
100  else
101  return;
102 
103  if(graphml=="-")
104  write_graphml(graphml_witness.graph(), std::cout);
105  else
106  {
107  std::ofstream out(graphml);
108  write_graphml(graphml_witness.graph(), out);
109  }
110 }
111 
113 {
114  status() << "converting SSA" << eom;
115 
116  // convert SSA
118 
119  // hook for cegis to freeze synthesis program vars
121 }
122 
125 {
126  status() << "Passing problem to "
128 
130 
131  auto solver_start = std::chrono::steady_clock::now();
132 
133  do_conversion();
134 
135  status() << "Running " << prop_conv.decision_procedure_text() << eom;
136 
138 
139  {
140  auto solver_stop = std::chrono::steady_clock::now();
141  status() << "Runtime decision procedure: "
142  << std::chrono::duration<double>(solver_stop-solver_start).count()
143  << "s" << eom;
144  }
145 
146  return dec_result;
147 }
148 
150 {
151  result() << "VERIFICATION SUCCESSFUL" << eom;
152 
153  switch(ui)
154  {
156  break;
157 
159  {
160  xmlt xml("cprover-status");
161  xml.data="SUCCESS";
162  result() << xml;
163  }
164  break;
165 
167  {
168  json_objectt json_result;
169  json_result["cProverStatus"]=json_stringt("success");
170  result() << json_result;
171  }
172  break;
173  }
174 }
175 
177 {
178  result() << "VERIFICATION FAILED" << eom;
179 
180  switch(ui)
181  {
183  break;
184 
186  {
187  xmlt xml("cprover-status");
188  xml.data="FAILURE";
189  result() << xml;
190  }
191  break;
192 
194  {
195  json_objectt json_result;
196  json_result["cProverStatus"]=json_stringt("failure");
197  result() << json_result;
198  }
199  break;
200  }
201 }
202 
204 {
205  unsigned count=1;
206 
207  std::cout << "\n" << "Program constraints:" << "\n";
208 
209  for(const auto &step : equation.SSA_steps)
210  {
211  std::cout << "// " << step.source.pc->location_number << " ";
212  std::cout << step.source.pc->source_location.as_string() << "\n";
213  const irep_idt &function = step.source.pc->function;
214 
215  if(step.is_assignment())
216  {
217  std::string string_value = from_expr(ns, function, step.cond_expr);
218  std::cout << "(" << count << ") " << string_value << "\n";
219 
220  if(!step.guard.is_true())
221  {
222  std::string string_value = from_expr(ns, function, step.guard);
223  std::cout << std::string(std::to_string(count).size()+3, ' ');
224  std::cout << "guard: " << string_value << "\n";
225  }
226 
227  count++;
228  }
229  else if(step.is_assert())
230  {
231  std::string string_value = from_expr(ns, function, step.cond_expr);
232  std::cout << "(" << count << ") ASSERT("
233  << string_value <<") " << "\n";
234 
235  if(!step.guard.is_true())
236  {
237  std::string string_value = from_expr(ns, function, step.guard);
238  std::cout << std::string(std::to_string(count).size()+3, ' ');
239  std::cout << "guard: " << string_value << "\n";
240  }
241 
242  count++;
243  }
244  else if(step.is_assume())
245  {
246  std::string string_value = from_expr(ns, function, step.cond_expr);
247  std::cout << "(" << count << ") ASSUME("
248  << string_value <<") " << "\n";
249 
250  if(!step.guard.is_true())
251  {
252  std::string string_value = from_expr(ns, function, step.guard);
253  std::cout << std::string(std::to_string(count).size()+3, ' ');
254  std::cout << "guard: " << string_value << "\n";
255  }
256 
257  count++;
258  }
259  else if(step.is_constraint())
260  {
261  std::string string_value = from_expr(ns, function, step.cond_expr);
262  std::cout << "(" << count << ") CONSTRAINT("
263  << string_value <<") " << "\n";
264 
265  count++;
266  }
267  else if(step.is_shared_read() || step.is_shared_write())
268  {
269  std::string string_value = from_expr(ns, function, step.ssa_lhs);
270  std::cout << "(" << count << ") SHARED_"
271  << (step.is_shared_write()?"WRITE":"READ")
272  << "(" << string_value <<")\n";
273 
274  if(!step.guard.is_true())
275  {
276  std::string string_value = from_expr(ns, function, step.guard);
277  std::cout << std::string(std::to_string(count).size()+3, ' ');
278  std::cout << "guard: " << string_value << "\n";
279  }
280 
281  count++;
282  }
283  }
284 }
285 
286 
288 {
289  const std::string mm=options.get_option("mm");
290 
291  if(mm.empty() || mm=="sc")
292  memory_model=util_make_unique<memory_model_sct>(ns);
293  else if(mm=="tso")
294  memory_model=util_make_unique<memory_model_tsot>(ns);
295  else if(mm=="pso")
296  memory_model=util_make_unique<memory_model_psot>(ns);
297  else
298  {
299  error() << "Invalid memory model " << mm
300  << " -- use one of sc, tso, pso" << eom;
301  throw "invalid memory model";
302  }
303 }
304 
306 {
308 
309  {
310  const symbolt *init_symbol;
311  if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
312  symex.language_mode=init_symbol->mode;
313  }
314 
315  status() << "Starting Bounded Model Checking" << eom;
316 
318 
321 }
322 
324  abstract_goto_modelt &goto_model)
325 {
326  try
327  {
328  auto get_goto_function = [&goto_model](const irep_idt &id) ->
330  {
331  return goto_model.get_goto_function(id);
332  };
333 
334  perform_symbolic_execution(get_goto_function);
335 
336  // Borrow a reference to the goto functions map. This reference, or
337  // iterators pointing into it, must not be stored by this function or its
338  // callees, as goto_model.get_goto_function (as used by symex)
339  // will have side-effects on it.
340  const goto_functionst &goto_functions =
341  goto_model.get_goto_functions();
342 
345 
346  // This provides the driver program the opportunity to do things like a
347  // symbol-table or goto-functions dump instead of actually running the
348  // checker, like show-vcc except driver-program specific.
349  // In particular clients that use symex-driven program loading need to print
350  // GOTO functions after symex, as function bodies are not produced until
351  // symex first requests them.
353  return safety_checkert::resultt::SAFE; // to indicate non-error
354 
355  // add a partial ordering, if required
356  if(equation.has_threads())
357  {
358  memory_model->set_message_handler(get_message_handler());
359  (*memory_model)(equation);
360  }
361 
362  statistics() << "size of program expression: "
363  << equation.SSA_steps.size()
364  << " steps" << eom;
365 
366  slice();
367 
368  // coverage report
369  std::string cov_out=options.get_option("symex-coverage-report");
370  if(!cov_out.empty() &&
371  symex.output_coverage_report(goto_functions, cov_out))
372  {
373  error() << "Failed to write symex coverage report" << eom;
375  }
376 
377  if(options.get_bool_option("show-vcc"))
378  {
379  show_vcc();
380  return safety_checkert::resultt::SAFE; // to indicate non-error
381  }
382 
383  if(!options.get_list_option("cover").empty())
384  {
385  const optionst::value_listt criteria=
386  options.get_list_option("cover");
387  return cover(goto_functions, criteria)?
389  }
390 
391  if(options.get_option("localize-faults")!="")
392  {
393  fault_localizationt fault_localization(
394  goto_functions, *this, options);
395  return fault_localization();
396  }
397 
398  // any properties to check at all?
399  if(!options.get_bool_option("program-only") &&
401  {
402  report_success();
405  }
406 
407  if(options.get_bool_option("program-only"))
408  {
409  show_program();
411  }
412 
413  return decide(goto_functions, prop_conv);
414  }
415 
416  catch(const std::string &error_str)
417  {
418  messaget message(get_message_handler());
420  message.error() << error_str << messaget::eom;
421 
423  }
424 
425  catch(const char *error_str)
426  {
427  messaget message(get_message_handler());
429  message.error() << error_str << messaget::eom;
430 
432  }
433 
434  catch(const std::bad_alloc &)
435  {
436  error() << "Out of memory" << eom;
438  }
439 }
440 
442 {
443  if(options.get_option("slice-by-trace")!="")
444  {
445  symex_slice_by_tracet symex_slice_by_trace(ns);
446 
447  symex_slice_by_trace.slice_by_trace
448  (options.get_option("slice-by-trace"),
449  equation);
450  }
451  // any properties to check at all?
452  if(equation.has_threads())
453  {
454  // we should build a thread-aware SSA slicer
455  statistics() << "no slicing due to threads" << eom;
456  }
457  else
458  {
459  if(options.get_bool_option("slice-formula"))
460  {
461  ::slice(equation);
462  statistics() << "slicing removed "
464  << " assignments"<<eom;
465  }
466  else
467  {
468  if(options.get_list_option("cover").empty())
469  {
471  statistics() << "simple slicing removed "
473  << " assignments"<<eom;
474  }
475  }
476  }
477  statistics() << "Generated "
478  << symex.total_vccs<<" VCC(s), "
480  << " remaining after simplification" << eom;
481 }
482 
484  abstract_goto_modelt &goto_model)
485 {
486  setup();
487 
488  return execute(goto_model);
489 }
490 
492  const goto_functionst &goto_functions,
493  prop_convt &prop_conv)
494 {
496 
497  if(options.get_bool_option("stop-on-fail"))
498  return stop_on_fail(prop_conv);
499  else
500  return all_properties(goto_functions, prop_conv);
501 }
502 
504 {
505  if(options.get_bool_option("show-vcc"))
506  {
507  show_vcc();
508  }
509 
510  if(options.get_bool_option("program-only"))
511  {
512  show_program();
513  }
514 }
515 
517 {
519  {
521  report_success();
523  return resultt::SAFE;
524 
526  if(options.get_bool_option("trace"))
527  {
528  if(options.get_bool_option("beautify"))
530  dynamic_cast<bv_cbmct &>(prop_conv), equation, ns);
531 
532  error_trace();
534  }
535 
536  report_failure();
537  return resultt::UNSAFE;
538 
539  default:
540  if(options.get_bool_option("dimacs") ||
541  options.get_option("outfile")!="")
542  return resultt::SAFE;
543 
544  error() << "decision procedure failed" << eom;
545 
546  return resultt::ERROR;
547  }
548 }
549 
554 // creating those function bodies on demand.
562  const path_strategy_choosert &path_strategy_chooser,
563  const optionst &opts,
564  abstract_goto_modelt &model,
565  const ui_message_handlert::uit &ui,
566  messaget &message,
567  std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
568  std::function<bool(void)> callback_after_symex)
569 {
572  const symbol_tablet &symbol_table = model.get_symbol_table();
573  message_handlert &mh = message.get_message_handler();
574  std::unique_ptr<path_storaget> worklist;
575  std::string strategy = opts.get_option("exploration-strategy");
576  INVARIANT(
577  path_strategy_chooser.is_valid_strategy(strategy),
578  "Front-end passed us invalid path strategy '" + strategy + "'");
579  worklist = path_strategy_chooser.get(strategy);
580  try
581  {
582  {
583  cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
584  solvers.set_ui(ui);
585  std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
586  cbmc_solver = solvers.get_solver();
587  prop_convt &pc = cbmc_solver->prop_conv();
588  bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex);
589  bmc.set_ui(ui);
590  if(driver_configure_bmc)
591  driver_configure_bmc(bmc, symbol_table);
592  tmp_result = bmc.run(model);
593  if(tmp_result != safety_checkert::resultt::PAUSED)
594  final_result = tmp_result;
595  }
596  INVARIANT(
597  opts.get_bool_option("paths") || worklist->empty(),
598  "the worklist should be empty after doing full-program "
599  "model checking, but the worklist contains " +
600  std::to_string(worklist->size()) + " unexplored branches.");
601 
602  // When model checking, the bmc.run() above will already have explored
603  // the entire program, and final_result contains the verification result.
604  // The worklist (containing paths that have not yet been explored) is thus
605  // empty, and we don't enter this loop.
606  //
607  // When doing path exploration, there will be some saved paths left to
608  // explore in the worklist. We thus need to run the above code again,
609  // once for each saved path in the worklist, to continue symbolically
610  // execute the program. Note that the code in the loop is similar to
611  // the code above except that we construct a path_explorert rather than
612  // a bmct, which allows us to execute from a saved state rather than
613  // from the entry point. See the path_explorert documentation, and the
614  // difference between the implementations of perform_symbolic_exection()
615  // in bmct and path_explorert, for more information.
616 
617  while(!worklist->empty())
618  {
619  if(tmp_result != safety_checkert::resultt::PAUSED)
620  message.status() << "___________________________\n"
621  << "Starting new path (" << worklist->size()
622  << " to go)\n"
623  << message.eom;
624  cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
625  solvers.set_ui(ui);
626  std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
627  cbmc_solver = solvers.get_solver();
628  prop_convt &pc = cbmc_solver->prop_conv();
629  path_storaget::patht &resume = worklist->peek();
630  path_explorert pe(
631  opts,
632  symbol_table,
633  mh,
634  pc,
635  resume.equation,
636  resume.state,
637  *worklist,
638  callback_after_symex);
639  if(driver_configure_bmc)
640  driver_configure_bmc(pe, symbol_table);
641  tmp_result = pe.run(model);
642  if(tmp_result != safety_checkert::resultt::PAUSED)
643  final_result &= tmp_result;
644  worklist->pop();
645  }
646  }
647  catch(const char *error_msg)
648  {
649  message.error() << error_msg << message.eom;
650  return CPROVER_EXIT_EXCEPTION;
651  }
652  catch(const std::string &error_msg)
653  {
654  message.error() << error_msg << message.eom;
655  return CPROVER_EXIT_EXCEPTION;
656  }
657  catch(std::runtime_error &e)
658  {
659  message.error() << e.what() << message.eom;
660  return CPROVER_EXIT_EXCEPTION;
661  }
662 
663  switch(final_result)
664  {
674  UNREACHABLE;
675  }
676  UNREACHABLE;
677 }
678 
680  goto_symext::get_goto_functiont get_goto_function)
681 {
683  INVARIANT(
685  "Branch points were saved even though we should have been "
686  "executing the entire program and merging paths");
687 }
688 
690  goto_symext::get_goto_functiont get_goto_function)
691 {
693  get_goto_function, saved_state, &equation, symex_symbol_table);
694 }
Fault Localization.
void do_conversion()
Definition: bmc.cpp:112
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
Definition: bmc.cpp:679
void set_ui(ui_message_handlert::uit _ui)
Definition: bmc.h:106
Abstract interface to eager or lazy GOTO models.
void convert(prop_convt &prop_conv)
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:240
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
irep_idt mode
Language mode.
Definition: symbol.h:52
void set_ui(ui_message_handlert::uit _ui)
Definition: cbmc_solvers.h:123
Provides methods for streaming JSON objects.
Definition: json_stream.h:139
void show()
Definition: bmc.cpp:503
const graphmlt & graph()
void slice()
Definition: bmc.cpp:441
virtual void show_vcc()
Definition: show_vcc.cpp:135
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Slicer for matching with trace files.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
path_storaget & path_storage
Definition: bmc.h:184
virtual void report_failure()
Definition: bmc.cpp:176
prop_convt & prop_conv() const
Definition: cbmc_solvers.h:72
We haven&#39;t yet assigned a safety check result to this object.
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
Definition: options.cpp:78
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
Definition: bmc_cover.cpp:429
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...
Definition: symbol.h:30
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:84
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:247
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
TO_BE_DOCUMENTED.
Definition: goto_trace.h:36
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:41
stepst steps
Definition: goto_trace.h:156
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
goto_programt::const_targett pc
Definition: goto_trace.h:95
symex_target_equationt equation
Definition: path_storage.h:30
virtual resultt decide(const goto_functionst &, prop_convt &)
Definition: bmc.cpp:491
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
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.
goto_tracet error_trace
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, 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)...
Definition: bmc.cpp:561
namespacet ns
Definition: bmc.h:182
Factory and information for path_storaget.
Definition: path_storage.h:119
symex_bmct symex
Definition: bmc.h:185
const goto_symex_statet & saved_state
Definition: bmc.h:288
virtual void error_trace()
Definition: bmc.cpp:47
virtual void symex_from_entry_point_of(const goto_functionst &goto_functions, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
Definition: symex_main.cpp:260
virtual resultt dec_solve()=0
Some safety properties were violated.
ui_message_handlert::uit ui
Definition: bmc.h:189
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:75
Traces of GOTO Programs.
void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override
Resume symbolic execution from saved branch point.
Definition: bmc.cpp:689
source_locationt source_location
Definition: message.h:214
prop_convt & prop_conv
Definition: bmc.h:186
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
Safety is unknown due to an error during safety checking.
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *const 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...
Definition: symex_main.cpp:216
#define INITIALIZE_FUNCTION
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
Definition: path_storage.h:128
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
void setup()
Definition: bmc.cpp:305
The symbol table.
Definition: symbol_table.h:19
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
mstreamt & error() const
Definition: message.h:302
std::list< std::string > value_listt
Definition: options.h:22
::goto_functiont goto_functiont
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
Symbolic execution from a saved branch point.
Definition: bmc.h:263
Definition: xml.h:18
unsigned remaining_vccs
Definition: goto_symex.h:213
Traces of GOTO Programs.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
std::string data
Definition: xml.h:30
No safety properties were violated.
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Definition: bmc.cpp:124
const optionst & options
Definition: bmc.h:177
void parse_unwindset(const std::string &unwindset)
Definition: unwindset.cpp:24
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)
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:36
std::unique_ptr< path_storaget > get(const std::string strategy) const
Factory for a path_storaget.
Definition: path_storage.h:137
message_handlert & get_message_handler()
Definition: message.h:153
Bounded Model Checking for ANSI-C + HDL.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & result() const
Definition: message.h:312
void get_memory_model()
Definition: bmc.cpp:287
mstreamt & status() const
Definition: message.h:317
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
Definition: goto_symex.h:220
safety_checkert::resultt execute(abstract_goto_modelt &)
Definition: bmc.cpp:323
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:175
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...
Slicer for symex traces.
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indiciates the analysis has been performed without error AND the software is ...
Definition: exit_codes.h:25
virtual resultt run(const goto_functionst &goto_functions)
Definition: bmc.h:96
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:212
virtual void show_program()
Definition: bmc.cpp:203
virtual resultt stop_on_fail(prop_convt &solver)
Definition: bmc.cpp:516
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define UNREACHABLE
Definition: invariant.h:250
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
Definition: bmc.h:181
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:28
bool empty() const
Is this storage empty?
Definition: path_storage.h:75
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
void make_nil()
Definition: irep.h:243
Bounded Model Checking for ANSI-C + HDL.
std::unique_ptr< memory_model_baset > memory_model
Definition: bmc.h:187
symex_target_equationt equation
Definition: bmc.h:183
std::size_t count_ignored_SSA_steps() const
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indiciates the analysis has been performed without error AND the software is ...
Definition: exit_codes.h:21
std::function< bool(void)> driver_callback_after_symex
Optional callback, to be run after symex but before handing the resulting equation to the solver...
Definition: bmc.h:250
virtual void report_success()
Definition: bmc.cpp:149
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
source_locationt last_source_location
Definition: symex_bmc.h:36
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:18
trace_optionst trace_options()
Definition: bmc.h:206
json_stream_arrayt & json_stream()
Returns a reference to the top-level JSON array stream.
Definition: message.h:252
virtual void freeze_program_variables()
Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added t...
Definition: bmc.cpp:42
unsigned total_vccs
Definition: goto_symex.h:213
goto_symex_statet state
Definition: path_storage.h:31
mstreamt & statistics() const
Definition: message.h:322
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
unwindsett unwindset
Definition: symex_bmc.h:84
void output_graphml(resultt result)
outputs witnesses in graphml format
Definition: bmc.cpp:89
Traces of GOTO Programs.
Witnesses for Traces and Proofs.
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0