cprover
invariant_set_domain.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Invariant Set Domain
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "invariant_set_domain.h"
13 
14 #include <util/expr_util.h>
15 #include <util/simplify_expr.h>
16 
18  const irep_idt &,
19  locationt from_l,
20  const irep_idt &,
21  locationt to_l,
22  ai_baset &,
23  const namespacet &ns)
24 {
25  switch(from_l->type)
26  {
27  case GOTO:
28  {
29  // Comparing iterators is safe as the target must be within the same list
30  // of instructions because this is a GOTO.
31  exprt tmp(from_l->guard);
32 
33  goto_programt::const_targett next=from_l;
34  next++;
35  if(next==to_l)
36  tmp = boolean_negate(from_l->guard);
37 
38  simplify(tmp, ns);
40  }
41  break;
42 
43  case ASSERT:
44  case ASSUME:
45  {
46  exprt tmp(from_l->guard);
47  simplify(tmp, ns);
49  }
50  break;
51 
52  case RETURN:
53  // ignore
54  break;
55 
56  case ASSIGN:
57  {
58  const code_assignt &assignment=to_code_assign(from_l->code);
59  invariant_set.assignment(assignment.lhs(), assignment.rhs());
60  }
61  break;
62 
63  case OTHER:
64  if(from_l->code.is_not_nil())
65  invariant_set.apply_code(from_l->code);
66  break;
67 
68  case DECL:
69  invariant_set.apply_code(from_l->code);
70  break;
71 
72  case FUNCTION_CALL:
73  invariant_set.apply_code(from_l->code);
74  break;
75 
76  case START_THREAD:
78  break;
79 
80  default:
81  {
82  // do nothing
83  }
84  }
85 }
void strengthen(const exprt &expr)
Deprecated expression utility functions.
void assignment(const exprt &lhs, const exprt &rhs)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
exprt & lhs()
Definition: std_code.h:269
void make_threaded()
exprt & rhs()
Definition: std_code.h:274
void apply_code(const codet &code)
instructionst::const_iterator const_targett
Definition: goto_program.h:415
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
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:54
goto_programt::const_targett locationt
Definition: ai_domain.h:40
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
virtual void transform(const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
A codet representing an assignment in the program.
Definition: std_code.h:256
bool simplify(exprt &expr, const namespacet &ns)