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/simplify_expr.h>
15 
17  locationt from_l,
18  locationt to_l,
19  ai_baset &ai,
20  const namespacet &ns)
21 {
22  switch(from_l->type)
23  {
24  case GOTO:
25  {
26  // Comparing iterators is safe as the target must be within the same list
27  // of instructions because this is a GOTO.
28  exprt tmp(from_l->guard);
29 
30  goto_programt::const_targett next=from_l;
31  next++;
32  if(next==to_l)
33  tmp.make_not();
34 
35  simplify(tmp, ns);
37  }
38  break;
39 
40  case ASSERT:
41  case ASSUME:
42  {
43  exprt tmp(from_l->guard);
44  simplify(tmp, ns);
46  }
47  break;
48 
49  case RETURN:
50  // ignore
51  break;
52 
53  case ASSIGN:
54  {
55  const code_assignt &assignment=to_code_assign(from_l->code);
56  invariant_set.assignment(assignment.lhs(), assignment.rhs());
57  }
58  break;
59 
60  case OTHER:
61  if(from_l->code.is_not_nil())
62  invariant_set.apply_code(from_l->code);
63  break;
64 
65  case DECL:
66  invariant_set.apply_code(from_l->code);
67  break;
68 
69  case FUNCTION_CALL:
70  invariant_set.apply_code(from_l->code);
71  break;
72 
73  case START_THREAD:
75  break;
76 
77  default:
78  {
79  // do nothing
80  }
81  }
82 }
void strengthen(const exprt &expr)
void assignment(const exprt &lhs, const exprt &rhs)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
exprt & lhs()
Definition: std_code.h:208
void make_threaded()
exprt & rhs()
Definition: std_code.h:213
void apply_code(const codet &code)
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
virtual void transform(locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final override
void make_not()
Definition: expr.cpp:91
Definition: ai.h:128
Base class for all expressions.
Definition: expr.h:42
goto_programt::const_targett locationt
Definition: ai.h:44
Assignment.
Definition: std_code.h:195
bool simplify(exprt &expr, const namespacet &ns)