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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
diff -Naurp frama-c-Beryllium-20090901-orig/src/value/eval.ml frama-c-Beryllium-20090901-ptch/src/value/eval.ml
--- frama-c-Beryllium-20090901-orig/src/value/eval.ml 2009-08-31 15:38:54.000000000 +0000
+++ frama-c-Beryllium-20090901-ptch/src/value/eval.ml 2009-11-26 02:04:43.000000000 +0000
@@ -1688,7 +1688,7 @@ let make_well size hidden_base state loc
(** [initialize_var_using_type varinfo state] uses the type of [varinfo]
to create an initial value in [state]. *)
-let initialize_var_using_type varinfo state =
+let initialize_all_var_using_type always varinfo state =
CurrentLoc.set varinfo.vdecl;
let rec add_offsetmap depth v name_desc name typ offset_orig typ_orig state =
let typ = Cil.unrollType typ in
@@ -1739,7 +1739,10 @@ let initialize_var_using_type varinfo st
(Cvalue_type.V.top_leaf_origin ())
| TPtr (typ, _) as full_typ
when depth <= Value_parameters.AutomaticContextMaxDepth.get () ->
- let attr = typeAttr full_typ in
+
+ if always then Relations_type.Model.add_binding_unspecified state loc
+
+ else (let attr = typeAttr full_typ in
if not (isVoidType typ) && not (isFunctionType typ) then
let i = match findAttribute "arraylen" attr with
@@ -1806,7 +1809,7 @@ let initialize_var_using_type varinfo st
else
Base.Unknown (Int.zero,Bit_utils.max_bit_address ()))
in
- make_well (Bit_utils.max_bit_size ()) hidden_base state loc
+ make_well (Bit_utils.max_bit_size ()) hidden_base state loc)
| TArray (typ, len, _, _) ->
begin try
@@ -1926,6 +1929,12 @@ let initialize_var_using_type varinfo st
(Base.create_varinfo varinfo)
varinfo.vname varinfo.vname varinfo.vtype NoOffset varinfo.vtype state
+let always_initialize_var_using_type varinfo state =
+ initialize_all_var_using_type true varinfo state
+
+let initialize_var_using_type varinfo state =
+ initialize_all_var_using_type false varinfo state
+
let initial_state_only_globals () =
Value_parameters.feedback "Computing globals values";
let state = ref Relations_type.Model.empty in
@@ -2034,6 +2043,8 @@ let initial_state_only_globals () =
if varinfo.vstorage = Extern then
(* Must not initialize when the storage is extern. *)
state := initialize_var_using_type varinfo !state
+ else if Parameters.Dynamic.Bool.get "-always-init-globals" then
+ state := always_initialize_var_using_type varinfo !state
else complete_init 0 varinfo.vtype [] (Var varinfo,NoOffset)
(* | None ->
(* Cannot initialize with a default when type is incomplete. *)
@@ -4315,13 +4326,20 @@ let compute_with_initial_state kf initia
| Definition (f,_) ->
let initial_state = check_precondition kf initial_state in
let initial_state =
- List.fold_left
- (fun acc local ->
- Relations_type.Model.add_binding_unspecified
- acc
- (Locations.loc_of_varinfo local))
- initial_state
- f.slocals
+ if Parameters.Dynamic.Bool.get "-always-init-locals"
+ then
+ List.fold_right
+ always_initialize_var_using_type
+ f.slocals
+ initial_state
+ else
+ List.fold_left
+ (fun acc local ->
+ Relations_type.Model.add_binding_unspecified
+ acc
+ (Locations.loc_of_varinfo local))
+ initial_state
+ f.slocals
in
compute_using_cfg kf (ref (State_set.singleton initial_state))
diff -Naurp frama-c-Beryllium-20090901-orig/src/value/value_parameters.ml frama-c-Beryllium-20090901-ptch/src/value/value_parameters.ml
--- frama-c-Beryllium-20090901-orig/src/value/value_parameters.ml 2009-08-31 15:38:54.000000000 +0000
+++ frama-c-Beryllium-20090901-ptch/src/value/value_parameters.ml 2009-11-26 02:05:49.000000000 +0000
@@ -136,6 +136,24 @@ module PropagateTop =
let () = add_dependency PropagateTop.self
let () = Plugin.set_group precision_tuning
+module AlwaysInitLocals =
+ False
+ (struct
+ let option_name = "-always-init-locals"
+ let descr = "define uninitialized locals like extern variables"
+ end)
+let () = add_dependency AlwaysInitLocals.self
+
+let () = Plugin.set_group precision_tuning
+module AlwaysInitGlobals =
+ False
+ (struct
+ let option_name = "-always-init-globals"
+ let descr = "define uninitialized globals like extern variables"
+ end)
+let () = add_dependency AlwaysInitGlobals.self
+
+let () = Plugin.set_group precision_tuning
module WideningLevel =
Int
(struct
diff -Naurp frama-c-Beryllium-20090901-orig/src/value/value_parameters.mli frama-c-Beryllium-20090901-ptch/src/value/value_parameters.mli
--- frama-c-Beryllium-20090901-orig/src/value/value_parameters.mli 2009-08-31 15:38:54.000000000 +0000
+++ frama-c-Beryllium-20090901-ptch/src/value/value_parameters.mli 2009-11-26 02:04:43.000000000 +0000
@@ -29,6 +29,9 @@ module WarnUnspecifiedOrder: Plugin.BOOL
module PropagateTop: Plugin.BOOL
+module AlwaysInitLocals: Plugin.BOOL
+module AlwaysInitGlobals: Plugin.BOOL
+
module AutomaticContextMaxDepth: Plugin.INT
module AutomaticContextMaxWidth: Plugin.INT
|
GitWeb