28 const std::size_t goals_covered =
30 log.
status() <<
"** " << goals_covered <<
" of " << properties.size()
31 <<
" covered (" << std::fixed << std::setw(1)
32 << std::setprecision(1)
33 << (properties.empty()
35 : 100.0 * goals_covered / properties.size())
37 log.
statistics() <<
"** Used " << iterations <<
" iteration"
45 for(
const auto &property_pair : properties)
47 log.
result() <<
"[" << property_pair.first <<
"]";
49 if(property_pair.second.pc->source_location.is_not_nil())
52 if(!property_pair.second.description.empty())
53 log.
result() <<
' ' << property_pair.second.description;
67 for(
const auto &property_pair : properties)
72 {
"description", property_pair.second.description},
78 if(property_pair.second.pc->source_location.is_not_nil())
79 xml_result.
new_element() =
xml(property_pair.second.pc->source_location);
81 log.
result() << xml_result;
90 if(log.
status().tellp() > 0)
95 for(
const auto &property_pair : properties)
105 if(property_info.
pc->source_location.is_not_nil())
106 json_goal[
"sourceLocation"] =
json(property_info.
pc->source_location);
108 goals_array.
push_back(std::move(json_goal));
110 const std::size_t goals_covered =
124 switch(ui_message_handler.
get_ui())
Provides methods for streaming JSON arrays.
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Provides methods for streaming JSON objects.
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
mstreamt & statistics() const
mstreamt & status() const
mstreamt & result() const
virtual uit get_ui() const
virtual json_stream_arrayt & get_json_stream()
xmlt & new_element(const std::string &key)
static void output_goals_iterations(const propertiest &properties, unsigned iterations, messaget &log)
static void output_goals_xml(const propertiest &properties, messaget &log)
static void output_goals_json(const propertiest &properties, messaget &log, ui_message_handlert &ui_message_handler)
void output_goals(const propertiest &properties, unsigned iterations, ui_message_handlert &ui_message_handler)
Outputs the properties interpreted as 'coverage goals' and the number of goto verifier iterations tha...
static void output_goals_plain(const propertiest &properties, messaget &log)
Cover Goals Reporting Utilities.
const std::string & id2string(const irep_idt &d)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
@ FAIL
The property was violated.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
property_statust status
The status of the property.
std::string description
A description (usually derived from the assertion's comment)
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.