CBMC
value_set_domain_fi.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Domain (Flow Insensitive)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #include "value_set_domain_fi.h"
14 
16  const namespacet &ns,
17  const irep_idt &function_from,
18  locationt from_l,
19  const irep_idt &function_to,
20  locationt to_l)
21 {
22  value_set.changed = false;
23 
24  value_set.set_from(function_from, from_l->location_number);
25  value_set.set_to(function_to, to_l->location_number);
26 
27  // std::cout << "transforming: " <<
28  // from_l->function << " " << from_l->location_number << " to " <<
29  // to_l->function << " " << to_l->location_number << '\n';
30 
31  switch(from_l->type())
32  {
33  case GOTO:
34  // ignore for now
35  break;
36 
37  case END_FUNCTION:
39  break;
40 
41  case SET_RETURN_VALUE:
42  case OTHER:
43  case ASSIGN:
44  value_set.apply_code(from_l->code(), ns);
45  break;
46 
47  case FUNCTION_CALL:
48  value_set.do_function_call(function_to, from_l->call_arguments(), ns);
49  break;
50 
51  case CATCH:
52  case THROW:
53  case DECL:
54  case DEAD:
55  case ATOMIC_BEGIN:
56  case ATOMIC_END:
57  case START_THREAD:
58  case END_THREAD:
59  case LOCATION:
60  case SKIP:
61  case ASSERT:
62  case ASSUME:
63  case INCOMPLETE_GOTO:
65  // do nothing
66  break;
67  }
68 
69  return (value_set.changed);
70 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
void set_from(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:44
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:50
void apply_code(const codet &code, const namespacet &ns)
void do_end_function(const exprt &lhs, const namespacet &ns)
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
Value Set (Flow Insensitive)