cprover
Loading...
Searching...
No Matches
show_vcc.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Output of the verification conditions (VCCs)
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "show_vcc.h"
14
15#include <fstream>
16#include <iostream>
17
19#include <util/format_expr.h>
20#include <util/json_irep.h>
21#include <util/ui_message.h>
22
26static void
28{
29 bool has_threads = equation.has_threads();
30 bool first = true;
31
32 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
33 equation.SSA_steps.begin();
34 s_it != equation.SSA_steps.end();
35 s_it++)
36 {
37 if(!s_it->is_assert())
38 continue;
39
40 if(first)
41 first = false;
42 else
43 out << '\n';
44
45 if(s_it->source.pc->source_location().is_not_nil())
46 out << s_it->source.pc->source_location() << '\n';
47
48 if(!s_it->comment.empty())
49 out << s_it->comment << '\n';
50
51 symex_target_equationt::SSA_stepst::const_iterator p_it =
52 equation.SSA_steps.begin();
53
54 // we show everything in case there are threads
55 symex_target_equationt::SSA_stepst::const_iterator last_it =
56 has_threads ? equation.SSA_steps.end() : s_it;
57
58 for(std::size_t count = 1; p_it != last_it; p_it++)
59 if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
60 {
61 if(!p_it->ignore)
62 {
63 out << messaget::faint << "{-" << count << "} " << messaget::reset
64 << format(p_it->cond_expr) << '\n';
65
66#ifdef DEBUG
67 out << "GUARD: " << format(p_it->guard) << '\n';
68 out << '\n';
69#endif
70
71 count++;
72 }
73 }
74
75 // Unicode equivalent of "|--------------------------"
76 out << messaget::faint << u8"\u251c";
77 for(unsigned i = 0; i < 26; i++)
78 out << u8"\u2500";
79 out << messaget::reset << '\n';
80
81 // split property into multiple disjunts, if applicable
83
84 if(s_it->cond_expr.id() == ID_or)
85 disjuncts = to_or_expr(s_it->cond_expr).operands();
86 else
87 disjuncts.push_back(s_it->cond_expr);
88
89 std::size_t count = 1;
90 for(const auto &disjunct : disjuncts)
91 {
92 out << messaget::faint << '{' << count << "} " << messaget::reset
93 << format(disjunct) << '\n';
94 count++;
95 }
96
97 out << messaget::eom;
98 }
99}
100
109static void
110show_vcc_json(std::ostream &out, const symex_target_equationt &equation)
111{
113
114 json_arrayt &json_vccs = json_result["vccs"].make_array();
115
116 bool has_threads = equation.has_threads();
117
118 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
119 equation.SSA_steps.begin();
120 s_it != equation.SSA_steps.end();
121 s_it++)
122 {
123 if(!s_it->is_assert())
124 continue;
125
126 // vcc object
127 json_objectt &object = json_vccs.push_back(jsont()).make_object();
128
129 const source_locationt &source_location =
130 s_it->source.pc->source_location();
131 if(source_location.is_not_nil())
132 object["sourceLocation"] = json(source_location);
133
134 const std::string &s = s_it->comment;
135 if(!s.empty())
136 object["comment"] = json_stringt(s);
137
138 // we show everything in case there are threads
139 symex_target_equationt::SSA_stepst::const_iterator last_it =
140 has_threads ? equation.SSA_steps.end() : s_it;
141
142 json_arrayt &json_constraints = object["constraints"].make_array();
143
144 for(symex_target_equationt::SSA_stepst::const_iterator p_it =
145 equation.SSA_steps.begin();
146 p_it != last_it;
147 p_it++)
148 {
149 if(
150 (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) &&
151 !p_it->ignore)
152 {
153 std::ostringstream string_value;
154 string_value << format(p_it->cond_expr);
156 }
157 }
158
159 std::ostringstream string_value;
160 string_value << format(s_it->cond_expr);
161 object["expression"] = json_stringt(string_value.str());
162 }
163
164 out << ",\n" << json_result;
165}
166
168 const optionst &options,
169 ui_message_handlert &ui_message_handler,
170 const symex_target_equationt &equation)
171{
172 messaget msg(ui_message_handler);
173
174 const std::string &filename = options.get_option("outfile");
175 bool have_file = !filename.empty() && filename != "-";
176
177 std::ofstream of;
178
179 if(have_file)
180 {
181 of.open(filename);
182 if(!of)
184 "failed to open output file: " + filename, "--outfile");
185 }
186
187 std::ostream &out = have_file ? of : std::cout;
188
189 switch(ui_message_handler.get_ui())
190 {
192 msg.error() << "XML UI not supported" << messaget::eom;
193 return;
194
196 show_vcc_json(out, equation);
197 break;
198
200 if(have_file)
201 {
202 msg.status() << "Verification conditions written to file"
203 << messaget::eom;
206 show_vcc_plain(mout.status(), equation);
207 }
208 else
209 {
210 msg.status() << "VERIFICATION CONDITIONS:\n" << messaget::eom;
211 show_vcc_plain(msg.status(), equation);
212 }
213 break;
214 }
215
216 if(have_file)
217 of.close();
218}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
std::vector< exprt > operandst
Definition expr.h:56
operandst & operands()
Definition expr.h:92
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool is_not_nil() const
Definition irep.h:380
Definition json.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & error() const
Definition message.h:399
static const commandt reset
return to default formatting, as defined by the terminal
Definition message.h:343
static const commandt faint
render text with faint font
Definition message.h:385
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
const std::string get_option(const std::string &option) const
Definition options.cpp:67
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual uit get_ui() const
Definition ui_message.h:33
static format_containert< T > format(const T &o)
Definition format.h:37
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
static void show_vcc_plain(messaget::mstreamt &out, const symex_target_equationt &equation)
Output equations from equation in plain text format to the given output stream out.
Definition show_vcc.cpp:27
static void show_vcc_json(std::ostream &out, const symex_target_equationt &equation)
Output equations from equation in the JSON format to the given output stream out.
Definition show_vcc.cpp:110
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Output equations from equation to a file or to the standard output.
Definition show_vcc.cpp:167
Output of the verification conditions (VCCs)
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2129
Generate Equation using Symbolic Execution.