From 91625d6c6eea924c4e7f90d2c0ce20d586b33d57 Mon Sep 17 00:00:00 2001 From: Jonathan-Christofer Demay Date: Fri, 27 Nov 2009 16:26:47 +0000 Subject: sci-mathematics/frama-c20090901: always_init.patch -> fix ptr init --- .../files/frama-c-20090901-always_init.patch | 72 ++++++++++++++-------- 1 file changed, 47 insertions(+), 25 deletions(-) mode change 100644 => 100755 sci-mathematics/frama-c/files/frama-c-20090901-always_init.patch (limited to 'sci-mathematics') 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 old mode 100644 new mode 100755 index e8c0ff4ed..30753ac17 --- 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 -- cgit v1.2.3-18-g5258