aboutsummaryrefslogtreecommitdiff
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