Go to the documentation of this file.
54 symex_target_equationt::SSA_stepst::iterator
step;
62 symex_target_equationt::SSA_stepst::iterator step,
77 const std::string &_description,
92 std::vector<exprt> tmp;
109 return loc->source_location.get_property_id();
121 for(
const auto &step : goto_trace.
steps)
132 if(step.io_args.size()==1)
146 symex_target_equationt::SSA_stepst::const_iterator step,
149 return step->is_assume() && prop_conv.
l_get(step->cond_literal).
is_false();
159 goalt &g=goal_pair.second;
191 auto solver_start=std::chrono::steady_clock::now();
199 if(i_it->is_assert())
202 id2string(i_it->source_location.get_comment()),
203 i_it->source_location);
226 goal_map[
id(it->source.pc)].add_instance(it, l_c);
243 "we add coverage for each goal");
251 auto solver_stop=std::chrono::steady_clock::now();
252 status() <<
"Runtime decision procedure: "
253 << std::chrono::duration<double>(solver_stop-solver_start).count()
258 unsigned goals_covered=0;
261 if(g.second.satisfied)
268 result() <<
"\n** coverage results:" <<
eom;
272 const goalt &goal=g.second;
274 result() <<
"[" << g.first <<
"]";
292 for(
const auto &goal_pair :
goal_map)
294 const goalt &goal=goal_pair.second;
296 xmlt xml_result(
"goal");
307 for(
const auto &test :
tests)
309 xmlt xml_result(
"test");
318 for(
const auto &step : test.goto_trace.steps)
324 if(step.io_args.size()==1)
331 for(
const auto &goal_id : test.covered_goals)
348 for(
const auto &goal_pair :
goal_map)
350 const goalt &goal=goal_pair.second;
352 json_result[
"status"] =
363 json_arrayt &tests_array=json_result[
"tests"].make_array();
364 for(
const auto &test :
tests)
369 json_arrayt &json_trace = json_result[
"trace"].make_array();
374 json_arrayt &json_test = json_result[
"inputs"].make_array();
376 for(
const auto &step : test.goto_trace.steps)
382 if(step.io_args.size()==1)
384 json(step.io_args.front(),
bmc.
ns, ID_unknown);
390 for(
const auto &goal_id : test.covered_goals)
400 status() <<
"** " << goals_covered
401 <<
" of " <<
goal_map.size() <<
" covered ("
402 << std::fixed << std::setw(1) << std::setprecision(1)
413 result() <<
"Test suite:" <<
'\n';
415 for(
const auto &test :
tests)
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.
const irep_idt & get_function() const
static bool is_failed_assumption_step(symex_target_equationt::SSA_stepst::const_iterator step, const prop_convt &prop_conv)
#define PRECONDITION(CONDITION)
trace_optionst trace_options()
json_objectt json(const source_locationt &location)
irep_idt id(goto_programt::const_targett loc)
Bounded model checking or path exploration for goto-programs.
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
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)
mstreamt & status() const
const goto_functionst & goto_functions
virtual void satisfying_assignment()
xmlt xml(const source_locationt &location)
Base class for all expressions.
goalt(const std::string &_description, const source_locationt &_source_location)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
json_objectt & make_object()
Try to cover some given set of goals incrementally.
std::map< irep_idt, goalt > goal_mapt
symex_target_equationt::SSA_stepst::iterator step
unsigned iterations() const
ui_message_handlert & ui_message_handler
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::vector< irep_idt > covered_goals
mstreamt & result() const
const std::string & id2string(const irep_idt &d)
json_stream_arrayt & get_json_stream()
virtual literalt convert(const exprt &expr)=0
void register_observer(observert &o)
virtual void set_message_handler(message_handlert &_message_handler)
goalst::size_type size() const
virtual tvt l_get(literalt a) const =0
std::vector< testt > testst
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
void add(const literalt condition)
virtual std::string decision_procedure_text() const =0
Provides methods for streaming JSON objects.
A collection of goto functions.
message_handlert & get_message_handler()
void add_instance(symex_target_equationt::SSA_stepst::iterator step, literalt condition)
bmc_covert(const goto_functionst &_goto_functions, bmct &_bmc)
void set_attribute(const std::string &attribute, unsigned value)
bool get_bool_option(const std::string &option) const
symex_target_equationt equation
source_locationt source_location
std::vector< instancet > instancest
#define forall_goto_functions(it, functions)
instructionst::const_iterator const_targett
std::string get_test(const goto_tracet &goto_trace) const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
jsont & push_back(const jsont &json)
#define forall_goto_program_instructions(it, program)
xmlt & new_element(const std::string &key)
mstreamt & statistics() const