33 if(g.second.status==goalt::statust::FAILURE)
37 for(
auto &c : g.second.instances)
43 g.second.status=goalt::statust::FAILURE;
44 symex_target_equationt::SSA_stepst::iterator next=c;
60 auto solver_start=std::chrono::steady_clock::now();
69 goal_map[i_it->source_location.get_property_id()]=
goalt(*i_it);
73 for(symex_target_equationt::SSA_stepst::iterator
82 if(it->source.pc->is_assert())
83 property_id=it->source.pc->source_location.get_property_id();
84 else if(it->source.pc->is_goto())
88 it->source.pc->source_location.get_function())+
".unwind."+
90 goal_map[property_id].description=it->comment;
95 goal_map[property_id].instances.push_back(it);
124 if(g.second.status==goalt::statust::UNKNOWN)
125 g.second.status=goalt::statust::ERROR;
130 if(g.second.status==goalt::statust::UNKNOWN)
131 g.second.status=goalt::statust::SUCCESS;
135 auto solver_stop = std::chrono::steady_clock::now();
137 status() <<
"Runtime decision procedure: " 138 << std::chrono::duration<double>(solver_stop-solver_start).count()
166 for(
const auto &goal_pair :
goal_map)
167 result() <<
"[" << goal_pair.first <<
"] " 168 << goal_pair.second.description <<
": " 169 << goal_pair.second.status_string()
175 if(g.second.status==goalt::statust::FAILURE)
177 result() <<
"\n" <<
"Trace for " << g.first <<
":" <<
"\n";
184 <<
" of " << cover_goals.
size() <<
" failed (" 195 xmlt xml_result(
"result");
197 xml_result.
set_attribute(
"status", g.second.status_string());
199 if(g.second.status==goalt::statust::FAILURE)
221 if(g.second.status==goalt::statust::FAILURE)
224 result.push_back_stream_array(
"trace");
225 convert<json_stream_arrayt>(
240 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()
Provides methods for streaming JSON objects.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
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 &)
Some safety properties were violated.
ui_message_handlert::uit ui
int solver(std::istream &in)
Safety is unknown due to an error during safety checking.
bool get_bool_option(const std::string &option) const
void set_attribute(const std::string &attribute, unsigned value)
Provides methods for streaming JSON arrays.
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)
Symbolic Execution of ANSI-C.
std::size_t number_covered() const
No safety properties were violated.
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()
mstreamt & result() const
mstreamt & status() const
virtual void report(const cover_goalst &cover_goals)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
Try to cover some given set of goals incrementally.
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
symex_target_equationt equation
void register_observer(observert &o)
virtual void report_success()
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)
goalst::size_type size() const
virtual std::string decision_procedure_text() const =0