cprover
value_set_domain_fivr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Domain (Flow Insensitive, Sharing, Validity Regions)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #include "value_set_domain_fivr.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.set_from(from_l->function, from_l->location_number);
23  value_set.set_to(to_l->function, to_l->location_number);
24 
25  #if 0
26  std::cout << "Transforming: " <<
27  from_l->function << " " << from_l->location_number << " to " <<
28  to_l->function << " " << to_l->location_number << '\n';
29  #endif
30 
31  switch(from_l->type)
32  {
33  case END_FUNCTION:
35  break;
36 
37  case RETURN:
38  case OTHER:
39  case ASSIGN:
40  value_set.apply_code(from_l->code, ns);
41  break;
42 
43  case FUNCTION_CALL:
44  {
45  const code_function_callt &code=
46  to_code_function_call(from_l->code);
47 
48  value_set.do_function_call(to_l->function, code.arguments(), ns);
49  break;
50  }
51 
52  default:
53  {
54  }
55  }
56 
57  return value_set.handover();
58 }
void do_end_function(const exprt &lhs, const namespacet &ns)
void set_from(const irep_idt &function, unsigned inx)
virtual bool transform(const namespacet &ns, locationt from_l, locationt to_l)
void set_to(const irep_idt &function, unsigned inx)
argumentst & arguments()
Definition: std_code.h:1109
void apply_code(const exprt &code, const namespacet &ns)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
codet representation of a function call statement.
Definition: std_code.h:1036
Value Set (Flow Insensitive, Sharing, Validity Regions)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173