CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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"
13
15#include <util/format_expr.h>
16#include <util/json_irep.h>
17#include <util/ui_message.h>
18
20
21#include <fstream> // IWYU pragma: keep
22#include <iostream>
23
27static void
29{
30 bool has_threads = equation.has_threads();
31 bool first = true;
32
33 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
34 equation.SSA_steps.begin();
35 s_it != equation.SSA_steps.end();
36 s_it++)
37 {
38 if(!s_it->is_assert())
39 continue;
40
41 if(first)
42 first = false;
43 else
44 out << '\n';
45
46 if(s_it->source.pc->source_location().is_not_nil())
47 out << s_it->source.pc->source_location() << '\n';
48
49 if(!s_it->comment.empty())
50 out << s_it->comment << '\n';
51
52 symex_target_equationt::SSA_stepst::const_iterator p_it =
53 equation.SSA_steps.begin();
54
55 // we show everything in case there are threads
56 symex_target_equationt::SSA_stepst::const_iterator last_it =
57 has_threads ? equation.SSA_steps.end() : s_it;
58
59 for(std::size_t count = 1; p_it != last_it; p_it++)
60 if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
61 {
62 if(!p_it->ignore)
63 {
64 out << messaget::faint << "{-" << count << "} " << messaget::reset
65 << format(p_it->cond_expr) << '\n';
66
67#ifdef DEBUG
68 out << "GUARD: " << format(p_it->guard) << '\n';
69 out << '\n';
70#endif
71
72 count++;
73 }
74 }
75
76 // Unicode equivalent of "|--------------------------"
77 out << messaget::faint << u8"\u251c";
78 for(unsigned i = 0; i < 26; i++)
79 out << u8"\u2500";
80 out << messaget::reset << '\n';
81
82 // split property into multiple disjunts, if applicable
84
85 if(s_it->cond_expr.id() == ID_or)
86 disjuncts = to_or_expr(s_it->cond_expr).operands();
87 else
88 disjuncts.push_back(s_it->cond_expr);
89
90 std::size_t count = 1;
91 for(const auto &disjunct : disjuncts)
92 {
93 out << messaget::faint << '{' << count << "} " << messaget::reset
94 << format(disjunct) << '\n';
95 count++;
96 }
97
98 out << messaget::eom;
99 }
100}
101
110static void
111show_vcc_json(std::ostream &out, const symex_target_equationt &equation)
112{
114
115 json_arrayt &json_vccs = json_result["vccs"].make_array();
116
117 bool has_threads = equation.has_threads();
118
119 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
120 equation.SSA_steps.begin();
121 s_it != equation.SSA_steps.end();
122 s_it++)
123 {
124 if(!s_it->is_assert())
125 continue;
126
127 // vcc object
128 json_objectt &object = json_vccs.push_back(jsont()).make_object();
129
130 const source_locationt &source_location =
131 s_it->source.pc->source_location();
132 if(source_location.is_not_nil())
133 object["sourceLocation"] = json(source_location);
134
135 const std::string &s = s_it->comment;
136 if(!s.empty())
137 object["comment"] = json_stringt(s);
138
139 // we show everything in case there are threads
140 symex_target_equationt::SSA_stepst::const_iterator last_it =
141 has_threads ? equation.SSA_steps.end() : s_it;
142
143 json_arrayt &json_constraints = object["constraints"].make_array();
144
145 for(symex_target_equationt::SSA_stepst::const_iterator p_it =
146 equation.SSA_steps.begin();
147 p_it != last_it;
148 p_it++)
149 {
150 if(
151 (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) &&
152 !p_it->ignore)
153 {
154 std::ostringstream string_value;
155 string_value << format(p_it->cond_expr);
157 }
158 }
159
160 std::ostringstream string_value;
161 string_value << format(s_it->cond_expr);
162 object["expression"] = json_stringt(string_value.str());
163 }
164
165 out << ",\n" << json_result;
166}
167
169 const optionst &options,
170 ui_message_handlert &ui_message_handler,
171 const symex_target_equationt &equation)
172{
173 messaget msg(ui_message_handler);
174
175 const std::string &filename = options.get_option("outfile");
176 bool have_file = !filename.empty() && filename != "-";
177
178 std::ofstream of;
179
180 if(have_file)
181 {
182 of.open(filename);
183 if(!of)
185 "failed to open output file: " + filename, "--outfile");
186 }
187
188 std::ostream &out = have_file ? of : std::cout;
189
190 switch(ui_message_handler.get_ui())
191 {
193 msg.error() << "XML UI not supported" << messaget::eom;
194 return;
195
197 show_vcc_json(out, equation);
198 break;
199
201 if(have_file)
202 {
203 msg.status() << "Verification conditions written to file"
204 << messaget::eom;
207 show_vcc_plain(mout.status(), equation);
208 }
209 else
210 {
211 msg.status() << "VERIFICATION CONDITIONS:\n" << messaget::eom;
212 show_vcc_plain(msg.status(), equation);
213 }
214 break;
215 }
216
217 if(have_file)
218 of.close();
219}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::vector< exprt > operandst
Definition expr.h:58
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool is_not_nil() const
Definition irep.h:372
Definition json.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static const commandt reset
return to default formatting, as defined by the terminal
Definition message.h:335
static const commandt faint
render text with faint font
Definition message.h:377
static eomt eom
Definition message.h:289
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:28
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:111
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:168
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:2317
Generate Equation using Symbolic Execution.