-
Notifications
You must be signed in to change notification settings - Fork 273
/
Copy pathvalue_set_domain_fi.cpp
70 lines (56 loc) · 1.5 KB
/
value_set_domain_fi.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
/*******************************************************************\
Module: Value Set Domain (Flow Insensitive)
Author: Daniel Kroening, [email protected]
CM Wintersteiger
\*******************************************************************/
/// \file
/// Value Set Domain (Flow Insensitive)
#include "value_set_domain_fi.h"
bool value_set_domain_fit::transform(
const namespacet &ns,
const irep_idt &function_from,
locationt from_l,
const irep_idt &function_to,
locationt to_l)
{
value_set.changed = false;
value_set.set_from(function_from, from_l->location_number);
value_set.set_to(function_to, to_l->location_number);
// std::cout << "transforming: " <<
// from_l->function << " " << from_l->location_number << " to " <<
// to_l->function << " " << to_l->location_number << '\n';
switch(from_l->type())
{
case GOTO:
// ignore for now
break;
case END_FUNCTION:
value_set.do_end_function(get_return_lhs(to_l), ns);
break;
case SET_RETURN_VALUE:
case OTHER:
case ASSIGN:
value_set.apply_code(from_l->code(), ns);
break;
case FUNCTION_CALL:
value_set.do_function_call(function_to, from_l->call_arguments(), ns);
break;
case CATCH:
case THROW:
case DECL:
case DEAD:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case LOCATION:
case SKIP:
case ASSERT:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
// do nothing
break;
}
return (value_set.changed);
}