diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml index 89af52fd24d8e1b71b7bc6468b506bdb65bf8c68..cebc53197c970139cab11bfd44936719ff4518cb 100644 --- a/src/plugins/instantiate/stdlib/calloc.ml +++ b/src/plugins/instantiate/stdlib/calloc.ml @@ -131,17 +131,17 @@ let generate_prototype alloc_type = ] in name, (TFun((ptr_of alloc_type), Some params, false, [])) -let well_typed_call ret fct args = +let well_typed_call ret _fct args = match ret, args with - | Some ret, [ _ ; _ ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> + | Some ret, [ _ ; _ ] -> let t = Cil.typeOfLval ret in Cil.isPointerType t && not (Cil.isVoidPtrType t) && Cil.isCompleteType (Cil.typeOf_pointed t) | _ -> false -let key_from_call ret fct _ = +let key_from_call ret _fct _ = match ret with - | Some ret when Cil.hasAttribute "fc_stdlib" fct.vattr -> + | Some ret -> let ret_t = Cil.unrollTypeDeep (Cil.typeOfLval ret) in let ret_t = Cil.type_remove_qualifier_attributes_deep ret_t in Cil.typeOf_pointed ret_t diff --git a/src/plugins/instantiate/stdlib/free.ml b/src/plugins/instantiate/stdlib/free.ml index ec63f84f4aa307d5cec0d97d4ba8f6c5b8f25d0b..b1adaae34a331f69f8b9f4110511a726cda44cb9 100644 --- a/src/plugins/instantiate/stdlib/free.ml +++ b/src/plugins/instantiate/stdlib/free.ml @@ -83,16 +83,16 @@ let generate_prototype alloc_t = ] in name, (TFun(Cil.voidType, Some params, false, [])) -let well_typed_call _ret fct args = +let well_typed_call _ret _fct args = match args with - | [ ptr ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> + | [ ptr ] -> let t = Cil.typeOf (Cil.stripCasts ptr) in Cil.isPointerType t && not (Cil.isVoidPtrType t) | _ -> false -let key_from_call _ret fct args = +let key_from_call _ret _fct args = match args with - | [ ptr ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> + | [ ptr ] -> let ptr = Cil.stripCasts ptr in let ptr_t = Cil.unrollTypeDeep (Cil.typeOf ptr) in let ptr_t = Cil.type_remove_qualifier_attributes_deep ptr_t in diff --git a/src/plugins/instantiate/stdlib/malloc.ml b/src/plugins/instantiate/stdlib/malloc.ml index fbf3374bcdd266c04f82936c4a422e903f64b196..f7b3e9f3b0d3485f7cf7ace2a47d12712b19f0bd 100644 --- a/src/plugins/instantiate/stdlib/malloc.ml +++ b/src/plugins/instantiate/stdlib/malloc.ml @@ -70,17 +70,17 @@ let generate_prototype alloc_t = ] in name, (TFun((ptr_of alloc_t), Some params, false, [])) -let well_typed_call ret fct args = +let well_typed_call ret _fct args = match ret, args with - | Some ret, [ _ ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> + | Some ret, [ _ ] -> let t = Cil.typeOfLval ret in Cil.isPointerType t && not (Cil.isVoidPtrType t) && Cil.isCompleteType (Cil.typeOf_pointed t) | _ -> false -let key_from_call ret fct _ = +let key_from_call ret _fct _ = match ret with - | Some ret when Cil.hasAttribute "fc_stdlib" fct.vattr -> + | Some ret -> let ret_t = Cil.unrollTypeDeep (Cil.typeOfLval ret) in let ret_t = Cil.type_remove_qualifier_attributes_deep ret_t in Cil.typeOf_pointed ret_t diff --git a/src/plugins/instantiate/string/mem_utils.ml b/src/plugins/instantiate/string/mem_utils.ml index 02ccd376309958c77e2e5701327a2567db8d2bbe..de076b1e3c029f90e6ab4698b6ffe971b07c369b 100644 --- a/src/plugins/instantiate/string/mem_utils.ml +++ b/src/plugins/instantiate/string/mem_utils.ml @@ -128,10 +128,9 @@ struct let name = F.name ^ "_" ^ (string_of_typ t) in name, ftype - let well_typed_call lval fct args = + let well_typed_call lval _fct args = let _, ps = F.prototype () in if List.length args <> List.length ps then false - else if not (Cil.hasAttribute "fc_stdlib" fct.vattr) then false else let extract e = function | _, (CPtr | Ptr), _ -> exp_type_of_pointed e @@ -158,12 +157,11 @@ struct in List.map2 retype args ps - let key_from_call _ret fct args = + let key_from_call _ret _fct args = let _, ps = F.prototype () in match ps, args with | (_, (Ptr|CPtr), _) :: ps, fst :: args - when List.(length ps = length args) - && Cil.hasAttribute "fc_stdlib" fct.vattr -> + when List.(length ps = length args) -> begin match exp_type_of_pointed fst with | Value_of t -> t | _ -> diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml index 21e44be2106cd71a710f2a9992cab90110011752..1538ba32be03820bce1499f1dc1d25cdc35be6ff 100644 --- a/src/plugins/instantiate/string/memset.ml +++ b/src/plugins/instantiate/string/memset.ml @@ -195,8 +195,8 @@ let rec contains_union_type t = contains_union_type t | _ -> false -let well_typed_call _ret fct = function - | [ ptr ; value ; _ ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> +let well_typed_call _ret _fct = function + | [ ptr ; value ; _ ] -> begin match Mem_utils.exp_type_of_pointed ptr, memset_value value with | (No_pointed | Of_null _) , _ -> false | Value_of t , _ when any_char_composed_type t -> true @@ -208,8 +208,8 @@ let well_typed_call _ret fct = function end | _ -> false -let key_from_call _ret fct = function - | [ ptr ; value ; _ ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> +let key_from_call _ret _fct = function + | [ ptr ; value ; _ ] -> begin match Mem_utils.exp_type_of_pointed ptr, memset_value value with | Value_of t, _ when any_char_composed_type t -> t, None | Value_of t, value when not (contains_union_type t) -> t, value