Go to the documentation of this file.
27 const std::size_t goals_covered =
29 log.
status() <<
"** " << goals_covered <<
" of " << properties.size()
30 <<
" covered (" << std::fixed << std::setw(1)
31 << std::setprecision(1)
32 << (properties.empty()
34 : 100.0 * goals_covered / properties.size())
36 log.
statistics() <<
"** Used " << iterations <<
" iteration"
44 for(
const auto &property_pair : properties)
46 log.
result() <<
"[" << property_pair.first <<
"]";
48 if(property_pair.second.pc->source_location.is_not_nil())
51 if(!property_pair.second.description.empty())
52 log.
result() <<
' ' << property_pair.second.description;
66 for(
const auto &property_pair : properties)
71 {
"description", property_pair.second.description},
77 if(property_pair.second.pc->source_location.is_not_nil())
78 xml_result.
new_element() =
xml(property_pair.second.pc->source_location);
80 log.
result() << xml_result;
89 if(log.
status().tellp() > 0)
94 for(
const auto &property_pair : properties)
104 if(property_info.
pc->source_location.is_not_nil())
105 json_goal[
"sourceLocation"] =
json(property_info.
pc->source_location);
107 goals_array.
push_back(std::move(json_goal));
109 const std::size_t goals_covered =
123 switch(ui_message_handler.
get_ui())
Class that provides messages with a built-in verbosity 'level'.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
@ FAIL
The property was violated.
mstreamt & status() const
static void output_goals_json(const propertiest &properties, messaget &log, ui_message_handlert &ui_message_handler)
static void output_goals_iterations(const propertiest &properties, unsigned iterations, messaget &log)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static void output_goals_xml(const propertiest &properties, messaget &log)
std::string description
A description (usually derived from the assertion's comment)
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...
virtual uit get_ui() const
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
virtual json_stream_arrayt & get_json_stream()
property_statust status
The status of the property.
Cover Goals Reporting Utilities.
mstreamt & result() const
const std::string & id2string(const irep_idt &d)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
source_locationt source_location
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Provides methods for streaming JSON arrays.
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Provides methods for streaming JSON objects.
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
static void output_goals_plain(const propertiest &properties, messaget &log)
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
xmlt & new_element(const std::string &key)
mstreamt & statistics() const