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 
25 static void show_step(
26  const namespacet &ns,
27  const SSA_stept &step,
28  const std::string &annotation,
29  std::size_t &count)
30 {
31  const irep_idt &function_id = step.source.function_id;
32 
33  std::string string_value = (step.is_shared_read() || step.is_shared_write())
34  ? from_expr(ns, function_id, step.ssa_lhs)
35  : from_expr(ns, function_id, step.cond_expr);
36  std::cout << '(' << count << ") ";
37  if(annotation.empty())
38  std::cout << string_value;
39  else
40  std::cout << annotation << '(' << string_value << ')';
41  std::cout << '\n';
42 
43  if(!step.guard.is_true())
44  {
45  const std::string guard_string = from_expr(ns, function_id, step.guard);
46  std::cout << std::string(std::to_string(count).size() + 3, ' ');
47  std::cout << "guard: " << guard_string << '\n';
48  }
49 
50  ++count;
51 }
52 
53 void show_program(const namespacet &ns, const symex_target_equationt &equation)
54 {
55  std::size_t count = 1;
56 
57  std::cout << '\n' << "Program constraints:" << '\n';
58 
59  for(const auto &step : equation.SSA_steps)
60  {
61  std::cout << "// " << step.source.pc->location_number << " ";
62  std::cout << step.source.pc->source_location.as_string() << "\n";
63 
64  if(step.is_assignment())
65  show_step(ns, step, "", count);
66  else if(step.is_assert())
67  show_step(ns, step, "ASSERT", count);
68  else if(step.is_assume())
69  show_step(ns, step, "ASSUME", count);
70  else if(step.is_constraint())
71  {
72  PRECONDITION(step.guard.is_true());
73  show_step(ns, step, "CONSTRAINT", count);
74  }
75  else if(step.is_shared_read())
76  show_step(ns, step, "SHARED_READ", count);
77  else if(step.is_shared_write())
78  show_step(ns, step, "SHARED_WRITE", count);
79  }
80 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
show_program
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Print the steps of equation on the standard output.
Definition: show_program.cpp:53
symex_target_equation.h
show_step
static void show_step(const namespacet &ns, const SSA_stept &step, const std::string &annotation, std::size_t &count)
Output a single SSA step.
Definition: show_program.cpp:25
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
SSA_stept::guard
exprt guard
Definition: ssa_step.h:137
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
SSA_stept::source
symex_targett::sourcet source
Definition: ssa_step.h:47
SSA_stept::is_shared_write
bool is_shared_write() const
Definition: ssa_step.h:105
SSA_stept::is_shared_read
bool is_shared_read() const
Definition: ssa_step.h:100
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
language_util.h
SSA_stept::cond_expr
exprt cond_expr
Definition: ssa_step.h:147
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:39
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:255
show_program.h
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20