28 for(
const auto &step : goto_trace.
steps)
39 if(step.io_args.size()==1)
40 test+=
from_expr(ns,
"", step.io_args.front());
50 unsigned goals_covered=0;
52 for(
const auto &prop_pair : property_map)
53 if(prop_pair.second.is_failure())
60 status() <<
"\n** coverage results:" <<
eom;
62 for(
const auto &prop_pair : property_map)
64 const auto &
property=prop_pair.second;
66 status() <<
"[" << prop_pair.first <<
"]";
68 if(property.source_location.is_not_nil())
71 if(!property.description.empty())
72 status() <<
' ' <<
property.description;
74 status() <<
": " << (
property.is_failure()?
"SATISFIED":
"FAILED")
85 for(
const auto &prop_pair : property_map)
87 const auto &
property=prop_pair.second;
89 xmlt xml_result(
"result");
92 "description",
id2string(property.description));
94 "status", property.is_failure()?
"SATISFIED":
"FAILED");
96 if(property.source_location.is_not_nil())
99 if(property.is_failure())
111 for(
const auto &step : property.error_trace.steps)
117 if(step.io_args.size()==1)
119 xml(step.io_args.front(), ns);
125 std::cout << xml_result <<
"\n";
134 for(
const auto &prop_pair : property_map)
136 const auto &
property=prop_pair.second;
140 json_stringt(property.is_failure()?
"satisfied":
"failed");
144 if(property.source_location.is_not_nil())
145 result[
"sourceLocation"]=
json(property.source_location);
147 if(property.is_failure())
154 convert(ns, property.error_trace, json_trace);
160 for(
const auto &step : property.error_trace.steps)
166 if(step.io_args.size()==1)
167 json_input[
"value"]=
json(step.io_args.front(), ns);
174 json_result[
"totalGoals"]=
176 json_result[
"goalsCovered"]=
json_numbert(std::to_string(goals_covered));
177 std::cout <<
",\n" << json_result;
182 status() <<
"** " << goals_covered
183 <<
" of " << property_map.size() <<
" covered (" 184 << std::fixed << std::setw(1) << std::setprecision(1)
185 << (property_map.empty()?
186 100.0:100.0*goals_covered/property_map.size())
192 std::set<std::string> tests;
194 for(
const auto &prop_pair : property_map)
195 if(prop_pair.second.is_failure())
196 tests.insert(
get_test(prop_pair.second.error_trace));
198 std::cout <<
"Test suite:" <<
'\n';
200 for(
const auto &t : tests)
201 std::cout << t <<
'\n';
void report_cover(const path_searcht::property_mapt &)
const std::string & id2string(const irep_idt &d)
std::map< irep_idt, property_entryt > property_mapt
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
symbol_tablet symbol_table
static mstreamt & eom(mstreamt &m)
xmlt xml(const source_locationt &location)
json_arrayt & make_array()
jsont & push_back(const jsont &json)
virtual bool isset(char option) const
source_locationt source_location
void set_attribute(const std::string &attribute, unsigned value)
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
xmlt & new_element(const std::string &name)
json_objectt & make_object()
std::string get_test(const goto_tracet &goto_trace)
json_objectt json(const source_locationt &location)