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)
148 symex_target_equationt::SSA_stepst::const_iterator step,
151 return step->is_assume() && prop_conv.
l_get(step->cond_literal).
is_false();
161 goalt &g=goal_pair.second;
193 auto solver_start=std::chrono::steady_clock::now();
201 if(i_it->is_assert())
204 id2string(i_it->source_location.get_comment()),
205 i_it->source_location);
224 assert(it->source.pc->is_assert());
228 goal_map[
id(it->source.pc)].add_instance(it, l_c);
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)
346 for(
const auto &goal_pair :
goal_map)
348 const goalt &goal=goal_pair.second;
350 json_result[
"status"] =
361 json_arrayt &tests_array=json_result[
"tests"].make_array();
362 for(
const auto &test :
tests)
367 json_arrayt &json_trace = json_result[
"trace"].make_array();
372 json_arrayt &json_test = json_result[
"inputs"].make_array();
374 for(
const auto &step : test.goto_trace.steps)
380 if(step.io_args.size()==1)
382 json(step.io_args.front(),
bmc.
ns, ID_unknown);
388 for(
const auto &goal_id : test.covered_goals)
398 status() <<
"** " << goals_covered
399 <<
" of " <<
goal_map.size() <<
" covered (" 400 << std::fixed << std::setw(1) << std::setprecision(1)
411 result() <<
"Test suite:" <<
'\n';
413 for(
const auto &test :
tests)
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)
source_locationt source_location
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
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.
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)
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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.
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)
static bool is_failed_assumption_step(symex_target_equationt::SSA_stepst::const_iterator step, const prop_convt &prop_conv)
virtual std::string decision_procedure_text() const =0