32 if(g.second.status==goalt::statust::FAILURE)
36 for(
auto &c : g.second.instances)
42 g.second.status=goalt::statust::FAILURE;
56 auto solver_start=std::chrono::steady_clock::now();
65 goal_map[i_it->source_location.get_property_id()]=
goalt(*i_it);
69 for(symex_target_equationt::SSA_stepst::iterator
78 if(it->source.pc->is_assert())
79 property_id=it->source.pc->source_location.get_property_id();
80 else if(it->source.pc->is_goto())
84 it->source.pc->source_location.get_function())+
".unwind."+
86 goal_map[property_id].description=it->comment;
91 goal_map[property_id].instances.push_back(it);
120 if(g.second.status==goalt::statust::UNKNOWN)
121 g.second.status=goalt::statust::ERROR;
126 if(g.second.status==goalt::statust::UNKNOWN)
127 g.second.status=goalt::statust::SUCCESS;
131 auto solver_stop = std::chrono::steady_clock::now();
133 status() <<
"Runtime decision procedure: " 134 << std::chrono::duration<double>(solver_stop-solver_start).count()
163 std::vector<goal_mapt::const_iterator> goals;
166 goals.push_back(g_it);
175 [](goal_mapt::const_iterator git1, goal_mapt::const_iterator git2) {
176 const auto &g1 = git1->second.source_location;
177 const auto &g2 = git2->second.source_location;
178 if(g1.get_file() != g2.get_file())
180 else if(!g1.get_line().empty() && !g2.get_line().empty())
181 return std::stoul(
id2string(g1.get_line())) <
191 for(
const auto &g : goals)
193 const auto &l = g->second.source_location;
195 if(l.get_function() != previous_function)
197 if(!previous_function.empty())
199 previous_function = l.get_function();
200 if(!previous_function.empty())
202 current_file = l.get_file();
203 if(!current_file.
empty())
204 result() << current_file <<
' ';
205 if(!l.get_function().empty())
206 result() <<
"function " << l.get_function();
213 if(l.get_file() != current_file)
214 result() <<
"file " << l.get_file() <<
' ';
216 if(!l.get_line().empty())
217 result() <<
"line " << l.get_line() <<
' ';
219 result() << g->second.description <<
": ";
221 if(g->second.status == goalt::statust::SUCCESS)
232 if(g.second.status==goalt::statust::FAILURE)
234 result() <<
"\n" <<
"Trace for " << g.first <<
":" <<
"\n";
242 <<
" of " << cover_goals.
size() <<
" failed (" 253 xmlt xml_result(
"result");
255 xml_result.
set_attribute(
"status", g.second.status_string());
257 if(g.second.status==goalt::statust::FAILURE)
281 if(g.second.status==goalt::statust::FAILURE)
284 result.push_back_stream_array(
"trace");
285 convert<json_stream_arrayt>(
300 return bmc_all_properties();
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)
const goto_functionst & goto_functions
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
ui_message_handlert & ui_message_handler
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()
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Provides methods for streaming JSON objects.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
virtual void report_failure()
static const commandt reset
return to default formatting, as defined by the terminal
virtual void goal_covered(const cover_goalst::goalt &)
json_stream_arrayt & get_json_stream()
Some safety properties were violated.
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.
static const commandt red
render text with red foreground color
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)
A collection of goto functions.
virtual void set_message_handler(message_handlert &_message_handler)
Symbolic Execution of ANSI-C.
std::size_t number_covered() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
No safety properties were violated.
void add(const literalt condition)
unsigned iterations() const
static const commandt faint
render text with faint font
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
mstreamt & result() const
xmlt & new_element(const std::string &key)
mstreamt & status() const
virtual void report(const cover_goalst &cover_goals)
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()
static const commandt green
render text with green foreground color
trace_optionst trace_options()
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
goalst::size_type size() const
virtual std::string decision_procedure_text() const =0