cprover
value_set_domain.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "value_set_domain.h"
13 
14 #include <util/std_code.h>
15 
17  const namespacet &ns,
18  locationt from_l,
19  locationt to_l)
20 {
21  switch(from_l->type)
22  {
23  case GOTO:
24  // ignore for now
25  break;
26 
27  case END_FUNCTION:
29  break;
30 
31  case RETURN:
32  case OTHER:
33  case ASSIGN:
34  case DECL:
35  value_set.apply_code(from_l->code, ns);
36  break;
37 
38  case ASSUME:
39  value_set.guard(from_l->guard, ns);
40  break;
41 
42  case FUNCTION_CALL:
43  {
44  const code_function_callt &code=
45  to_code_function_call(from_l->code);
46 
47  value_set.do_function_call(to_l->function, code.arguments(), ns);
48  }
49  break;
50 
51  default:
52  {
53  // do nothing
54  }
55  }
56 }
static exprt get_return_lhs(locationt to)
goto_programt::const_targett locationt
argumentst & arguments()
Definition: std_code.h:689
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition: value_set.cpp:1423
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition: value_set.cpp:1469
virtual void transform(const namespacet &ns, locationt from_l, locationt to_l)
void guard(const exprt &expr, const namespacet &ns)
Definition: value_set.cpp:1616
void apply_code(const codet &code, const namespacet &ns)
Definition: value_set.cpp:1481
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700