53 symex_target_equationt::SSA_stepst::iterator
step;
61 symex_target_equationt::SSA_stepst::iterator step,
76 const std::string &_description,
91 std::vector<exprt> tmp;
108 return loc->source_location.get_property_id();
120 for(
const auto &step : goto_trace.
steps)
131 if(step.io_args.size()==1)
151 goalt &g=goal_pair.second;
178 for(goto_tracet::stepst::iterator
179 s_it1=goto_trace.steps.begin();
180 s_it1!=goto_trace.steps.end();
182 if(s_it1->is_assume() && !s_it1->cond_value)
184 goto_trace.
steps.erase(++s_it1, goto_trace.steps.end());
207 if(f_it->second.is_inlined())
continue;
210 if(i_it->is_assert())
213 id2string(i_it->source_location.get_comment()),
214 i_it->source_location);
235 assert(it->source.pc->is_assert());
241 goal_map[
id(it->source.pc)].add_instance(it, l_c);
267 status() <<
"Runtime decision procedure: " 268 << (sat_stop-sat_start) <<
"s" <<
eom;
272 unsigned goals_covered=0;
275 if(g.second.satisfied)
282 status() <<
"\n** coverage results:" <<
eom;
286 const goalt &goal=g.second;
288 status() <<
"[" << g.first <<
"]";
307 for(
const auto &goal_pair :
goal_map)
309 const goalt &goal=goal_pair.second;
311 xmlt xml_result(
"goal");
319 std::cout << xml_result <<
"\n";
322 for(
const auto &test :
tests)
324 xmlt xml_result(
"test");
333 for(
const auto &step : test.goto_trace.steps)
339 if(step.io_args.size()==1)
346 for(
const auto &goal_id : test.covered_goals)
352 std::cout << xml_result <<
"\n";
361 for(
const auto &goal_pair :
goal_map)
363 const goalt &goal=goal_pair.second;
374 json_result[
"goalsCovered"]=
json_numbert(std::to_string(goals_covered));
377 for(
const auto &test :
tests)
389 for(
const auto &step : test.goto_trace.steps)
395 if(step.io_args.size()==1)
396 json_input[
"value"]=
json(step.io_args.front(),
bmc.
ns);
402 for(
const auto &goal_id : test.covered_goals)
407 std::cout <<
",\n" << json_result;
412 status() <<
"** " << goals_covered
413 <<
" of " <<
goal_map.size() <<
" covered (" 414 << std::fixed << std::setw(1) << std::setprecision(1)
425 std::cout <<
"Test suite:" <<
'\n';
427 for(
const auto &test :
tests)
428 std::cout <<
get_test(test.goto_trace) <<
'\n';
source_locationt source_location
const std::string & id2string(const irep_idt &d)
const goto_functionst & goto_functions
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
static mstreamt & eom(mstreamt &m)
std::map< irep_idt, goalt > goal_mapt
xmlt xml(const source_locationt &location)
json_arrayt & make_array()
irep_idt id(goto_programt::const_targett loc)
jsont & push_back(const jsont &json)
exprt conjunction(const exprt::operandst &op)
instructionst::const_iterator const_targett
symex_target_equationt::SSA_stepst::iterator step
std::vector< instancet > instancest
bool get_bool_option(const std::string &option) const
void set_attribute(const std::string &attribute, unsigned value)
goalt(const std::string &_description, const source_locationt &_source_location)
std::list< std::string > value_listt
virtual literalt convert(const exprt &expr)=0
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
exprt disjunction(const exprt::operandst &op)
xmlt & new_element(const std::string &name)
void add(const literalt condition)
unsigned iterations() const
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
Bounded Model Checking for ANSI-C + HDL.
absolute_timet current_time()
Base class for all expressions.
std::vector< testt > testst
std::string get_test(const goto_tracet &goto_trace) const
Cover a set of goals incrementally.
Try to cover some given set of goals incrementally.
std::vector< irep_idt > covered_goals
symex_target_equationt equation
void add_instance(symex_target_equationt::SSA_stepst::iterator step, literalt condition)
json_objectt & make_object()
void register_observer(observert &o)
virtual void satisfying_assignment()
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
json_objectt json(const source_locationt &location)
goalst::size_type size() const
bmc_covert(const goto_functionst &_goto_functions, bmct &_bmc)
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)
virtual std::string decision_procedure_text() const =0