diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml index 830911e482e7229cdff6c952dd4d45e1023f021a..0fcd642c58fb5f787b7c6be8591ade0b97eeb43b 100644 --- a/src/plugins/instantiate/basic_blocks.ml +++ b/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 diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml index 393f6ae626bc5595188e3a252395c8e845b391c6..3eef4cdd5b9741dd0b14945dc882619acf235574 100644 --- a/src/plugins/instantiate/string/memset.ml +++ b/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 ] | _ ->