56 symex_target_equationt::SSA_stepst::iterator
step;
64 symex_target_equationt::SSA_stepst::iterator step,
79 const std::string &_description,
94 std::vector<exprt> tmp;
111 return loc->source_location.get_property_id();
123 for(
const auto &step : goto_trace.
steps)
134 if(step.io_args.size()==1)
154 goalt &g=goal_pair.second;
182 for(goto_tracet::stepst::iterator
183 s_it1=goto_trace.steps.begin();
184 s_it1!=goto_trace.steps.end();
186 if(s_it1->is_assume() && !s_it1->cond_value)
188 goto_trace.
steps.erase(++s_it1, goto_trace.steps.end());
199 auto solver_start=std::chrono::steady_clock::now();
207 if(i_it->is_assert())
210 id2string(i_it->source_location.get_comment()),
211 i_it->source_location);
230 assert(it->source.pc->is_assert());
234 goal_map[
id(it->source.pc)].add_instance(it, l_c);
257 auto solver_stop=std::chrono::steady_clock::now();
258 status() <<
"Runtime decision procedure: " 259 << std::chrono::duration<double>(solver_stop-solver_start).count()
264 unsigned goals_covered=0;
267 if(g.second.satisfied)
274 result() <<
"\n** coverage results:" <<
eom;
278 const goalt &goal=g.second;
280 result() <<
"[" << g.first <<
"]";
298 for(
const auto &goal_pair :
goal_map)
300 const goalt &goal=goal_pair.second;
302 xmlt xml_result(
"goal");
313 for(
const auto &test :
tests)
315 xmlt xml_result(
"test");
324 for(
const auto &step : test.goto_trace.steps)
330 if(step.io_args.size()==1)
337 for(
const auto &goal_id : test.covered_goals)
352 for(
const auto &goal_pair :
goal_map)
354 const goalt &goal=goal_pair.second;
356 json_result[
"status"] =
367 json_arrayt &tests_array=json_result[
"tests"].make_array();
368 for(
const auto &test :
tests)
373 json_arrayt &json_trace = json_result[
"trace"].make_array();
378 json_arrayt &json_test = json_result[
"inputs"].make_array();
380 for(
const auto &step : test.goto_trace.steps)
386 if(step.io_args.size()==1)
388 json(step.io_args.front(),
bmc.
ns, ID_unknown);
394 for(
const auto &goal_id : test.covered_goals)
404 status() <<
"** " << goals_covered
405 <<
" of " <<
goal_map.size() <<
" covered (" 406 << std::fixed << std::setw(1) << std::setprecision(1)
417 result() <<
"Test suite:" <<
'\n';
419 for(
const auto &test :
tests)
source_locationt source_location
const std::string & id2string(const irep_idt &d)
Provides methods for streaming JSON objects.
const irep_idt & get_function() const
const goto_functionst & goto_functions
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
static mstreamt & eom(mstreamt &m)
std::map< irep_idt, goalt > goal_mapt
xmlt xml(const source_locationt &location)
irep_idt id(goto_programt::const_targett loc)
jsont & push_back(const jsont &json)
ui_message_handlert::uit ui
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)
instructionst::const_iterator const_targett
goalt(const std::string &_description, const source_locationt &_source_location)
std::list< std::string > value_listt
virtual literalt convert(const exprt &expr)=0
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)
exprt disjunction(const exprt::operandst &op)
xmlt & new_element(const std::string &name)
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)
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.
mstreamt & result() const
mstreamt & status() const
Base class for all expressions.
std::vector< testt > testst
std::string to_string(const string_constraintt &expr)
Used for debug printing.
std::string get_test(const goto_tracet &goto_trace) const
Cover a set of goals incrementally.
Bounded model checking or path exploration for goto-programs.
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()
trace_optionst trace_options()
#define forall_goto_functions(it, functions)
json_stream_arrayt & json_stream()
Returns a reference to the top-level JSON array stream.
#define forall_goto_program_instructions(it, program)
mstreamt & statistics() const
json_objectt json(const source_locationt &location)
goalst::size_type size() const
bmc_covert(const goto_functionst &_goto_functions, bmct &_bmc)
virtual std::string decision_procedure_text() const =0