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