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  exprt tmp(from_l->guard);
27 
28  goto_programt::const_targett next=from_l;
29  next++;
30  if(next==to_l)
31  tmp.make_not();
32 
33  simplify(tmp, ns);
35  }
36  break;
37 
38  case ASSERT:
39  case ASSUME:
40  {
41  exprt tmp(from_l->guard);
42  simplify(tmp, ns);
44  }
45  break;
46 
47  case RETURN:
48  // ignore
49  break;
50 
51  case ASSIGN:
52  {
53  const code_assignt &assignment=to_code_assign(from_l->code);
54  invariant_set.assignment(assignment.lhs(), assignment.rhs());
55  }
56  break;
57 
58  case OTHER:
59  if(from_l->code.is_not_nil())
60  invariant_set.apply_code(from_l->code);
61  break;
62 
63  case DECL:
64  invariant_set.apply_code(from_l->code);
65  break;
66 
67  case FUNCTION_CALL:
68  invariant_set.apply_code(from_l->code);
69  break;
70 
71  case START_THREAD:
73  break;
74 
75  default:
76  {
77  // do nothing
78  }
79  }
80 }
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:178
exprt & lhs()
Definition: std_code.h:157
instructionst::const_iterator const_targett
void make_threaded()
exprt & rhs()
Definition: std_code.h:162
void apply_code(const codet &code)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void transform(locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final
void make_not()
Definition: expr.cpp:100
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
goto_programt::const_targett locationt
Definition: ai.h:42
Assignment.
Definition: std_code.h:144
bool simplify(exprt &expr, const namespacet &ns)