CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
value_set_domain_fi.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set Domain (Flow Insensitive)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#include "value_set_domain_fi.h"
14
16 const namespacet &ns,
19 const irep_idt &function_to,
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
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:91
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)
void set_to(const irep_idt &function, unsigned inx)
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
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
Value Set (Flow Insensitive)