cprover
show_vcc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "bmc.h"
13 
14 #include <iostream>
15 #include <fstream>
16 
17 #include <langapi/mode.h>
18 #include <langapi/language_util.h>
19 
20 #include <util/json.h>
21 #include <util/json_expr.h>
22 
23 void bmct::show_vcc_plain(std::ostream &out)
24 {
25  out << "\n" << "VERIFICATION CONDITIONS:" << "\n" << "\n";
26 
27  bool has_threads=equation.has_threads();
28 
29  for(symex_target_equationt::SSA_stepst::iterator
30  s_it=equation.SSA_steps.begin();
31  s_it!=equation.SSA_steps.end();
32  s_it++)
33  {
34  if(!s_it->is_assert())
35  continue;
36 
37  if(s_it->source.pc->source_location.is_not_nil())
38  out << s_it->source.pc->source_location << "\n";
39 
40  if(s_it->comment!="")
41  out << s_it->comment << "\n";
42 
43  symex_target_equationt::SSA_stepst::const_iterator
44  p_it=equation.SSA_steps.begin();
45 
46  // we show everything in case there are threads
47  symex_target_equationt::SSA_stepst::const_iterator
48  last_it=has_threads?equation.SSA_steps.end():s_it;
49 
50  for(std::size_t count=1; p_it!=last_it; p_it++)
51  if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
52  {
53  if(!p_it->ignore)
54  {
55  std::string string_value=
56  from_expr(ns, p_it->source.pc->function, p_it->cond_expr);
57  out << "{-" << count << "} " << string_value << "\n";
58 
59  #if 0
60  languages.from_expr(p_it->guard_expr, string_value);
61  out << "GUARD: " << string_value << "\n";
62  out << "\n";
63  #endif
64 
65  count++;
66  }
67  }
68 
69  out << "|--------------------------" << "\n";
70 
71  std::string string_value=
72  from_expr(ns, s_it->source.pc->function, s_it->cond_expr);
73  out << "{" << 1 << "} " << string_value << "\n";
74 
75  out << "\n";
76  }
77 }
78 
79 void bmct::show_vcc_json(std::ostream &out)
80 {
81  json_objectt json_result;
82 
83  json_arrayt &json_vccs=json_result["vccs"].make_array();
84 
85  bool has_threads=equation.has_threads();
86 
87  for(symex_target_equationt::SSA_stepst::iterator
88  s_it=equation.SSA_steps.begin();
89  s_it!=equation.SSA_steps.end();
90  s_it++)
91  {
92  if(!s_it->is_assert())
93  continue;
94 
95  // vcc object
96  json_objectt &object=json_vccs.push_back(jsont()).make_object();
97 
98  const source_locationt &source_location=s_it->source.pc->source_location;
99  if(source_location.is_not_nil())
100  object["sourceLocation"]=json(source_location);
101 
102  const std::string &s=s_it->comment;
103  if(!s.empty())
104  object["comment"]=json_stringt(s);
105 
106  // we show everything in case there are threads
107  symex_target_equationt::SSA_stepst::const_iterator
108  last_it=has_threads?equation.SSA_steps.end():s_it;
109 
110  json_arrayt &json_constraints=object["constraints"].make_array();
111 
112  for(symex_target_equationt::SSA_stepst::const_iterator p_it
113  =equation.SSA_steps.begin();
114  p_it!=last_it; p_it++)
115  {
116  if((p_it->is_assume() ||
117  p_it->is_assignment() ||
118  p_it->is_constraint()) &&
119  !p_it->ignore)
120  {
121  std::string string_value=
122  from_expr(ns, p_it->source.pc->function, p_it->cond_expr);
123  json_constraints.push_back(json_stringt(string_value));
124  }
125  }
126 
127  std::string string_value=
128  from_expr(ns, s_it->source.pc->function, s_it->cond_expr);
129  object["expression"]=json_stringt(string_value);
130  }
131 
132  out << ",\n" << json_result;
133 }
134 
136 {
137  const std::string &filename=options.get_option("outfile");
138  bool have_file=!filename.empty() && filename!="-";
139 
140  std::ofstream of;
141 
142  if(have_file)
143  {
144  of.open(filename);
145  if(!of)
146  throw "failed to open file "+filename;
147  }
148 
149  std::ostream &out=have_file?of:std::cout;
150 
151  switch(ui)
152  {
154  error() << "XML UI not supported" << eom;
155  return;
156 
158  show_vcc_json(out);
159  break;
160 
162  show_vcc_plain(out);
163  break;
164  }
165 
166  if(have_file)
167  of.close();
168 }
bool is_not_nil() const
Definition: irep.h:173
virtual void show_vcc_plain(std::ostream &out)
Definition: show_vcc.cpp:23
Definition: json.h:23
virtual void show_vcc()
Definition: show_vcc.cpp:135
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
json_arrayt & make_array()
Definition: json.h:284
namespacet ns
Definition: bmc.h:182
jsont & push_back(const jsont &json)
Definition: json.h:163
ui_message_handlert::uit ui
Definition: bmc.h:189
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
Expressions in JSON.
mstreamt & error() const
Definition: message.h:302
virtual void show_vcc_json(std::ostream &out)
Definition: show_vcc.cpp:79
const optionst & options
Definition: bmc.h:177
Bounded Model Checking for ANSI-C + HDL.
symex_target_equationt equation
Definition: bmc.h:183
json_objectt & make_object()
Definition: json.h:290
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83
languagest languages
Definition: mode.cpp:32