aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJonathan-Christofer Demay <jcdemay@gmail.com>2009-11-27 16:26:47 +0000
committerJonathan-Christofer Demay <jcdemay@gmail.com>2009-11-27 16:26:47 +0000
commit91625d6c6eea924c4e7f90d2c0ce20d586b33d57 (patch)
treee354eb33a01dc8b88834a84ac5938399e08c088f /sci-mathematics
parentRepomans QA issues in sci-libs (diff)
downloadsci-91625d6c6eea924c4e7f90d2c0ce20d586b33d57.tar.gz
sci-91625d6c6eea924c4e7f90d2c0ce20d586b33d57.tar.bz2
sci-91625d6c6eea924c4e7f90d2c0ce20d586b33d57.zip
sci-mathematics/frama-c20090901: always_init.patch -> fix ptr init
Diffstat (limited to 'sci-mathematics')
-rwxr-xr-x[-rw-r--r--]sci-mathematics/frama-c/files/frama-c-20090901-always_init.patch72
1 files changed, 47 insertions, 25 deletions
diff --git a/sci-mathematics/frama-c/files/frama-c-20090901-always_init.patch b/sci-mathematics/frama-c/files/frama-c-20090901-always_init.patch
index e8c0ff4ed..30753ac17 100644..100755
--- a/sci-mathematics/frama-c/files/frama-c-20090901-always_init.patch
+++ b/sci-mathematics/frama-c/files/frama-c-20090901-always_init.patch
@@ -1,28 +1,50 @@
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-25 16:46:06.000000000 +0000
-@@ -1685,7 +1685,6 @@ let make_well size hidden_base state loc
- loc
- well
++++ 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 =
-@@ -1926,6 +1925,12 @@ let initialize_var_using_type varinfo st
+-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 =
-+ match Cil.unrollType varinfo.vtype with
-+ | TPtr _ -> Relations_type.Model.add_binding_unspecified state
-+ (loc_of_typoffset (Base.create_varinfo varinfo) varinfo.vtype NoOffset)
-+ | _ -> 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 +2039,8 @@ let initial_state_only_globals () =
+@@ -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
@@ -31,7 +53,7 @@ diff -Naurp frama-c-Beryllium-20090901-orig/src/value/eval.ml frama-c-Beryllium-
else complete_init 0 varinfo.vtype [] (Var varinfo,NoOffset)
(* | None ->
(* Cannot initialize with a default when type is incomplete. *)
-@@ -4315,13 +4322,20 @@ let compute_with_initial_state kf initia
+@@ -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 =
@@ -42,26 +64,26 @@ diff -Naurp frama-c-Beryllium-20090901-orig/src/value/eval.ml frama-c-Beryllium-
- (Locations.loc_of_varinfo local))
- initial_state
- f.slocals
-+ if not (Parameters.Dynamic.Bool.get "-always-init-locals")
-+ then
-+ List.fold_left
-+ (fun acc local ->
-+ Relations_type.Model.add_binding_unspecified
-+ acc
-+ (Locations.loc_of_varinfo local))
-+ initial_state
-+ f.slocals
-+ else
++ 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-25 15:07:18.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
@@ -89,7 +111,7 @@ diff -Naurp frama-c-Beryllium-20090901-orig/src/value/value_parameters.ml frama-
(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-25 14:58:46.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