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/exception_utils.h>
18 #include <util/exit_codes.h>
19 
20 #include <langapi/language_util.h>
21 
25 
29 #include <goto-symex/show_vcc.h>
30 #include <goto-symex/slice.h>
32 
34 
36 
38 #include "fault_localization.h"
39 
47 {
48  // this is a hook for cegis
49 }
50 
52 {
53  status() << "Building error trace" << eom;
54 
56  build_goto_trace(equation, prop_conv, ns, goto_trace);
57 
58  switch(ui_message_handler.get_ui())
59  {
61  result() << "Counterexample:" << eom;
62  show_goto_trace(result(), ns, goto_trace, trace_options());
63  result() << eom;
64  break;
65 
67  {
68  xmlt xml;
69  convert(ns, goto_trace, xml);
70  status() << xml;
71  }
72  break;
73 
75  {
76  if(status().tellp() > 0)
77  status() << eom; // force end of previous message
78  json_stream_objectt &json_result =
80  const goto_trace_stept &step=goto_trace.steps.back();
81  json_result["property"] =
82  json_stringt(step.pc->source_location.get_property_id());
83  json_result["description"] =
84  json_stringt(step.pc->source_location.get_comment());
85  json_result["status"]=json_stringt("failed");
86  json_stream_arrayt &json_trace =
87  json_result.push_back_stream_array("trace");
88  convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options());
89  }
90  break;
91  }
92 }
93 
96 {
97  const std::string graphml=options.get_option("graphml-witness");
98  if(graphml.empty())
99  return;
100 
101  graphml_witnesst graphml_witness(ns);
103  graphml_witness(safety_checkert::error_trace);
104  else if(result==resultt::SAFE)
105  graphml_witness(equation);
106  else
107  return;
108 
109  if(graphml=="-")
110  write_graphml(graphml_witness.graph(), std::cout);
111  else
112  {
113  std::ofstream out(graphml);
114  write_graphml(graphml_witness.graph(), out);
115  }
116 }
117 
119 {
120  status() << "converting SSA" << eom;
121 
122  // convert SSA
124 
125  // hook for cegis to freeze synthesis program vars
127 }
128 
131 {
132  status() << "Passing problem to "
134 
136 
137  auto solver_start = std::chrono::steady_clock::now();
138 
139  do_conversion();
140 
141  status() << "Running " << prop_conv.decision_procedure_text() << eom;
142 
144 
145  {
146  auto solver_stop = std::chrono::steady_clock::now();
147  status() << "Runtime decision procedure: "
148  << std::chrono::duration<double>(solver_stop-solver_start).count()
149  << "s" << eom;
150  }
151 
152  return dec_result;
153 }
154 
156 {
158 }
159 
161 {
162  log.result() << log.bold << "VERIFICATION SUCCESSFUL" << log.reset << log.eom;
163 
164  switch(handler.get_ui())
165  {
167  break;
168 
170  {
171  xmlt xml("cprover-status");
172  xml.data="SUCCESS";
173  log.result() << xml;
174  }
175  break;
176 
178  {
179  json_objectt json_result;
180  json_result["cProverStatus"]=json_stringt("success");
181  log.result() << json_result;
182  }
183  break;
184  }
185 }
186 
188 {
190 }
191 
193 {
194  log.result() << log.bold << "VERIFICATION FAILED" << log.reset << log.eom;
195 
196  switch(handler.get_ui())
197  {
199  break;
200 
202  {
203  xmlt xml("cprover-status");
204  xml.data="FAILURE";
205  log.result() << xml;
206  }
207  break;
208 
210  {
211  json_objectt json_result;
212  json_result["cProverStatus"]=json_stringt("failure");
213  log.result() << json_result;
214  }
215  break;
216  }
217 }
218 
220 {
221  const std::string mm=options.get_option("mm");
222 
223  if(mm.empty() || mm=="sc")
224  memory_model=util_make_unique<memory_model_sct>(ns);
225  else if(mm=="tso")
226  memory_model=util_make_unique<memory_model_tsot>(ns);
227  else if(mm=="pso")
228  memory_model=util_make_unique<memory_model_psot>(ns);
229  else
230  {
232  "invalid parameter " + mm, "--mm", "try values of sc, tso, pso");
233  }
234 }
235 
237 {
239 
240  {
241  const symbolt *init_symbol;
242  if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
243  symex.language_mode=init_symbol->mode;
244  }
245 
246  status() << "Starting Bounded Model Checking" << eom;
247 
249 
252 }
253 
255  abstract_goto_modelt &goto_model)
256 {
257  try
258  {
259  auto get_goto_function = [&goto_model](const irep_idt &id) ->
261  {
262  return goto_model.get_goto_function(id);
263  };
264 
265  perform_symbolic_execution(get_goto_function);
266 
267  // Borrow a reference to the goto functions map. This reference, or
268  // iterators pointing into it, must not be stored by this function or its
269  // callees, as goto_model.get_goto_function (as used by symex)
270  // will have side-effects on it.
271  const goto_functionst &goto_functions =
272  goto_model.get_goto_functions();
273 
274  // This provides the driver program the opportunity to do things like a
275  // symbol-table or goto-functions dump instead of actually running the
276  // checker, like show-vcc except driver-program specific.
277  // In particular clients that use symex-driven program loading need to print
278  // GOTO functions after symex, as function bodies are not produced until
279  // symex first requests them.
281  return safety_checkert::resultt::SAFE; // to indicate non-error
282 
283  if(equation.has_threads())
284  {
285  // When doing path exploration in a concurrent setting, we should avoid
286  // model-checking the program until we reach the end of a path.
289 
290  // add a partial ordering, if required
291  memory_model->set_message_handler(get_message_handler());
292  (*memory_model)(equation);
293  }
294 
295  statistics() << "size of program expression: "
296  << equation.SSA_steps.size()
297  << " steps" << eom;
298 
299  slice();
300 
301  // coverage report
302  std::string cov_out=options.get_option("symex-coverage-report");
303  if(!cov_out.empty() &&
304  symex.output_coverage_report(goto_functions, cov_out))
305  {
306  error() << "Failed to write symex coverage report" << eom;
308  }
309 
310  if(options.get_bool_option("show-vcc"))
311  {
313  return safety_checkert::resultt::SAFE; // to indicate non-error
314  }
315 
316  if(!options.get_list_option("cover").empty())
317  {
318  return cover(goto_functions)?
320  }
321 
322  if(options.get_option("localize-faults")!="")
323  {
324  fault_localizationt fault_localization(
325  goto_functions, *this, options);
326  return fault_localization();
327  }
328 
329  // any properties to check at all?
330  if(
331  !options.get_bool_option("program-only") &&
332  symex.get_remaining_vccs() == 0)
333  {
334  if(options.is_set("paths"))
336  report_success();
339  }
340 
341  if(options.get_bool_option("program-only"))
342  {
345  }
346 
347  if(!options.is_set("paths") || symex.path_segment_vccs > 0)
348  return decide(goto_functions, prop_conv);
349 
351  }
352 
353  catch(const std::string &error_str)
354  {
355  messaget message(get_message_handler());
357  message.error() << error_str << messaget::eom;
358 
360  }
361 
362  catch(const char *error_str)
363  {
364  messaget message(get_message_handler());
366  message.error() << error_str << messaget::eom;
367 
369  }
370 
371  catch(const std::bad_alloc &)
372  {
373  error() << "Out of memory" << eom;
375  }
376 }
377 
379 {
380  if(options.get_option("slice-by-trace")!="")
381  {
382  symex_slice_by_tracet symex_slice_by_trace(ns);
383 
384  symex_slice_by_trace.slice_by_trace
385  (options.get_option("slice-by-trace"),
386  equation);
387  }
388  // any properties to check at all?
389  if(equation.has_threads())
390  {
391  // we should build a thread-aware SSA slicer
392  statistics() << "no slicing due to threads" << eom;
393  }
394  else
395  {
396  if(options.get_bool_option("slice-formula"))
397  {
398  ::slice(equation);
399  statistics() << "slicing removed "
401  << " assignments"<<eom;
402  }
403  else
404  {
405  if(options.get_list_option("cover").empty())
406  {
408  statistics() << "simple slicing removed "
410  << " assignments"<<eom;
411  }
412  }
413  }
414  statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
416  << " remaining after simplification" << eom;
417 
418  if(options.is_set("paths"))
419  statistics() << "Generated " << symex.path_segment_vccs
420  << " new VCC(s) along current path segment" << eom;
421 }
422 
424  abstract_goto_modelt &goto_model)
425 {
426  setup();
427 
428  return execute(goto_model);
429 }
430 
432  const goto_functionst &goto_functions,
433  prop_convt &prop_conv)
434 {
436 
437  if(options.get_bool_option("stop-on-fail"))
438  return stop_on_fail(prop_conv);
439  else
440  return all_properties(goto_functions, prop_conv);
441 }
442 
444 {
445  if(options.get_bool_option("show-vcc"))
446  {
448  }
449 
450  if(options.get_bool_option("program-only"))
451  {
453  }
454 }
455 
457 {
459  {
461  report_success();
463  return resultt::SAFE;
464 
466  if(options.get_bool_option("trace"))
467  {
468  if(options.get_bool_option("beautify"))
470  dynamic_cast<boolbvt &>(prop_conv), equation);
471 
472  error_trace();
474  }
475 
476  report_failure();
477  return resultt::UNSAFE;
478 
479  default:
480  if(options.get_bool_option("dimacs") ||
481  options.get_option("outfile")!="")
482  return resultt::SAFE;
483 
484  error() << "decision procedure failed" << eom;
485 
486  return resultt::ERROR;
487  }
488 }
489 
496 // creating those function bodies on demand.
503  const path_strategy_choosert &path_strategy_chooser,
504  const optionst &opts,
505  abstract_goto_modelt &model,
507  std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
508  std::function<bool(void)> callback_after_symex)
509 {
512  const symbol_tablet &symbol_table = model.get_symbol_table();
513  messaget message(ui);
514  std::unique_ptr<path_storaget> worklist;
515  std::string strategy = opts.get_option("exploration-strategy");
516  INVARIANT(
517  path_strategy_chooser.is_valid_strategy(strategy),
518  "Front-end passed us invalid path strategy '" + strategy + "'");
519  worklist = path_strategy_chooser.get(strategy);
520  try
521  {
522  {
523  solver_factoryt solvers(
524  opts,
525  symbol_table,
526  ui,
528  std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
529  solvers.get_solver();
530  prop_convt &pc = cbmc_solver->prop_conv();
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);
535 
536  if(
537  tmp_result == safety_checkert::resultt::UNSAFE &&
538  opts.get_bool_option("stop-on-fail") && opts.is_set("paths"))
539  {
540  worklist->clear();
542  }
543 
544  if(tmp_result != safety_checkert::resultt::PAUSED)
545  final_result = tmp_result;
546  }
547  INVARIANT(
548  opts.get_bool_option("paths") || worklist->empty(),
549  "the worklist should be empty after doing full-program "
550  "model checking, but the worklist contains " +
551  std::to_string(worklist->size()) + " unexplored branches.");
552 
553  // When model checking, the bmc.run() above will already have explored
554  // the entire program, and final_result contains the verification result.
555  // The worklist (containing paths that have not yet been explored) is thus
556  // empty, and we don't enter this loop.
557  //
558  // When doing path exploration, there will be some saved paths left to
559  // explore in the worklist. We thus need to run the above code again,
560  // once for each saved path in the worklist, to continue symbolically
561  // execute the program. Note that the code in the loop is similar to
562  // the code above except that we construct a path_explorert rather than
563  // a bmct, which allows us to execute from a saved state rather than
564  // from the entry point. See the path_explorert documentation, and the
565  // difference between the implementations of perform_symbolic_exection()
566  // in bmct and path_explorert, for more information.
567 
568  while(!worklist->empty())
569  {
570  solver_factoryt solvers(
571  opts,
572  symbol_table,
573  ui,
575  std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
576  solvers.get_solver();
577  prop_convt &pc = cbmc_solver->prop_conv();
578  path_storaget::patht &resume = worklist->peek();
579  path_explorert pe(
580  opts,
581  symbol_table,
582  ui,
583  pc,
584  resume.equation,
585  resume.state,
586  *worklist,
587  callback_after_symex);
588  if(driver_configure_bmc)
589  driver_configure_bmc(pe, symbol_table);
590  tmp_result = pe.run(model);
591 
592  if(
593  tmp_result == safety_checkert::resultt::UNSAFE &&
594  opts.get_bool_option("stop-on-fail") && opts.is_set("paths"))
595  {
596  worklist->clear();
598  }
599 
600  if(tmp_result != safety_checkert::resultt::PAUSED)
601  final_result &= tmp_result;
602  worklist->pop();
603  }
604  }
605  catch(const char *error_msg)
606  {
607  message.error() << error_msg << message.eom;
608  return CPROVER_EXIT_EXCEPTION;
609  }
610  catch(const std::string &error_msg)
611  {
612  message.error() << error_msg << message.eom;
613  return CPROVER_EXIT_EXCEPTION;
614  }
615  catch(std::runtime_error &e)
616  {
617  message.error() << e.what() << message.eom;
618  return CPROVER_EXIT_EXCEPTION;
619  }
620 
621  switch(final_result)
622  {
624  if(opts.is_set("paths"))
625  report_success(message, ui);
628  if(opts.is_set("paths"))
629  report_failure(message, ui);
634  UNREACHABLE;
635  }
636  UNREACHABLE;
637 }
638 
640  goto_symext::get_goto_functiont get_goto_function)
641 {
643 
644  if(options.get_bool_option("validate-ssa-equation"))
645  {
647  }
648 
649  INVARIANT(
651  "Branch points were saved even though we should have been "
652  "executing the entire program and merging paths");
653 }
654 
656  goto_symext::get_goto_functiont get_goto_function)
657 {
659  get_goto_function, saved_state, &equation, symex_symbol_table);
660 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
graphml_witnesst::graph
const graphmlt & graph()
Definition: graphml_witness.h:32
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
fault_localization.h
slice_by_trace.h
show_program
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Definition: show_program.cpp:20
bmct::decide
virtual resultt decide(const goto_functionst &, prop_convt &)
Definition: bmc.cpp:431
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
path_strategy_choosert::get
std::unique_ptr< path_storaget > get(const std::string strategy) const
Factory for a path_storaget.
Definition: path_storage.h:147
path_explorert::perform_symbolic_execution
void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override
Resume symbolic execution from saved branch point.
Definition: bmc.cpp:655
bmct::run
virtual resultt run(const goto_functionst &goto_functions)
Definition: bmc.h:91
abstract_goto_modelt::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
path_storaget::empty
bool empty() const
Is this storage empty?
Definition: path_storage.h:83
bmct::trace_options
trace_optionst trace_options()
Definition: bmc.h:191
CPROVER_EXIT_VERIFICATION_UNSAFE
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
Definition: exit_codes.h:25
ui_message_handlert
Definition: ui_message.h:19
bmct
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
path_storaget::peek
patht & peek()
Reference to the next path to resume.
Definition: path_storage.h:47
bmct::cover
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
Definition: bmc_cover.cpp:425
bmct::report_success
virtual void report_success()
Definition: bmc.cpp:155
build_goto_trace
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)
Definition: build_goto_trace.cpp:166
memory_model_pso.h
bmct::output_graphml
void output_graphml(resultt result)
outputs witnesses in graphml format
Definition: bmc.cpp:95
symex_target_equationt::convert
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:366
ui_message_handlert::uit::XML_UI
@ XML_UI
symex_bmct::unwindset
unwindsett unwindset
Definition: symex_bmc.h:85
bmct::get_memory_model
void get_memory_model()
Definition: bmc.cpp:219
optionst
Definition: options.h:22
show_vcc.h
irept::make_nil
void make_nil()
Definition: irep.h:315
goto_symext::get_total_vccs
unsigned get_total_vccs()
Definition: goto_symex.h:453
prop_convt
Definition: prop_conv.h:27
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
safety_checkert::resultt::PAUSED
@ PAUSED
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
messaget::status
mstreamt & status() const
Definition: message.h:401
safety_checkert::resultt::SAFE
@ SAFE
No safety properties were violated.
goto_symext::resume_symex_from_saved_state
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...
Definition: symex_main.cpp:273
bmct::memory_model
std::unique_ptr< memory_model_baset > memory_model
Definition: bmc.h:176
unwindsett::parse_unwindset
void parse_unwindset(const std::string &unwindset)
Definition: unwindset.cpp:24
xml
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
counterexample_beautificationt
Definition: counterexample_beautification.h:21
goto_tracet::steps
stepst steps
Definition: goto_trace.h:154
bmct::show
void show()
Definition: bmc.cpp:443
simple_slice
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:239
CPROVER_EXIT_EXCEPTION
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:41
CPROVER_EXIT_VERIFICATION_SAFE
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
Definition: exit_codes.h:21
path_storaget::pop
void pop()
Remove the next path to resume from the storage.
Definition: path_storage.h:73
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
messaget::eom
static eomt eom
Definition: message.h:284
goto_trace_stept
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
bmct::slice
void slice()
Definition: bmc.cpp:378
solver_factoryt
Definition: solver_factory.h:28
bmct::symex
symex_bmct symex
Definition: bmc.h:174
bmct::run_decision_procedure
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Definition: bmc.cpp:130
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
bmct::path_storage
path_storaget & path_storage
Definition: bmc.h:173
goto_symext::path_segment_vccs
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
Definition: goto_symex.h:439
unwindsett::parse_unwind
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:18
bmct::error_trace
virtual void error_trace()
Definition: bmc.cpp:51
json_objectt
Definition: json.h:244
json_stream_objectt::push_back_stream_array
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
Definition: json_stream.cpp:120
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
symex_bmct::output_coverage_report
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:76
bmct::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: bmc.h:178
bmct::perform_symbolic_execution
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
Definition: bmc.cpp:639
path_storaget::patht::equation
symex_target_equationt equation
Definition: path_storage.h:30
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
solver_factoryt::get_solver
virtual std::unique_ptr< solvert > get_solver()
Definition: solver_factory.h:102
convert
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: builtin_factory.cpp:41
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::result
mstreamt & result() const
Definition: message.h:396
messaget::error
mstreamt & error() const
Definition: message.h:386
messaget::bold
static const commandt bold
render text with bold font
Definition: message.h:369
bmct::ns
namespacet ns
Definition: bmc.h:171
path_explorert
Symbolic execution from a saved branch point.
Definition: bmc.h:248
ui_message_handlert::uit::JSON_UI
@ JSON_UI
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
ui_message_handlert::get_json_stream
json_stream_arrayt & get_json_stream()
Definition: ui_message.h:37
language_util.h
safety_checkert::error_trace
goto_tracet error_trace
Definition: safety_checker.h:54
optionst::is_set
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:60
bmct::options
const optionst & options
Definition: bmc.h:166
bmct::stop_on_fail
virtual resultt stop_on_fail(prop_convt &solver)
Definition: bmc.cpp:456
xml_goto_trace.h
goto_symext::symex_from_entry_point_of
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
Definition: symex_main.cpp:295
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
decision_proceduret::dec_solve
virtual resultt dec_solve()=0
goto_trace_stept::pc
goto_programt::const_targett pc
Definition: goto_trace.h:92
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
bmct::prop_conv
prop_convt & prop_conv
Definition: bmc.h:175
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
path_storaget::clear
virtual void clear()=0
Clear all saved paths.
solver_factory.h
bmct::execute
safety_checkert::resultt execute(abstract_goto_modelt &)
Definition: bmc.cpp:254
json_goto_trace.h
graphml_witness.h
bmct::setup
void setup()
Definition: bmc.cpp:236
safety_checkert::resultt::ERROR
@ ERROR
Safety is unknown due to an error during safety checking.
bmc.h
xmlt
Definition: xml.h:18
path_storaget::patht
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:28
goto_symext::get_remaining_vccs
unsigned get_remaining_vccs()
Definition: goto_symex.h:462
safety_checkert::resultt::UNSAFE
@ UNSAFE
Some safety properties were violated.
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
symex_target_equationt::has_threads
bool has_threads() const
Definition: symex_target_equation.h:389
path_explorert::saved_state
const goto_symex_statet & saved_state
Definition: bmc.h:273
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
json_stream_arrayt::push_back_stream_object
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
bmct::do_language_agnostic_bmc
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).
Definition: bmc.cpp:502
decision_proceduret::decision_procedure_text
virtual std::string decision_procedure_text() const =0
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:139
ui_message_handlert::get_ui
uit get_ui() const
Definition: ui_message.h:30
symex_target_equationt::count_ignored_SSA_steps
std::size_t count_ignored_SSA_steps() const
Definition: symex_target_equation.h:357
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
safety_checkert::resultt
resultt
Definition: safety_checker.h:33
symex_slice_by_tracet::slice_by_trace
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
Definition: slice_by_trace.cpp:28
abstract_goto_modelt::get_goto_functions
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
bmct::driver_callback_after_symex
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:235
bmct::symex_symbol_table
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
Definition: bmc.h:170
goto_symext::validate
void validate(const namespacet &ns, const validation_modet vm) const
Definition: goto_symex.h:471
write_graphml
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:212
show_goto_trace
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:748
show_vcc
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Definition: show_vcc.cpp:161
goto_symext::language_mode
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:197
ui_message_handlert::uit::PLAIN
@ PLAIN
path_storaget::patht::state
goto_symex_statet state
Definition: path_storage.h:31
symbolt
Symbol table entry.
Definition: symbol.h:27
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
exit_codes.h
abstract_goto_modelt::get_goto_function
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.
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
bmct::all_properties
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
Definition: all_properties.cpp:294
bmct::equation
symex_target_equationt equation
Definition: bmc.h:172
symex_slice_by_tracet
Definition: slice_by_trace.h:17
build_goto_trace.h
path_strategy_choosert::is_valid_strategy
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
Definition: path_storage.h:138
goto_tracet
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
boolbvt
Definition: boolbv.h:32
fault_localizationt
Definition: fault_localization.h:24
goto_symext::get_goto_functiont
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:109
counterexample_beautification.h
path_strategy_choosert
Factory and information for path_storaget.
Definition: path_storage.h:129
bmct::report_failure
virtual void report_failure()
Definition: bmc.cpp:187
show_program.h
bmct::freeze_program_variables
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:46
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:19
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:46
static_lifetime_init.h
graphml_witnesst
Definition: graphml_witness.h:21
xmlt::data
std::string data
Definition: xml.h:30
slice.h
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:37
path_storaget::size
virtual std::size_t size() const =0
How many paths does this storage contain?
symex_bmct::last_source_location
source_locationt last_source_location
Definition: symex_bmc.h:36
bmct::do_conversion
void do_conversion()
Definition: bmc.cpp:118
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:78
solver_factoryt::solvert::prop_conv
prop_convt & prop_conv() const
Definition: solver_factory.h:68
validation_modet::INVARIANT
@ INVARIANT
messaget::statistics
mstreamt & statistics() const
Definition: message.h:406
json_stringt
Definition: json.h:214
goto_symext::should_pause_symex
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:162