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 
15 #include <util/std_code.h>
16 
18  const namespacet &ns,
19  const irep_idt &function_from,
20  locationt from_l,
21  const irep_idt &function_to,
22  locationt to_l)
23 {
24  value_set.changed = false;
25 
26  value_set.set_from(function_from, from_l->location_number);
27  value_set.set_to(function_to, to_l->location_number);
28 
29  // std::cout << "transforming: " <<
30  // from_l->function << " " << from_l->location_number << " to " <<
31  // to_l->function << " " << to_l->location_number << '\n';
32 
33  switch(from_l->type())
34  {
35  case GOTO:
36  // ignore for now
37  break;
38 
39  case END_FUNCTION:
41  break;
42 
43  case SET_RETURN_VALUE:
44  case OTHER:
45  case ASSIGN:
46  value_set.apply_code(from_l->code(), ns);
47  break;
48 
49  case FUNCTION_CALL:
50  value_set.do_function_call(function_to, from_l->call_arguments(), ns);
51  break;
52 
53  case CATCH:
54  case THROW:
55  case DECL:
56  case DEAD:
57  case ATOMIC_BEGIN:
58  case ATOMIC_END:
59  case START_THREAD:
60  case END_THREAD:
61  case LOCATION:
62  case SKIP:
63  case ASSERT:
64  case ASSUME:
65  case INCOMPLETE_GOTO:
67  // do nothing
68  break;
69  }
70 
71  return (value_set.changed);
72 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
SET_RETURN_VALUE
@ SET_RETURN_VALUE
Definition: goto_program.h:45
value_set_fit::do_function_call
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition: value_set_fi.cpp:1276
value_set_domain_fit::value_set
value_set_fit value_set
Definition: value_set_domain_fi.h:23
value_set_domain_fit::transform
bool transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
Definition: value_set_domain_fi.cpp:17
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition: flow_insensitive_analysis.cpp:31
coverage_criteriont::ASSUME
@ ASSUME
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
THROW
@ THROW
Definition: goto_program.h:50
coverage_criteriont::LOCATION
@ LOCATION
GOTO
@ GOTO
Definition: goto_program.h:34
value_set_fit::apply_code
void apply_code(const codet &code, const namespacet &ns)
Definition: value_set_fi.cpp:1338
value_set_fit::changed
bool changed
Definition: value_set_fi.h:260
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:44
value_set_domain_fi.h
value_set_fit::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:44
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
OTHER
@ OTHER
Definition: goto_program.h:37
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
std_code.h
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
CATCH
@ CATCH
Definition: goto_program.h:51
DECL
@ DECL
Definition: goto_program.h:47
value_set_fit::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition: value_set_fi.cpp:1325
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
DEAD
@ DEAD
Definition: goto_program.h:48
value_set_fit::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:50
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
ASSERT
@ ASSERT
Definition: goto_program.h:36
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52