cprover
bmc_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking Utilities
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "bmc_util.h"
13 
14 #include <iostream>
15 
19 
22 #include <goto-symex/slice.h>
24 
26 
28 
29 #include <util/json_stream.h>
30 #include <util/make_unique.h>
31 #include <util/ui_message.h>
32 
34 #include "symex_bmc.h"
35 
37 {
38  log.status() << "Building error trace" << messaget::eom;
39 }
40 
42  goto_tracet &goto_trace,
43  const namespacet &ns,
44  const symex_target_equationt &symex_target_equation,
45  const decision_proceduret &decision_procedure,
46  ui_message_handlert &ui_message_handler)
47 {
48  messaget log(ui_message_handler);
50 
51  build_goto_trace(symex_target_equation, decision_procedure, ns, goto_trace);
52 }
53 
56 {
57  return [property_id](
58  symex_target_equationt::SSA_stepst::const_iterator step,
59  const decision_proceduret &decision_procedure) {
60  return step->is_assert() && step->get_property_id() == property_id &&
61  decision_procedure.get(step->cond_handle).is_false();
62  };
63 }
64 
66  const goto_tracet &goto_trace,
67  const namespacet &ns,
68  const trace_optionst &trace_options,
69  ui_message_handlert &ui_message_handler)
70 {
71  messaget msg(ui_message_handler);
72  switch(ui_message_handler.get_ui())
73  {
75  msg.result() << "Counterexample:" << messaget::eom;
76  show_goto_trace(msg.result(), ns, goto_trace, trace_options);
77  msg.result() << messaget::eom;
78  break;
79 
81  {
82  const goto_trace_stept &last_step = goto_trace.get_last_step();
83  property_infot info{
84  last_step.pc, last_step.comment, property_statust::FAIL};
85  xmlt xml_result = xml(last_step.property_id, info);
86  convert(ns, goto_trace, xml_result.new_element());
87  msg.result() << xml_result;
88  }
89  break;
90 
92  {
93  json_stream_objectt &json_result =
94  ui_message_handler.get_json_stream().push_back_stream_object();
95  const goto_trace_stept &step = goto_trace.get_last_step();
96  json_result["property"] = json_stringt(step.property_id);
97  json_result["description"] = json_stringt(step.comment);
98  json_result["status"] = json_stringt("failed");
99  json_stream_arrayt &json_trace =
100  json_result.push_back_stream_array("trace");
101  convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
102  }
103  break;
104  }
105 }
106 
109  const goto_tracet &goto_trace,
110  const namespacet &ns,
111  const optionst &options)
112 {
113  const std::string graphml = options.get_option("graphml-witness");
114  if(graphml.empty())
115  return;
116 
117  graphml_witnesst graphml_witness(ns);
118  graphml_witness(goto_trace);
119 
120  if(graphml == "-")
121  write_graphml(graphml_witness.graph(), std::cout);
122  else
123  {
124  std::ofstream out(graphml);
125  write_graphml(graphml_witness.graph(), out);
126  }
127 }
128 
131  const symex_target_equationt &symex_target_equation,
132  const namespacet &ns,
133  const optionst &options)
134 {
135  const std::string graphml = options.get_option("graphml-witness");
136  if(graphml.empty())
137  return;
138 
139  graphml_witnesst graphml_witness(ns);
140  graphml_witness(symex_target_equation);
141 
142  if(graphml == "-")
143  write_graphml(graphml_witness.graph(), std::cout);
144  else
145  {
146  std::ofstream out(graphml);
147  write_graphml(graphml_witness.graph(), out);
148  }
149 }
150 
152  symex_target_equationt &equation,
153  decision_proceduret &decision_procedure,
154  message_handlert &message_handler)
155 {
156  messaget msg(message_handler);
157  msg.status() << "converting SSA" << messaget::eom;
158 
159  equation.convert(decision_procedure);
160 }
161 
162 std::unique_ptr<memory_model_baset>
163 get_memory_model(const optionst &options, const namespacet &ns)
164 {
165  const std::string mm = options.get_option("mm");
166 
167  if(mm.empty() || mm == "sc")
168  return util_make_unique<memory_model_sct>(ns);
169  else if(mm == "tso")
170  return util_make_unique<memory_model_tsot>(ns);
171  else if(mm == "pso")
172  return util_make_unique<memory_model_psot>(ns);
173  else
174  {
175  throw "invalid memory model '" + mm + "': use one of sc, tso, pso";
176  }
177 }
178 
180  symex_bmct &symex,
181  const namespacet &ns,
182  const optionst &options,
183  ui_message_handlert &ui_message_handler)
184 {
185  messaget msg(ui_message_handler);
186  const symbolt *init_symbol;
187  if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
188  symex.language_mode = init_symbol->mode;
189 
190  msg.status() << "Starting Bounded Model Checking" << messaget::eom;
191 
193 
194  symex.unwindset.parse_unwind(options.get_option("unwind"));
195  symex.unwindset.parse_unwindset(options.get_list_option("unwindset"));
196 }
197 
198 void slice(
199  symex_bmct &symex,
200  symex_target_equationt &symex_target_equation,
201  const namespacet &ns,
202  const optionst &options,
203  ui_message_handlert &ui_message_handler)
204 {
205  messaget msg(ui_message_handler);
206 
207  // any properties to check at all?
208  if(symex_target_equation.has_threads())
209  {
210  // we should build a thread-aware SSA slicer
211  msg.statistics() << "no slicing due to threads" << messaget::eom;
212  }
213  else
214  {
215  if(options.get_bool_option("slice-formula"))
216  {
217  ::slice(symex_target_equation);
218  msg.statistics() << "slicing removed "
219  << symex_target_equation.count_ignored_SSA_steps()
220  << " assignments" << messaget::eom;
221  }
222  else
223  {
224  if(options.get_bool_option("simple-slice"))
225  {
226  simple_slice(symex_target_equation);
227  msg.statistics() << "simple slicing removed "
228  << symex_target_equation.count_ignored_SSA_steps()
229  << " assignments" << messaget::eom;
230  }
231  }
232  }
233  msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
234  << symex.get_remaining_vccs()
235  << " remaining after simplification" << messaget::eom;
236 }
237 
239  propertiest &properties,
240  std::unordered_set<irep_idt> &updated_properties,
241  const symex_target_equationt &equation)
242 {
243  for(const auto &step : equation.SSA_steps)
244  {
245  if(!step.is_assert())
246  continue;
247 
248  irep_idt property_id = step.get_property_id();
249  CHECK_RETURN(!property_id.empty());
250 
251  // Don't update status of properties that are constant 'false';
252  // we wouldn't have traces for them.
253  const auto status = step.cond_expr.is_true() ? property_statust::PASS
255  auto emplace_result = properties.emplace(
256  property_id, property_infot{step.source.pc, step.comment, status});
257 
258  if(emplace_result.second)
259  {
260  updated_properties.insert(property_id);
261  }
262  else
263  {
264  property_infot &property_info = emplace_result.first->second;
265  property_statust old_status = property_info.status;
266  property_info.status |= status;
267 
268  if(property_info.status != old_status)
269  updated_properties.insert(property_id);
270  }
271  }
272 }
273 
275  propertiest &properties,
276  std::unordered_set<irep_idt> &updated_properties)
277 {
278  for(auto &property_pair : properties)
279  {
280  if(property_pair.second.status == property_statust::NOT_CHECKED)
281  {
282  // This could be a NOT_CHECKED, NOT_REACHABLE or PASS,
283  // but the equation doesn't give us precise information.
284  property_pair.second.status = property_statust::PASS;
285  updated_properties.insert(property_pair.first);
286  }
287  }
288 }
289 
291  propertiest &properties,
292  std::unordered_set<irep_idt> &updated_properties)
293 {
294  for(auto &property_pair : properties)
295  {
296  if(property_pair.second.status == property_statust::UNKNOWN)
297  {
298  // This could have any status except NOT_CHECKED.
299  // We consider them PASS because we do verification modulo bounds.
300  property_pair.second.status = property_statust::PASS;
301  updated_properties.insert(property_pair.first);
302  }
303  }
304 }
305 
307  const std::string &cov_out,
308  const abstract_goto_modelt &goto_model,
309  const symex_bmct &symex,
310  ui_message_handlert &ui_message_handler)
311 {
312  if(
313  !cov_out.empty() &&
314  symex.output_coverage_report(goto_model.get_goto_functions(), cov_out))
315  {
316  messaget log(ui_message_handler);
317  log.error() << "Failed to write symex coverage report to '" << cov_out
318  << "'" << messaget::eom;
319  }
320 }
321 
323  symex_bmct &symex,
324  symex_target_equationt &equation,
325  const optionst &options,
326  const namespacet &ns,
327  ui_message_handlert &ui_message_handler)
328 {
329  const auto postprocess_equation_start = std::chrono::steady_clock::now();
330  // add a partial ordering, if required
331  if(equation.has_threads())
332  {
333  std::unique_ptr<memory_model_baset> memory_model =
334  get_memory_model(options, ns);
335  (*memory_model)(equation, ui_message_handler);
336  }
337 
338  messaget log(ui_message_handler);
339  log.statistics() << "size of program expression: "
340  << equation.SSA_steps.size() << " steps" << messaget::eom;
341 
342  slice(symex, equation, ns, options, ui_message_handler);
343 
344  if(options.get_bool_option("validate-ssa-equation"))
345  {
347  }
348 
349  const auto postprocess_equation_stop = std::chrono::steady_clock::now();
350  std::chrono::duration<double> postprocess_equation_runtime =
351  std::chrono::duration<double>(
352  postprocess_equation_stop - postprocess_equation_start);
353  log.status() << "Runtime Postprocess Equation: "
354  << postprocess_equation_runtime.count() << "s" << messaget::eom;
355 }
356 
357 std::chrono::duration<double> prepare_property_decider(
358  propertiest &properties,
359  symex_target_equationt &equation,
360  goto_symex_property_decidert &property_decider,
361  ui_message_handlert &ui_message_handler)
362 {
363  auto solver_start = std::chrono::steady_clock::now();
364 
365  messaget log(ui_message_handler);
366  log.status()
367  << "Passing problem to "
368  << property_decider.get_decision_procedure().decision_procedure_text()
369  << messaget::eom;
370 
372  equation, property_decider.get_decision_procedure(), ui_message_handler);
374  properties);
375  property_decider.convert_goals();
376 
377  auto solver_stop = std::chrono::steady_clock::now();
378  return std::chrono::duration<double>(solver_stop - solver_start);
379 }
380 
383  propertiest &properties,
384  goto_symex_property_decidert &property_decider,
385  ui_message_handlert &ui_message_handler,
386  std::chrono::duration<double> solver_runtime,
387  bool set_pass)
388 {
389  auto solver_start = std::chrono::steady_clock::now();
390 
391  messaget log(ui_message_handler);
392  log.status()
393  << "Running "
394  << property_decider.get_decision_procedure().decision_procedure_text()
395  << messaget::eom;
396 
397  property_decider.add_constraint_from_goals(
398  [&properties](const irep_idt &property_id) {
399  return is_property_to_check(properties.at(property_id).status);
400  });
401 
402  auto const sat_solver_start = std::chrono::steady_clock::now();
403 
404  decision_proceduret::resultt dec_result = property_decider.solve();
405 
406  auto const sat_solver_stop = std::chrono::steady_clock::now();
407  std::chrono::duration<double> sat_solver_runtime =
408  std::chrono::duration<double>(sat_solver_stop - sat_solver_start);
409  log.status() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
410  << messaget::eom;
411 
412  property_decider.update_properties_status_from_goals(
413  properties, result.updated_properties, dec_result, set_pass);
414 
415  auto solver_stop = std::chrono::steady_clock::now();
416  solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
417  log.status() << "Runtime decision procedure: " << solver_runtime.count()
418  << "s" << messaget::eom;
419 
421  {
423  }
424 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
graphml_witnesst::graph
const graphmlt & graph()
Definition: graphml_witness.h:34
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
symex_target_equation.h
Generate Equation using Symbolic Execution.
update_status_of_unknown_properties
void update_status_of_unknown_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of UNKNOWN properties to PASS.
Definition: bmc_util.cpp:290
postprocess_equation
void postprocess_equation(symex_bmct &symex, symex_target_equationt &equation, const optionst &options, const namespacet &ns, ui_message_handlert &ui_message_handler)
Post process the equation.
Definition: bmc_util.cpp:322
message_building_error_trace
void message_building_error_trace(messaget &log)
Outputs a message that an error trace is being built.
Definition: bmc_util.cpp:36
property_statust
property_statust
The status of a property.
Definition: properties.h:26
goto_trace_stept::comment
std::string comment
Definition: goto_trace.h:123
build_goto_trace
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace)
Build a trace by going through the steps of target and stopping after the step matching a given condi...
Definition: build_goto_trace.cpp:204
output_graphml
void output_graphml(const goto_tracet &goto_trace, const namespacet &ns, const optionst &options)
outputs an error witness in graphml format
Definition: bmc_util.cpp:108
ui_message_handlert
Definition: ui_message.h:22
ssa_step_predicatet
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
Definition: build_goto_trace.h:48
incremental_goto_checkert::resultt
Definition: incremental_goto_checker.h:43
memory_model_pso.h
Memory models for partial order concurrency.
ui_message_handlert::uit::XML_UI
@ XML_UI
symex_bmct::unwindset
unwindsett unwindset
Definition: symex_bmc.h:84
optionst
Definition: options.h:23
irept::make_nil
void make_nil()
Definition: irep.h:465
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::status
mstreamt & status() const
Definition: message.h:414
decision_proceduret
Definition: decision_procedure.h:21
json_stream.h
update_status_of_not_checked_properties
void update_status_of_not_checked_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of NOT_CHECKED properties to PASS.
Definition: bmc_util.cpp:274
goto_symex_property_decider.h
Property Decider for Goto-Symex.
simple_slice
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:234
incremental_goto_checkert::resultt::progresst::FOUND_FAIL
@ FOUND_FAIL
The goto checker may be able to find another FAILed property if operator() is called again.
messaget::eom
static eomt eom
Definition: message.h:297
goto_symex_property_decidert::solve
decision_proceduret::resultt solve()
Calls solve() on the solver instance.
Definition: goto_symex_property_decider.cpp:101
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
decision_procedure.h
Decision Procedure Interface.
unwindsett::parse_unwind
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:20
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:33
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:74
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
ui_message_handlert::get_json_stream
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:40
bmc_util.h
Bounded Model Checking Utilities.
property_infot::status
property_statust status
The status of the property.
Definition: properties.h:72
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
build_error_trace
void build_error_trace(goto_tracet &goto_trace, const namespacet &ns, const symex_target_equationt &symex_target_equation, const decision_proceduret &decision_procedure, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:41
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
update_properties_status_from_symex_target_equation
void update_properties_status_from_symex_target_equation(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
Sets property status to PASS for properties whose conditions are constant true in the equation.
Definition: bmc_util.cpp:238
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::result
mstreamt & result() const
Definition: message.h:409
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:399
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:107
ui_message_handlert::uit::JSON_UI
@ JSON_UI
goto_symex_property_decidert::convert_goals
void convert_goals()
Convert the instances of a property into a goal variable.
Definition: goto_symex_property_decider.cpp:71
xml_goto_trace.h
Traces of GOTO Programs.
goto_symext::validate
void validate(const validation_modet vm) const
Definition: goto_symex.h:836
slice
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:198
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
goto_trace_stept::pc
goto_programt::const_targett pc
Definition: goto_trace.h:112
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
get_memory_model
std::unique_ptr< memory_model_baset > get_memory_model(const optionst &options, const namespacet &ns)
Definition: bmc_util.cpp:163
is_property_to_check
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:170
convert_symex_target_equation
void convert_symex_target_equation(symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
Definition: bmc_util.cpp:151
goto_symex_property_decidert::get_decision_procedure
decision_proceduret & get_decision_procedure() const
Returns the solver instance.
Definition: goto_symex_property_decider.cpp:107
message_handlert
Definition: message.h:28
dstringt::empty
bool empty() const
Definition: dstring.h:88
json_goto_trace.h
Traces of GOTO Programs.
graphml_witness.h
Witnesses for Traces and Proofs.
goto_symex_property_decidert::add_constraint_from_goals
void add_constraint_from_goals(std::function< bool(const irep_idt &property_id)> select_property)
Add disjunction of negated selected properties to the equation.
Definition: goto_symex_property_decider.cpp:82
xmlt
Definition: xml.h:21
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
symex_target_equationt::has_threads
bool has_threads() const
Definition: symex_target_equation.h:270
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:34
property_statust::UNKNOWN
@ UNKNOWN
The checker was unable to determine the status of the property.
goto_symex_property_decidert::update_properties_goals_from_symex_target_equation
void update_properties_goals_from_symex_target_equation(propertiest &properties)
Get the conditions for the properties from the equation and collect all 'instances' of the properties...
Definition: goto_symex_property_decider.cpp:43
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
run_property_decider
void run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler, std::chrono::duration< double > solver_runtime, bool set_pass)
Runs the property decider to solve the equation.
Definition: bmc_util.cpp:381
decision_proceduret::decision_procedure_text
virtual std::string decision_procedure_text() const =0
Return a textual description of the decision procedure.
goto_trace_stept::property_id
irep_idt property_id
Definition: goto_trace.h:122
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
symex_target_equationt::count_ignored_SSA_steps
std::size_t count_ignored_SSA_steps() const
Definition: symex_target_equation.h:241
abstract_goto_modelt::get_goto_functions
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
ssa_step_matches_failing_property
ssa_step_predicatet ssa_step_matches_failing_property(const irep_idt &property_id)
Returns a function that checks whether an SSA step is an assertion with property_id.
Definition: bmc_util.cpp:55
property_infot
Definition: properties.h:59
write_graphml
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:205
show_goto_trace
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Output the trace on the given stream out.
Definition: goto_trace.cpp:784
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:226
ui_message_handlert::uit::PLAIN
@ PLAIN
trace_optionst
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:219
setup_symex
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:179
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_symex_property_decidert::update_properties_status_from_goals
void update_properties_status_from_goals(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, decision_proceduret::resultt dec_result, bool set_pass=true) const
Update the property status from the truth value of the goal variable.
Definition: goto_symex_property_decider.cpp:123
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:250
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
symex_target_equationt::convert
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:347
build_goto_trace.h
Traces of GOTO Programs.
output_coverage_report
void output_coverage_report(const std::string &cov_out, const abstract_goto_modelt &goto_model, const symex_bmct &symex, ui_message_handlert &ui_message_handler)
Output a coverage report as generated by symex_coveraget if cov_out is non-empty.
Definition: bmc_util.cpp:306
output_error_trace
void output_error_trace(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:65
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:175
goto_symex_property_decidert
Provides management of goal variables that encode properties.
Definition: goto_symex_property_decider.h:24
unwindsett::parse_unwindset
void parse_unwindset(const std::list< std::string > &unwindset)
Definition: unwindset.cpp:59
incremental_goto_checkert::resultt::progress
progresst progress
Definition: incremental_goto_checker.h:54
incremental_goto_checkert::resultt::updated_properties
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
Definition: incremental_goto_checker.h:61
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
symex_bmct
Definition: symex_bmc.h:24
goto_tracet::get_last_step
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Definition: goto_trace.h:203
static_lifetime_init.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
prepare_property_decider
std::chrono::duration< double > prepare_property_decider(propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler)
Converts the equation and sets up the property decider, but does not call solve.
Definition: bmc_util.cpp:357
graphml_witnesst
Definition: graphml_witness.h:24
goto_symext::get_total_vccs
unsigned get_total_vccs() const
Definition: goto_symex.h:818
slice.h
Slicer for symex traces.
property_infot::pc
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition: properties.h:66
symex_bmct::last_source_location
source_locationt last_source_location
Definition: symex_bmc.h:35
symex_bmc.h
Bounded Model Checking for ANSI-C.
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
goto_symext::get_remaining_vccs
unsigned get_remaining_vccs() const
Definition: goto_symex.h:827
json_stringt
Definition: json.h:270
ui_message.h