cprover
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  locationt from_l,
20  locationt to_l)
21 {
22  value_set.changed = false;
23 
24  value_set.set_from(from_l->function, from_l->location_number);
25  value_set.set_to(to_l->function, 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 RETURN:
42  case OTHER:
43  case ASSIGN:
44  value_set.apply_code(from_l->code, ns);
45  break;
46 
47  case FUNCTION_CALL:
48  {
49  const code_function_callt &code=
50  to_code_function_call(from_l->code);
51 
52  value_set.do_function_call(to_l->function, code.arguments(), ns);
53  }
54  break;
55 
56  default:
57  {
58  // do nothing
59  }
60  }
61 
62  return (value_set.changed);
63 }
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:1270
value_set_domain_fit::value_set
value_set_fit value_set
Definition: value_set_domain_fi.h:23
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition: flow_insensitive_analysis.cpp:37
value_set_domain_fit::transform
virtual bool transform(const namespacet &ns, locationt from_l, locationt to_l)
Definition: value_set_domain_fi.cpp:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
GOTO
@ GOTO
Definition: goto_program.h:34
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:42
OTHER
@ OTHER
Definition: goto_program.h:37
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
RETURN
@ RETURN
Definition: goto_program.h:45
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
value_set_fit::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition: value_set_fi.cpp:1319
value_set_fit::apply_code
void apply_code(const exprt &code, const namespacet &ns)
Definition: value_set_fi.cpp:1332
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
value_set_fit::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:48