cprover
show_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Output of the program (SSA) constraints
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "show_program.h"
13 
14 #include <iostream>
15 
17 
18 #include <langapi/language_util.h>
19 
20 void show_program(const namespacet &ns, const symex_target_equationt &equation)
21 {
22  unsigned count = 1;
23 
24  std::cout << "\n"
25  << "Program constraints:"
26  << "\n";
27 
28  for(const auto &step : equation.SSA_steps)
29  {
30  std::cout << "// " << step.source.pc->location_number << " ";
31  std::cout << step.source.pc->source_location.as_string() << "\n";
32  const irep_idt &function = step.source.function;
33 
34  if(step.is_assignment())
35  {
36  std::string string_value = from_expr(ns, function, step.cond_expr);
37  std::cout << "(" << count << ") " << string_value << "\n";
38 
39  if(!step.guard.is_true())
40  {
41  std::string string_value = from_expr(ns, function, step.guard);
42  std::cout << std::string(std::to_string(count).size() + 3, ' ');
43  std::cout << "guard: " << string_value << "\n";
44  }
45 
46  count++;
47  }
48  else if(step.is_assert())
49  {
50  std::string string_value = from_expr(ns, function, step.cond_expr);
51  std::cout << "(" << count << ") ASSERT(" << string_value << ") "
52  << "\n";
53 
54  if(!step.guard.is_true())
55  {
56  std::string string_value = from_expr(ns, function, step.guard);
57  std::cout << std::string(std::to_string(count).size() + 3, ' ');
58  std::cout << "guard: " << string_value << "\n";
59  }
60 
61  count++;
62  }
63  else if(step.is_assume())
64  {
65  std::string string_value = from_expr(ns, function, step.cond_expr);
66  std::cout << "(" << count << ") ASSUME(" << string_value << ") "
67  << "\n";
68 
69  if(!step.guard.is_true())
70  {
71  std::string string_value = from_expr(ns, function, step.guard);
72  std::cout << std::string(std::to_string(count).size() + 3, ' ');
73  std::cout << "guard: " << string_value << "\n";
74  }
75 
76  count++;
77  }
78  else if(step.is_constraint())
79  {
80  std::string string_value = from_expr(ns, function, step.cond_expr);
81  std::cout << "(" << count << ") CONSTRAINT(" << string_value << ") "
82  << "\n";
83 
84  count++;
85  }
86  else if(step.is_shared_read() || step.is_shared_write())
87  {
88  std::string string_value = from_expr(ns, function, step.ssa_lhs);
89  std::cout << "(" << count << ") SHARED_"
90  << (step.is_shared_write() ? "WRITE" : "READ") << "("
91  << string_value << ")\n";
92 
93  if(!step.guard.is_true())
94  {
95  std::string string_value = from_expr(ns, function, step.guard);
96  std::cout << std::string(std::to_string(count).size() + 3, ' ');
97  std::cout << "guard: " << string_value << "\n";
98  }
99 
100  count++;
101  }
102  }
103 }
Generate Equation using Symbolic Execution.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void show_program(const namespacet &ns, const symex_target_equationt &equation)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Output of the program (SSA) constraints.