CBMC
Loading...
Searching...
No Matches
report_properties.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Solver
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "report_properties.h"
13
14#include <util/console.h>
15
16void report_properties(const std::vector<propertyt> &properties)
17{
18 irep_idt current_file, current_function;
19
20 for(auto &property : properties)
21 {
22 const auto &l = property.source_location;
23
24 if(l.get_function() != current_function)
25 {
26 if(!current_function.empty())
27 consolet::out() << '\n';
28 current_function = l.get_function();
29 if(!current_function.empty())
30 {
31 current_file = l.get_file();
32 if(!current_file.empty())
33 consolet::out() << current_file << ' ';
34 if(!l.get_function().empty())
35 consolet::out() << "function " << l.get_function();
36 consolet::out() << '\n';
37 }
38 }
39
40 auto property_id = property.property_id();
42 if(property_id.empty())
43 consolet::out() << '?';
44 else
45 consolet::out() << property_id;
47
48 if(l.get_file() != current_file)
49 consolet::out() << ' ' << l.get_file();
50
51 if(!l.get_line().empty())
52 consolet::out() << " line " << l.get_line();
53
54 auto comment = l.get_comment();
55 if(!comment.empty())
56 consolet::out() << ' ' << comment;
57
58 consolet::out() << ": ";
59
60 switch(property.status)
61 {
62 case propertyt::PASS:
64 break;
65
67 consolet::out() << consolet::red << "REFUTED" << consolet::reset;
68 break;
69
70 case propertyt::ERROR:
73 break;
74
76 consolet::out() << consolet::red << consolet::bold << "DROPPED"
78 break;
79
80 case propertyt::UNKNOWN:
82 break;
83 }
84
85#if 0
87 << ' ' << consolet::faint << std::setw(1) << std::setprecision(1)
88 << std::chrono::duration<double>(property.stop - property.start).count()
89 << 's' << consolet::reset;
90#endif
91
92 consolet::out() << '\n';
93 }
94}
95
96solver_resultt overall_outcome(const std::vector<propertyt> &properties)
97{
98 auto result = solver_resultt::ALL_PASS;
99
100 for(auto &property : properties)
101 if(property.status == propertyt::ERROR)
102 result = solver_resultt::ERROR;
103 else if(property.status == propertyt::DROPPED)
104 result = solver_resultt::ERROR;
105 else if(property.status == propertyt::REFUTED)
107
108 return result;
109}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait()
Definition ai.h:565
static std::ostream & yellow(std::ostream &)
Definition console.cpp:136
static std::ostream & out()
Definition console.h:55
static std::ostream & reset(std::ostream &)
Definition console.cpp:176
static std::ostream & green(std::ostream &)
Definition console.cpp:120
static std::ostream & faint(std::ostream &)
Definition console.cpp:160
static std::ostream & bold(std::ostream &)
Definition console.cpp:152
static std::ostream & red(std::ostream &)
Definition console.cpp:128
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
Console.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
solver_resultt overall_outcome(const std::vector< propertyt > &properties)
void report_properties(const std::vector< propertyt > &properties)
Property Reporting.
solver_resultt
Definition solver.h:21