34 if(g.second.status==goalt::statust::FAILURE)
38 for(
auto &c : g.second.instances)
44 g.second.status=goalt::statust::FAILURE;
45 symex_target_equationt::SSA_stepst::iterator next=c;
71 goal_map[i_it->source_location.get_property_id()]=
goalt(*i_it);
75 for(symex_target_equationt::SSA_stepst::iterator
84 if(it->source.pc->is_assert())
85 property_id=it->source.pc->source_location.get_property_id();
86 else if(it->source.pc->is_goto())
90 it->source.pc->source_location.get_function())+
".unwind."+
91 std::to_string(it->source.pc->loop_number);
92 goal_map[property_id].description=it->comment;
97 goal_map[property_id].instances.push_back(it);
125 for(
auto &g : goal_map)
126 if(g.second.status==goalt::statust::UNKNOWN)
127 g.second.status=goalt::statust::ERROR;
131 for(
auto &g : goal_map)
132 if(g.second.status==goalt::statust::UNKNOWN)
133 g.second.status=goalt::statust::SUCCESS;
140 status() <<
"Runtime decision procedure: " 141 << (sat_stop-sat_start) <<
"s" <<
eom;
168 for(
const auto &goal_pair :
goal_map)
169 status() <<
"[" << goal_pair.first <<
"] " 170 << goal_pair.second.description <<
": " 171 << goal_pair.second.status_string()
176 for(
const auto &g : goal_map)
177 if(g.second.status==goalt::statust::FAILURE)
179 std::cout <<
"\n" <<
"Trace for " << g.first <<
":" <<
"\n";
185 <<
" of " << cover_goals.
size() <<
" failed (" 196 xmlt xml_result(
"result");
198 xml_result.
set_attribute(
"status", g.second.status_string());
200 if(g.second.status==goalt::statust::FAILURE)
203 std::cout << xml_result <<
"\n";
218 result[
"status"]=
json_stringt(g.second.status_string());
220 if(g.second.status==goalt::statust::FAILURE)
222 jsont &json_trace=result[
"trace"];
227 std::cout <<
",\n" << json_result;
239 return bmc_all_properties();
const goto_functionst & goto_functions
const std::string & id2string(const irep_idt &d)
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
safety_checkert::resultt operator()()
virtual void do_before_solving()
virtual void report_failure()
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
static mstreamt & eom(mstreamt &m)
virtual void goal_covered(const cover_goalst::goalt &)
json_arrayt & make_array()
jsont & push_back(const jsont &json)
bool get_bool_option(const std::string &option) const
void set_attribute(const std::string &attribute, unsigned value)
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
Symbolic Execution of ANSI-C.
std::size_t number_covered() const
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()
absolute_timet current_time()
virtual void report(const cover_goalst &cover_goals)
Try to cover some given set of goals incrementally.
symex_target_equationt equation
json_objectt & make_object()
void register_observer(observert &o)
virtual void report_success()
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
goalst::size_type size() const
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