blob: a597c093bf5db27b7da718e774bcfc4f4fd2eb73 (
plain)
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
|
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-23 23:44:25.000000000 +0000
@@ -4315,13 +4315,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 "-init-locals-defined"
+ then
+ List.fold_right
+ 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-23 23:43:18.000000000 +0000
@@ -136,6 +136,15 @@ module PropagateTop =
let () = add_dependency PropagateTop.self
let () = Plugin.set_group precision_tuning
+module InitLocalsDefined =
+ False
+ (struct
+ let option_name = "-init-locals-defined"
+ let descr = "init local variables defined like initialized extern globals"
+ end)
+let () = add_dependency InitLocalsDefined.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-23 23:43:04.000000000 +0000
@@ -29,6 +29,8 @@ module WarnUnspecifiedOrder: Plugin.BOOL
module PropagateTop: Plugin.BOOL
+module InitLocalsDefined: Plugin.BOOL
+
module AutomaticContextMaxDepth: Plugin.INT
module AutomaticContextMaxWidth: Plugin.INT
|