From 7b96b98b4d12a448c6f5fbd6928dba899da23c9a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Mar 2020 16:42:16 +0100
Subject: [PATCH] [Instantiate] No more frama_c_stdlib restriction
---
src/plugins/instantiate/stdlib/calloc.ml | 8 ++++----
src/plugins/instantiate/stdlib/free.ml | 8 ++++----
src/plugins/instantiate/stdlib/malloc.ml | 8 ++++----
src/plugins/instantiate/string/mem_utils.ml | 8 +++-----
src/plugins/instantiate/string/memset.ml | 8 ++++----
5 files changed, 19 insertions(+), 21 deletions(-)
diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
index 89af52fd24d..cebc53197c9 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 ec63f84f4aa..b1adaae34a3 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 fbf3374bcdd..f7b3e9f3b0d 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 02ccd376309..de076b1e3c0 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 21e44be2106..1538ba32be0 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
--
GitLab