[Instantiate] Takes care of constants in Memset

src/plugins/instantiate/basic_blocks.ml

@@ -54,7 +54,8 @@ let exp_type_of_pointed x =
   let no_cast = Cil.stripCasts x in
   if not (Cil.isPointerType (Cil.typeOf no_cast)) then
     match Cil.constFoldToInt x with
-    | Some t when Integer.(equal t (of_int 0)) -> Some (Cil.typeOf x)
+    | Some t when Integer.(equal t (of_int 0)) ->
+      Some (Cil.typeOf_pointed (Cil.typeOf x))
     | _ -> None
   else
     let xt = Cil.unrollTypeDeep (Cil.typeOf no_cast) in

src/plugins/instantiate/string/memset.ml

@@ -175,12 +175,6 @@ let generate_spec (_t, e) { svar = vi } loc =
   let ensures  = generate_ensures e loc t ptr value len in
   make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
 
-let type_from_arg x =
-  let x = Cil.stripCasts x in
-  let xt = Cil.unrollTypeDeep (Cil.typeOf x) in
-  let xt = Cil.type_remove_qualifier_attributes_deep xt in
-  Cil.typeOf_pointed xt
-
 let memset_value e =
   let ff = Integer.of_int 255 in
   match (Cil.constFold false e).enode with
@@ -199,22 +193,25 @@ let rec contains_union_type t =
   | _ -> false
 
 let well_typed_call _ret = function
-  | [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) -> true
-  | [ ptr ; _ ; _ ] when contains_union_type (type_from_arg ptr) -> false
-  | [ ptr ; _ ; _ ] when Cil.isVoidType (type_from_arg ptr) -> false
-  | [ ptr ; _ ; _ ] when not (Cil.isCompleteType (type_from_arg ptr)) -> false
-  | [ _ ; value ; _ ] ->
-    begin match memset_value value with
-      | None -> false
-      | Some _ -> true
+  | [ ptr ; value ; _ ] ->
+    begin match exp_type_of_pointed ptr, memset_value value with
+      | None , _ -> false
+      | Some t, _ when any_char_composed_type t -> true
+      | Some t, _ when contains_union_type t -> false
+      | Some t, _ when Cil.isVoidType t -> false
+      | Some t, _ when not (Cil.isCompleteType t) -> false
+      | _, None -> false
+      | _, Some _ -> true
     end
   | _ -> false
 
 let key_from_call _ret = function
-  | [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) ->
-    (type_from_arg ptr), None
-  | [ ptr ; value ; _ ] when not (contains_union_type (type_from_arg ptr)) ->
-    (type_from_arg ptr), (memset_value value)
+  | [ ptr ; value ; _ ] ->
+    begin match exp_type_of_pointed ptr, memset_value value with
+      | Some t, _ when any_char_composed_type t -> t, None
+      | Some t, value when not (contains_union_type t) -> t, value
+      | _ , _ -> unexpected "trying to generate a key on an ill-typed call"
+    end
   | _ -> unexpected "trying to generate a key on an ill-typed call"
 
 let char_prototype t =
@@ -246,17 +243,18 @@ let generate_prototype = function
   | _, _ ->
     unexpected "trying to generate a prototype on an ill-typed call"
 
-let retype_args (t, e) args =
+let retype_args (_t, e) args =
   match e, args with
   | None, [ ptr ; v ; n ] ->
     let ptr = Cil.stripCasts ptr in
-    assert (any_char_composed_type (type_from_arg ptr)) ;
-    let base_type = base_char_type (type_from_arg ptr) in
+    let base_type = match exp_type_of_pointed ptr with
+      | Some t -> base_char_type t
+      | None -> unexpected "trying to retype arguments on an ill-typed call"
+    in
     let v = Cil.mkCast (Cil.stripCasts v) base_type in
     [ ptr ; v ; n ]
   | Some fv, [ ptr ; v ; n ] ->
     let ptr = Cil.stripCasts ptr in
-    assert (Cil_datatype.Typ.equal (type_from_arg ptr) t) ;
     assert (match memset_value v with Some x when x = fv -> true | _ -> false) ;
     [ ptr ; n ]
   | _ ->