diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 9c669cda9390d35e43e048e6019ba9aa82c09c84..c93566dd8f25aa7f4af928fcf2b80a4f224dd72e 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -945,6 +945,8 @@ src/plugins/occurrence/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/basic_blocks.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/global_context.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/global_context.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/Instantiate.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/instantiator_builder.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/instantiator_builder.mli: CEA_LGPL_OR_PROPRIETARY
@@ -958,6 +960,8 @@ src/plugins/instantiate/stdlib/free.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/stdlib/free.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/stdlib/malloc.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/stdlib/malloc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/mem_utils.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/mem_utils.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/string/memcmp.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/string/memcmp.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/string/memcpy.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.mli
index 061723344f1df682af0b1900e95324f0cc451b5e..4444dd5d95bae406b65c2def46efcd16145479da 100644
--- a/src/plugins/instantiate/Instantiate.mli
+++ b/src/plugins/instantiate/Instantiate.mli
@@ -41,19 +41,20 @@ module Instantiator_builder: sig
(** Name of the implemented instantiator function *)
val function_name: string
- (** [well_typed_call ret args] must return true if and only if the
+ (** [well_typed_call ret fct args] must return true if and only if the
corresponding call is well typed in the sens that the generator can
produce a function override for the corresponding return value and
parameters, according to their types and/or values.
*)
- val well_typed_call: lval option -> exp list -> bool
+ val well_typed_call: lval option -> varinfo -> exp list -> bool
- (** [key_from_call ret args] must return an identifier for the corresponding
- call. [key_from_call ret1 args1] and [key_from_call ret2 args2] must equal
- if and only if the same override function can be used for both call. Any
- call for which [well_typed_call] returns true must be able to give a key.
+ (** [key_from_call ret fct args] must return an identifier for the
+ corresponding call. [key_from_call ret1 fct1 args1] and
+ [key_from_call ret2 fct2 args2] must equal if and only if the same
+ override function can be used for both call. Any call for which
+ [well_typed_call] returns true must be able to give a key.
*)
- val key_from_call: lval option -> exp list -> override_key
+ val key_from_call: lval option -> varinfo -> exp list -> override_key
(** [retype_args key args] must returns a new argument list compatible with
the function identified by [override_key]. [args] is the list of arguments
@@ -99,3 +100,13 @@ module Transform: sig
*)
val register: (module Instantiator_builder.Generator_sig) -> unit
end
+
+module Global_context:sig
+ (** [get_variable name f] searches for an existing variable [name]. If this
+ variable does not exists, it is created using [f].
+
+ The obtained varinfo does not need to be registered, nor [f] needs to
+ perform the registration, it will be done by the transformation.
+ *)
+ val get_variable: string -> (unit -> varinfo) -> varinfo
+end
diff --git a/src/plugins/instantiate/Makefile.in b/src/plugins/instantiate/Makefile.in
index 144f5c7128e6ee8400c61832f24d3ae069027a0a..8635d3bace9d9077ef18361548a18fc660a56aa2 100644
--- a/src/plugins/instantiate/Makefile.in
+++ b/src/plugins/instantiate/Makefile.in
@@ -30,6 +30,7 @@ FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
endif
SRC_STRING:= \
+ mem_utils \
memcmp \
memcpy \
memmove \
@@ -55,7 +56,9 @@ PLUGIN_EXTRA_DIRS:=\
stdlib
PLUGIN_CMI :=
PLUGIN_CMO := \
- options basic_blocks instantiator_builder transform register \
+ options basic_blocks \
+ global_context instantiator_builder \
+ transform register \
$(SRC_STRING) \
$(SRC_STDLIB)
diff --git a/src/plugins/instantiate/global_context.ml b/src/plugins/instantiate/global_context.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9791a78d529581153916776dd28b906b02c35232
--- /dev/null
+++ b/src/plugins/instantiate/global_context.ml
@@ -0,0 +1,90 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Table = Datatype.String.Hashtbl
+
+let varinfos = Table.create 13
+let logic_functions = Table.create 13
+let axiomatics = Table.create 13
+
+let get_variable name make =
+ if Table.mem varinfos name then Table.find varinfos name
+ else begin
+ try Globals.Vars.find_from_astinfo name VGlobal
+ with Not_found ->
+ let vi = make () in
+ Table.add varinfos name vi ;
+ vi
+ end
+
+let get_logic_function name make =
+ if Table.mem logic_functions name then Table.find logic_functions name
+ else begin
+ match Logic_env.find_all_logic_functions name with
+ | [] ->
+ let li = make () in
+ Table.add logic_functions name li ;
+ Logic_utils.add_logic_function li ;
+ li
+ | [x] -> x
+ | _ :: _ -> Options.not_yet_implemented "Logic function overloading"
+ end
+
+let in_axiomatic_functions = Table.create 13
+
+let get_logic_function_in_axiomatic name make =
+ if Table.mem in_axiomatic_functions name then
+ Table.find in_axiomatic_functions name
+ else begin
+ let make_then_find name =
+ let open Cil_types in
+ let (ax_name, ax_list), functions = make () in
+ List.iter
+ (fun f ->
+ Table.add in_axiomatic_functions f.l_var_info.lv_name f ;
+ Logic_utils.add_logic_function f)
+ functions ;
+ Table.add axiomatics ax_name ax_list ;
+ Table.find in_axiomatic_functions name
+ in
+ try match Logic_env.find_all_logic_functions name with
+ | [] -> make_then_find name
+ | [x] -> x
+ | _ :: _ -> Options.not_yet_implemented "Logic function overloading"
+ with Not_found ->
+ Options.fatal "Failed to build %s" name
+ end
+
+let clear () = Table.clear varinfos
+
+let globals loc =
+ let open Cil_types in
+ let l = [] in
+ let l =
+ Table.fold (fun _ x l -> GVarDecl(x, loc) :: l) varinfos l
+ in
+ let annot x loc = GAnnot(x, loc) in
+ let fun_or_pred x loc = annot (Dfun_or_pred (x, loc)) loc in
+ let axiomatic name list loc = annot(Daxiomatic(name, list, [], loc)) loc in
+ let l = Table.fold (fun _ x l -> fun_or_pred x loc :: l) logic_functions l in
+ let l = Table.fold (fun n x l -> axiomatic n x loc :: l) axiomatics l in
+ l
diff --git a/src/plugins/instantiate/global_context.mli b/src/plugins/instantiate/global_context.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9a1456ff0bb26db8834f8857a883749d52e91b8b
--- /dev/null
+++ b/src/plugins/instantiate/global_context.mli
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(** The purpose of this module global definitions when it is needed by
+ instantiation modules.
+*)
+
+(** [get_variable name f] searches for an existing variable [name]. If this
+ variable does not exists, it is created using [f].
+
+ The obtained varinfo does not need to be registered, nor [f] needs to
+ perform the registration, it will be done by the transformation.
+*)
+val get_variable: string -> (unit -> varinfo) -> varinfo
+
+(** [get_logic_function name f] searches for an existing logic function [name].
+ If this function does not exists, it is created using [f]. If the logic
+ function must be part of an axiomatic block **DO NOT** use this function,
+ use [get_logic_function_in_axiomatic].
+
+ Note that function overloading is not supported.
+*)
+val get_logic_function: string -> (unit -> logic_info) -> logic_info
+
+(** [get_logic_function_in_axiomatic name f] searches for an existing logic
+ function [name]. If this function does not exists, an axiomatic definition
+ is created using [f].
+
+ [f] must return:
+ - the axiomatic in a form [name, list of the defintions (incl. functions)]
+ - all functions that are part of the axiomatic definition
+
+ Note that function overloading is not supported.
+*)
+val get_logic_function_in_axiomatic:
+ string ->
+ (unit -> (string * global_annotation list) * logic_info list) ->
+ logic_info
+
+(** Clears internal tables *)
+val clear: unit -> unit
+
+(** Creates a list of global for the elements that have been created *)
+val globals: location -> global list
diff --git a/src/plugins/instantiate/instantiator_builder.ml b/src/plugins/instantiate/instantiator_builder.ml
index df9028d122de56f183632d9571c2f3e3056ec14c..74242ed7bb5f1a50f2fbde264954abda3404141e 100644
--- a/src/plugins/instantiate/instantiator_builder.ml
+++ b/src/plugins/instantiate/instantiator_builder.ml
@@ -28,8 +28,8 @@ module type Generator_sig = sig
type override_key = Hashtbl.key
val function_name: string
- val well_typed_call: lval option -> exp list -> bool
- val key_from_call: lval option -> exp list -> override_key
+ val well_typed_call: lval option -> varinfo -> exp list -> bool
+ val key_from_call: lval option -> varinfo -> exp list -> override_key
val retype_args: override_key -> exp list -> exp list
val args_for_original: override_key -> exp list -> exp list
val generate_prototype: override_key -> (string * typ)
@@ -41,15 +41,14 @@ module type Instantiator = sig
type override_key
val function_name: string
- val well_typed_call: lval option -> exp list -> bool
- val key_from_call: lval option -> exp list -> override_key
+ val well_typed_call: lval option -> varinfo -> exp list -> bool
+ val key_from_call: lval option -> varinfo -> exp list -> override_key
val retype_args: override_key -> exp list -> exp list
val get_override: override_key -> fundec
val get_kfs: unit -> kernel_function list
- val mark_as_computed: ?project:Project.t -> unit -> unit
+ val clear: unit -> unit
end
-
let build_body caller callee args_generator =
let open Extlib in
let loc = Cil_datatype.Location.unknown in
@@ -68,12 +67,13 @@ let build_body caller callee args_generator =
module Make_instantiator (G: Generator_sig) = struct
include G
module Enabled = Options.NewInstantiator (G)
- module Cache = State_builder.Hashtbl (G.Hashtbl) (Cil_datatype.Fundec)
- (struct
- let size = 5
- let dependencies = []
- let name = "Instantiator." ^ G.function_name
- end)
+ module Cache = struct
+ let tbl = G.Hashtbl.create 13
+ let find = G.Hashtbl.find tbl
+ let add = G.Hashtbl.add tbl
+ let fold f = G.Hashtbl.fold f tbl
+ let clear () = G.Hashtbl.clear tbl
+ end
let make_fundec key =
let open Globals.Functions in
@@ -113,5 +113,6 @@ module Make_instantiator (G: Generator_sig) = struct
let get_kfs () =
Cache.fold (fun _ fd l -> Globals.Functions.get fd.svar :: l) []
- let mark_as_computed = Cache.mark_as_computed
+ let clear () =
+ Cache.clear ()
end
diff --git a/src/plugins/instantiate/instantiator_builder.mli b/src/plugins/instantiate/instantiator_builder.mli
index e2432608275499398adeb83d13636fb8ea7f2146..b0eb2f79fcf975b1957079beed9ac29d32c14e6d 100644
--- a/src/plugins/instantiate/instantiator_builder.mli
+++ b/src/plugins/instantiate/instantiator_builder.mli
@@ -40,19 +40,20 @@ module type Generator_sig = sig
(** Name of the implemented function *)
val function_name: string
- (** [well_typed_call ret args] must return true if and only if the
+ (** [well_typed_call ret fct args] must return true if and only if the
corresponding call is well typed in the sens that the generator can
produce a function override for the corresponding return value and
parameters, according to their types and/or values.
*)
- val well_typed_call: lval option -> exp list -> bool
+ val well_typed_call: lval option -> varinfo -> exp list -> bool
- (** [key_from_call ret args] must return an identifier for the corresponding
- call. [key_from_call ret1 args1] and [key_from_call ret2 args2] must equal
- if and only if the same override function can be used for both call. Any
- call for which [well_typed_call] returns true must be able to give a key.
+ (** [key_from_call ret fct args] must return an identifier for the
+ corresponding call. [key_from_call ret1 fct1 args1] and
+ [key_from_call ret2 fct2 args2] must equal if and only if the same
+ override function can be used for both call. Any call for which
+ [well_typed_call] returns true must be able to give a key.
*)
- val key_from_call: lval option -> exp list -> override_key
+ val key_from_call: lval option -> varinfo -> exp list -> override_key
(** [retype_args key args] must returns a new argument list compatible with
the function identified by [override_key]. [args] is the list of arguments
@@ -105,9 +106,9 @@ module type Instantiator = sig
(** Same as [Generator_sig.override_key] *)
val function_name: string
(** Same as [Generator_sig.override_key] *)
- val well_typed_call: lval option -> exp list -> bool
+ val well_typed_call: lval option -> varinfo -> exp list -> bool
(** Same as [Generator_sig.override_key] *)
- val key_from_call: lval option -> exp list -> override_key
+ val key_from_call: lval option -> varinfo -> exp list -> override_key
(** Same as [Generator_sig.override_key] *)
val retype_args: override_key -> exp list -> exp list
@@ -123,10 +124,9 @@ module type Instantiator = sig
*)
val get_kfs: unit -> kernel_function list
- (** [mark_as_computed ?project ()] applies the [mark_as_computed] on the
- internal table.
+ (** [clear ()] clears the internal table of the instantiator.
*)
- val mark_as_computed: ?project:Project.t -> unit -> unit
+ val clear: unit -> unit
end
(** Generates a [Instantiator] from a [Generator_sig] adding all necessary stuff for
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index 41679ef1d11045cfaef1aff637ec7b4f1de63409..a35a97b53e37d96e97149e0bb851c4db758cac6c 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -47,10 +47,56 @@ let valid_size ?loc typ size =
in
new_predicate { p with pred_name = ["correct_size"] }
+let heap_status () =
+ let name = "__fc_heap_status" in
+ let make () =
+ let vi = Cil.makeVarinfo ~ghost:true true false name Cil.intType in
+ vi.vstorage <- Extern ;
+ vi
+ in
+ let vi = Global_context.get_variable name make in
+ Basic_blocks.cvar_to_tvar vi
+
+let make_is_allocable () =
+ let name = "is_allocable" in
+ {
+ l_var_info = Cil_const.make_logic_var_global name (Ctype Cil.voidType) ;
+ l_type = None ;
+ l_tparams = [];
+ l_labels = [FormalLabel("L")];
+ l_profile = [Cil_const.make_logic_var_formal "i" Linteger] ;
+ l_body = LBreads [new_identified_term (heap_status())];
+ }
+
+let make_axiomatic_is_allocable loc () =
+ let is_allocable = make_is_allocable () in
+ let lv_i = Cil_const.make_logic_var_quant "i" Linteger in
+ let t_i = tvar lv_i in
+ let zero = tinteger 0 in
+ let max =
+ tinteger
+ (Integer.to_int
+ (Cil.max_unsigned_number (Cil.bitsSizeOf (size_t ()))))
+ in
+ let label = FormalLabel("L") in
+ let cond = pand (prel (Rlt, t_i, zero), prel (Rgt, t_i, max)) in
+ let app = pnot (papp (is_allocable,[label],[t_i])) in
+ let prop = pforall ([lv_i], pimplies (cond, app)) in
+ let gfun = Dfun_or_pred(is_allocable, loc) in
+ let axiom = Dlemma("never_allocable", true, [label],[],prop,[], loc) in
+ ("dynamic_allocation", [gfun ; axiom]), [is_allocable]
+
+let get_is_allocable loc =
+ Global_context.get_logic_function_in_axiomatic
+ "is_allocable" (make_axiomatic_is_allocable loc)
+
let pis_allocable ?loc size =
- let is_allocable = Logic_env.find_all_logic_functions "is_allocable" in
- let is_allocable = as_singleton is_allocable in
- papp ?loc (is_allocable, [here_label], [size])
+ let loc = match loc with
+ | None -> Cil_datatype.Location.unknown
+ | Some l -> l
+ in
+ let is_allocable = get_is_allocable loc in
+ papp ~loc (is_allocable, [here_label], [size])
let is_allocable ?loc size =
let p = pis_allocable ?loc size in
@@ -60,10 +106,6 @@ let isnt_allocable ?loc size =
let p = pnot ?loc (pis_allocable ?loc size) in
new_predicate { p with pred_name = [ "allocable" ]}
-let heap_status () =
- let heap_status = Globals.Vars.find_from_astinfo "__fc_heap_status" VGlobal in
- Basic_blocks.cvar_to_tvar (heap_status)
-
let assigns_result ?loc typ deps =
let heap_status = new_identified_term (heap_status ()) in
let deps = match deps with
diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
index 86eada6103dfa765956508a1e25c231a346199d9..cebc53197c970139cab11bfd44936719ff4518cb 100644
--- a/src/plugins/instantiate/stdlib/calloc.ml
+++ b/src/plugins/instantiate/stdlib/calloc.ml
@@ -34,7 +34,7 @@ let pset_len_to_zero ?loc alloc_type num size =
let value = match Logic_utils.unroll_type t.term_type with
| Ctype(TPtr(_)) -> term Tnull t.term_type
| Ctype(TFloat(_)) -> treal ?loc 0.
- | Ctype(TInt(_)) -> tinteger ?loc 0
+ | Ctype(TInt(_) | TEnum (_)) -> tinteger ?loc 0
| _ -> unexpected "non atomic type during equality generation"
in
prel ?loc (Req, t, value)
@@ -131,7 +131,7 @@ let generate_prototype alloc_type =
] in
name, (TFun((ptr_of alloc_type), Some params, false, []))
-let well_typed_call ret args =
+let well_typed_call ret _fct args =
match ret, args with
| Some ret, [ _ ; _ ] ->
let t = Cil.typeOfLval ret in
@@ -139,13 +139,13 @@ let well_typed_call ret args =
Cil.isCompleteType (Cil.typeOf_pointed t)
| _ -> false
-let key_from_call ret _ =
+let key_from_call ret _fct _ =
match ret with
| 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
- | None -> unexpected "trying to generate a key on an ill-typed call"
+ | _ -> unexpected "trying to generate a key on an ill-typed call"
let retype_args _typ args = args
let args_for_original _typ args = args
diff --git a/src/plugins/instantiate/stdlib/free.ml b/src/plugins/instantiate/stdlib/free.ml
index 7ef4c509bb20f13e505b79ab71a2feabc99d5436..b1adaae34a331f69f8b9f4110511a726cda44cb9 100644
--- a/src/plugins/instantiate/stdlib/free.ml
+++ b/src/plugins/instantiate/stdlib/free.ml
@@ -83,14 +83,14 @@ let generate_prototype alloc_t =
] in
name, (TFun(Cil.voidType, Some params, false, []))
-let well_typed_call _ret args =
+let well_typed_call _ret _fct args =
match args with
| [ ptr ] ->
let t = Cil.typeOf (Cil.stripCasts ptr) in
Cil.isPointerType t && not (Cil.isVoidPtrType t)
| _ -> false
-let key_from_call _ret args =
+let key_from_call _ret _fct args =
match args with
| [ ptr ] ->
let ptr = Cil.stripCasts ptr in
diff --git a/src/plugins/instantiate/stdlib/malloc.ml b/src/plugins/instantiate/stdlib/malloc.ml
index 16521b530aebe5561a445c1e30216d24b338feef..f7b3e9f3b0d3485f7cf7ace2a47d12712b19f0bd 100644
--- a/src/plugins/instantiate/stdlib/malloc.ml
+++ b/src/plugins/instantiate/stdlib/malloc.ml
@@ -70,7 +70,7 @@ let generate_prototype alloc_t =
] in
name, (TFun((ptr_of alloc_t), Some params, false, []))
-let well_typed_call ret args =
+let well_typed_call ret _fct args =
match ret, args with
| Some ret, [ _ ] ->
let t = Cil.typeOfLval ret in
@@ -78,13 +78,13 @@ let well_typed_call ret args =
Cil.isCompleteType (Cil.typeOf_pointed t)
| _ -> false
-let key_from_call ret _ =
+let key_from_call ret _fct _ =
match ret with
| 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
- | None -> unexpected "trying to generate a key on an ill-typed call"
+ | _ -> unexpected "trying to generate a key on an ill-typed call"
let retype_args _typ args = args
let args_for_original _typ args = args
diff --git a/src/plugins/instantiate/string/mem_utils.ml b/src/plugins/instantiate/string/mem_utils.ml
new file mode 100644
index 0000000000000000000000000000000000000000..de076b1e3c029f90e6ab4698b6ffe971b07c369b
--- /dev/null
+++ b/src/plugins/instantiate/string/mem_utils.ml
@@ -0,0 +1,172 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Basic_blocks
+open Cil_types
+open Logic_const
+
+type kind = CPtr | Ptr | Data of typ
+type action = Strip | Id
+type param = string * kind * action
+type proto = kind * param list
+type 'a spec_gen = location -> typ -> term -> term -> term -> 'a
+
+type pointed_expr_type =
+ | Of_null of typ
+ | Value_of of typ
+ | No_pointed
+
+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)) ->
+ Of_null (Cil.typeOf_pointed (Cil.typeOf x))
+ | _ ->
+ No_pointed
+ else
+ let xt = Cil.unrollTypeDeep (Cil.typeOf no_cast) in
+ let xt = Cil.type_remove_qualifier_attributes_deep xt in
+ Value_of (Cil.typeOf_pointed xt)
+
+let unexpected = Options.fatal "Mem_utils: %s"
+
+let mem2s_typing _ = function
+ | [ dest ; src ; len ] ->
+ (Cil.isIntegralType len) &&
+ (Cil_datatype.Typ.equal dest src) &&
+ (not (Cil.isVoidType dest)) &&
+ (Cil.isCompleteType dest)
+ | _ -> false
+
+let mem2s_spec ~requires ~assigns ~ensures _t { svar = vi } loc =
+ let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
+ | [ dest ; src ; len ] -> dest, src, len
+ | _ -> unexpected "ill-formed fundec in specification generation"
+ in
+ let t = cdest.vtype in
+ let dest = cvar_to_tvar cdest in
+ let src = cvar_to_tvar csrc in
+ let len = cvar_to_tvar clen in
+ let requires = requires loc t dest src len in
+ let assigns = assigns loc t dest src len in
+ let ensures = ensures loc t dest src len in
+ make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
+
+let pcopied_len_bytes ?loc p1 p2 bytes_len =
+ plet_len_div_size ?loc p1.term_type bytes_len
+ (punfold_all_elems_eq ?loc p1 p2)
+
+let memcpy_memmove_common_requires loc _ dest src len =
+ List.map new_predicate [
+ { (pcorrect_len_bytes ~loc dest.term_type len)
+ with pred_name = ["aligned_end"] } ;
+ { (pvalid_len_bytes ~loc here_label dest len)
+ with pred_name = ["valid_dest"] } ;
+ { (pvalid_read_len_bytes ~loc here_label src len)
+ with pred_name = ["valid_read_src"] } ;
+ ]
+
+let memcpy_memmove_common_assigns loc t dest src len =
+ let dest_range = new_identified_term (tunref_range_bytes_len ~loc dest len) in
+ let src_range = new_identified_term(tunref_range_bytes_len ~loc src len) in
+ let copy = dest_range, From [src_range] in
+ let result = new_identified_term (tresult t) in
+ let dest = new_identified_term dest in
+ let res = result, From [dest] in
+ Writes [ copy ; res ]
+
+let presult_dest ?loc t dest =
+ prel ?loc (Req, (tresult ?loc t), dest)
+
+let memcpy_memmove_common_ensures name loc t dest src len =
+ List.map (fun p -> Normal, new_predicate p) [
+ { (pcopied_len_bytes ~loc dest src len) with pred_name = [name] } ;
+ { (presult_dest ~loc t dest) with pred_name = ["result"] }
+ ]
+
+module type Function = sig
+ val name: string
+ val prototype: unit -> proto
+ val well_typed: typ option -> typ list -> bool
+end
+
+module Make (F: Function) =
+struct
+ let generate_function_type t =
+ let to_type = function
+ | CPtr -> ptr_of (const_of t)
+ | Ptr -> ptr_of t
+ | Data t -> t
+ in
+ let ret, ps = F.prototype () in
+ let ret = to_type ret in
+ let ps = List.map (fun (name, kind, _) -> name, (to_type kind), []) ps in
+ TFun(ret, Some ps, false, [])
+
+ let generate_prototype t =
+ let ftype = generate_function_type t in
+ let name = F.name ^ "_" ^ (string_of_typ t) in
+ name, ftype
+
+ let well_typed_call lval _fct args =
+ let _, ps = F.prototype () in
+ if List.length args <> List.length ps then false
+ else
+ let extract e = function
+ | _, (CPtr | Ptr), _ -> exp_type_of_pointed e
+ | _, Data _ , _ -> Value_of (Cil.typeOf e)
+ in
+ let lvt = Extlib.opt_map Cil.typeOfLval lval in
+ let pts = List.map2 extract args ps in
+ let is_no_pointed = function No_pointed -> true | _ -> false in
+ let the_typ = function
+ | No_pointed -> assert false
+ | Value_of t | Of_null t -> t
+ in
+ if List.exists is_no_pointed pts then false
+ else F.well_typed lvt (List.map the_typ pts)
+
+ let retype_args _ args =
+ let _, ps = F.prototype () in
+ if List.length args <> List.length ps then
+ unexpected "trying to retype arguments on an ill-typed call"
+ else
+ let retype x = function
+ | _, _, Strip -> Cil.stripCasts x
+ | _, _, Id -> x
+ in
+ List.map2 retype args ps
+
+ 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) ->
+ begin match exp_type_of_pointed fst with
+ | Value_of t -> t
+ | _ ->
+ unexpected "Mem_utils: trying to get key on an ill-typed call"
+ end
+ | _ ->
+ unexpected "Mem_utils: trying to get key on an ill-typed call"
+end
diff --git a/src/plugins/instantiate/string/mem_utils.mli b/src/plugins/instantiate/string/mem_utils.mli
new file mode 100644
index 0000000000000000000000000000000000000000..2a580c48732ada81908001ff088e88858048da53
--- /dev/null
+++ b/src/plugins/instantiate/string/mem_utils.mli
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type kind = CPtr | Ptr | Data of typ
+type action = Strip | Id
+type param = string * kind * action
+type proto = kind * param list
+
+module type Function = sig
+ val name: string
+
+ val prototype: unit -> proto
+
+ (** receives the type of the lvalue and the types of the arguments received
+ for a call to the function and returns [true] iff they are correct.
+ The received types depend on the [prototype] of the module.
+ - if the kind is [Data t] -> it is the exact type of the expr/lvalue
+ - it the kind is [(C)Ptr] -> it is the pointed type of the expr/lvalue
+ *)
+ val well_typed: typ option -> typ list -> bool
+end
+
+module Make (F: Function) : sig
+ val generate_function_type : typ -> typ
+ val generate_prototype : typ -> string * typ
+ val well_typed_call : lval option -> varinfo -> exp list -> bool
+ val retype_args : typ -> exp list -> exp list
+ val key_from_call : lval option -> varinfo -> exp list -> typ
+end
+
+(** location -> key -> s1 -> s2 -> len -> spec_result *)
+type 'a spec_gen = location -> typ -> term -> term -> term -> 'a
+
+val mem2s_spec:
+ requires: (identified_predicate list) spec_gen ->
+ assigns: assigns spec_gen ->
+ ensures: (termination_kind * identified_predicate) list spec_gen ->
+ typ -> fundec -> location -> funspec
+
+val mem2s_typing: typ option -> typ list -> bool
+
+val memcpy_memmove_common_requires: (identified_predicate list) spec_gen
+
+val memcpy_memmove_common_assigns: assigns spec_gen
+
+val memcpy_memmove_common_ensures:
+ string -> (termination_kind * identified_predicate) list spec_gen
+
+type pointed_expr_type =
+ | Of_null of typ
+ | Value_of of typ
+ | No_pointed
+
+val exp_type_of_pointed: exp -> pointed_expr_type
diff --git a/src/plugins/instantiate/string/memcmp.ml b/src/plugins/instantiate/string/memcmp.ml
index 633294db95b177f66c5f927cfc794f8e7dcc04c3..59969c7ddeed41df219bd4ab7f2bd52d29d2e00c 100644
--- a/src/plugins/instantiate/string/memcmp.ml
+++ b/src/plugins/instantiate/string/memcmp.ml
@@ -26,9 +26,7 @@ open Basic_blocks
let function_name = "memcmp"
-let unexpected = Options.fatal "String.Memcmp: unexpected: %s"
-
-let generate_requires loc s1 s2 len =
+let requires loc _ s1 s2 len =
List.map new_predicate [
{ (pcorrect_len_bytes ~loc s1.term_type len)
with pred_name = ["aligned_end"] } ;
@@ -43,7 +41,7 @@ let presult_memcmp ?loc p1 p2 len =
let res = prel ?loc (Req, (tresult ?loc Cil.intType), (tinteger ?loc 0)) in
piff ?loc (res, eq)
-let generate_assigns loc s1 s2 len =
+let assigns loc _ s1 s2 len =
let indirect_range loc s len =
new_identified_term
{ (tunref_range_bytes_len ~loc s len) with term_name = ["indirect"] }
@@ -57,78 +55,37 @@ let generate_assigns loc s1 s2 len =
let presult_memcmp_len_bytes ?loc p1 p2 bytes_len =
plet_len_div_size ?loc p1.term_type bytes_len (presult_memcmp ?loc p1 p2)
-let generate_ensures loc s1 s2 len =
+let ensures loc _ s1 s2 len =
List.map (fun p -> Normal, new_predicate p) [
{ (presult_memcmp_len_bytes ~loc s1 s2 len) with pred_name = [ "equals" ] }
]
-let generate_spec _t { svar = vi } loc =
- let (c_s1, c_s2, clen) = match Cil.getFormalsDecl vi with
- | [ s1 ; s2 ; len ] -> s1, s2, len
- | _ -> unexpected "ill-formed fundec in specification generation"
- in
- let s1 = cvar_to_tvar c_s1 in
- let s2 = cvar_to_tvar c_s2 in
- let len = cvar_to_tvar clen in
- let requires = generate_requires loc s1 s2 len in
- let assigns = generate_assigns loc s1 s2 len in
- let ensures = generate_ensures loc s1 s2 len in
- make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-
-let generate_function_type t =
- let t = ptr_of (const_of t) in
- let params = [
- ("s1", t, []) ;
- ("s2", t, []) ;
- ("len", size_t (), [])
- ] in
- TFun(Cil.intType, Some params, false, [])
-
-let generate_prototype t =
- let fun_type = generate_function_type t in
- let name = function_name ^ "_" ^ (string_of_typ t) in
- name, fun_type
-
-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 well_typed_call _ret = function
- | [ s1 ; s2 ; len ] ->
- (Cil.isIntegralType (Cil.typeOf len)) &&
- (Cil_datatype.Typ.equal (type_from_arg s1) (type_from_arg s2)) &&
- (not (Cil.isVoidType (type_from_arg s1))) &&
- (Cil.isCompleteType (type_from_arg s1))
- | _ -> false
-
-let key_from_call _ret = function
- | [ s1 ; _ ; _ ] -> type_from_arg s1
- | _ -> unexpected "trying to generate a key on an ill-typed call"
-
-let retype_args override_key = function
- | [ s1 ; s2 ; len ] ->
- let s1 = Cil.stripCasts s1 in
- let s2 = Cil.stripCasts s2 in
- assert (
- Cil_datatype.Typ.equal (type_from_arg s1) override_key &&
- Cil_datatype.Typ.equal (type_from_arg s2) override_key
- ) ;
- [ s1 ; s2 ; len ]
- | _ -> unexpected "trying to retype arguments on an ill-typed call"
-
-let args_for_original _t args = args
+let generate_spec = Mem_utils.mem2s_spec ~requires ~assigns ~ensures
+
+module Function =
+struct
+ open Mem_utils
+ let name = function_name
+ let prototype () =
+ Data Cil.intType,
+ [
+ ("s1" , CPtr,Strip) ;
+ ("s2" , CPtr,Strip) ;
+ ("len", Data (size_t ()) ,Id)
+ ]
+ let well_typed = Mem_utils.mem2s_typing
+end
+module Memcmp_base = Mem_utils.Make(Function)
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
let function_name = function_name
- let well_typed_call = well_typed_call
- let key_from_call = key_from_call
- let retype_args = retype_args
- let generate_prototype = generate_prototype
+ let well_typed_call = Memcmp_base.well_typed_call
+ let key_from_call = Memcmp_base.key_from_call
+ let retype_args = Memcmp_base.retype_args
+ let generate_prototype = Memcmp_base.generate_prototype
let generate_spec = generate_spec
- let args_for_original = args_for_original
+ let args_for_original _ = Extlib.id
end)
diff --git a/src/plugins/instantiate/string/memcpy.ml b/src/plugins/instantiate/string/memcpy.ml
index d0db608eef172febd0665fb56a38d9543131e16a..e56778e6a5714e879f090c0421c121d5ea61dcb6 100644
--- a/src/plugins/instantiate/string/memcpy.ml
+++ b/src/plugins/instantiate/string/memcpy.ml
@@ -23,118 +23,48 @@
open Cil_types
open Logic_const
open Basic_blocks
+open Mem_utils
let function_name = "memcpy"
-let unexpected = Options.fatal "String.Memcpy: unexpected: %s"
-
let pseparated_memcpy_len_bytes ?loc p1 p2 bytes_len =
let generate len = pseparated_memories ?loc p1 len p2 len in
plet_len_div_size ?loc p1.term_type bytes_len generate
-let pcopied_len_bytes ?loc p1 p2 bytes_len =
- plet_len_div_size ?loc p1.term_type bytes_len
- (punfold_all_elems_eq ?loc p1 p2)
-
-let presult_dest ?loc t dest =
- prel ?loc (Req, (tresult ?loc t), dest)
-
-let generate_requires loc dest src len =
- List.map new_predicate [
- { (pcorrect_len_bytes ~loc dest.term_type len)
- with pred_name = ["aligned_end"] } ;
- { (pvalid_len_bytes ~loc here_label dest len)
- with pred_name = ["valid_dest"] } ;
- { (pvalid_read_len_bytes ~loc here_label src len)
- with pred_name = ["valid_read_src"] } ;
- { (pseparated_memcpy_len_bytes ~loc dest src len)
- with pred_name = ["separation"] }
- ]
-
-let generate_assigns loc t dest src len =
- let dest_range = new_identified_term (tunref_range_bytes_len ~loc dest len) in
- let src_range = new_identified_term(tunref_range_bytes_len ~loc src len) in
- let copy = dest_range, From [src_range] in
- let result = new_identified_term (tresult t) in
- let dest = new_identified_term dest in
- let res = result, From [dest] in
- Writes [ copy ; res ]
-
-let generate_ensures loc t dest src len =
- List.map (fun p -> Normal, new_predicate p) [
- { (pcopied_len_bytes ~loc dest src len) with pred_name = [ "copied"] } ;
- { (presult_dest ~loc t dest) with pred_name = [ "result"] }
- ]
-
-let generate_spec _t { svar = vi } loc =
- let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
- | [ dest ; src ; len ] -> dest, src, len
- | _ -> unexpected "ill-formed fundec in specification generation"
+let requires loc t dest src len =
+ let separated = new_predicate
+ { (pseparated_memcpy_len_bytes ~loc dest src len)
+ with pred_name = ["separation"] }
in
- let t = cdest.vtype in
- let dest = cvar_to_tvar cdest in
- let src = cvar_to_tvar csrc in
- let len = cvar_to_tvar clen in
- let requires = generate_requires loc dest src len in
- let assigns = generate_assigns loc t dest src len in
- let ensures = generate_ensures loc t dest src len in
- make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-
-let generate_function_type t =
- let dt = ptr_of t in
- let st = ptr_of (const_of t) in
- let params = [
- ("dest", dt, []) ;
- ("src", st, []) ;
- ("len", size_t (), [])
- ] in
- TFun(dt, Some params, false, [])
-
-let generate_prototype t =
- let fun_type = generate_function_type t in
- let name = function_name ^ "_" ^ (string_of_typ t) in
- name, fun_type
-
-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 well_typed_call _ret = function
- | [ dest ; src ; len ] ->
- (Cil.isIntegralType (Cil.typeOf len)) &&
- (Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src)) &&
- (not (Cil.isVoidType (type_from_arg dest))) &&
- (Cil.isCompleteType (type_from_arg dest))
- | _ -> false
-
-let key_from_call _ret = function
- | [ dest ; _ ; _ ] -> type_from_arg dest
- | _ -> unexpected "trying to generate a key on an ill-typed call"
-
-let retype_args override_key = function
- | [ dest ; src ; len ] ->
- let dest = Cil.stripCasts dest in
- let src = Cil.stripCasts src in
- assert (
- Cil_datatype.Typ.equal (type_from_arg dest) override_key &&
- Cil_datatype.Typ.equal (type_from_arg src) override_key
- ) ;
- [ dest ; src ; len ]
- | _ -> unexpected "trying to retype arguments on an ill-typed call"
-
-let args_for_original _t args = args
+ separated :: (memcpy_memmove_common_requires loc t dest src len)
+
+let assigns = memcpy_memmove_common_assigns
+let ensures = memcpy_memmove_common_ensures "copied"
+let generate_spec = mem2s_spec ~requires ~assigns ~ensures
+
+module Function =
+struct
+ let name = function_name
+ let prototype () =
+ Ptr,
+ [
+ ("dest", Ptr, Strip) ;
+ ("src", CPtr, Strip) ;
+ ("len", Data (size_t()), Id)
+ ]
+ let well_typed = Mem_utils.mem2s_typing
+end
+module Memcpy_base = Mem_utils.Make(Function)
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
let function_name = function_name
- let well_typed_call = well_typed_call
- let key_from_call = key_from_call
- let retype_args = retype_args
- let generate_prototype = generate_prototype
+ let well_typed_call = Memcpy_base.well_typed_call
+ let key_from_call = Memcpy_base.key_from_call
+ let retype_args = Memcpy_base.retype_args
+ let generate_prototype = Memcpy_base.generate_prototype
let generate_spec = generate_spec
- let args_for_original = args_for_original
+ let args_for_original _ = Extlib.id
end)
diff --git a/src/plugins/instantiate/string/memmove.ml b/src/plugins/instantiate/string/memmove.ml
index 6481c423a1ff763ac83f433f801d5872b1d75876..9ce6d75b6bdd8db4598ad0208d393a6cb6ae3059 100644
--- a/src/plugins/instantiate/string/memmove.ml
+++ b/src/plugins/instantiate/string/memmove.ml
@@ -21,114 +21,38 @@
(**************************************************************************)
open Cil_types
-open Logic_const
-open Basic_blocks
+open Mem_utils
let function_name = "memmove"
-let unexpected = Options.fatal "String.Memmove: unexpected: %s"
-
-let pmoved_len_bytes ?loc dest src bytes_len =
- plet_len_div_size ?loc dest.term_type bytes_len
- (punfold_all_elems_eq ?loc dest src)
-
-let presult_dest ?loc t dest =
- prel ?loc (Req, (tresult ?loc t), dest)
-
-let generate_requires loc dest src len =
- List.map new_predicate [
- { (pcorrect_len_bytes ~loc dest.term_type len)
- with pred_name = ["aligned_end"] } ;
- { (pvalid_len_bytes ~loc here_label dest len)
- with pred_name = ["valid_dest"] } ;
- { (pvalid_read_len_bytes ~loc here_label src len)
- with pred_name = ["valid_read_src"] } ;
- ]
-
-let generate_assigns loc t dest src len =
- let dest_range = new_identified_term (tunref_range_bytes_len ~loc dest len) in
- let src_range = new_identified_term(tunref_range_bytes_len ~loc src len) in
- let copy = dest_range, From [src_range] in
- let result = new_identified_term (tresult t) in
- let dest = new_identified_term dest in
- let res = result, From [dest] in
- Writes [ copy ; res ]
-
-let generate_ensures loc t dest src len =
- List.map (fun p -> Normal, new_predicate p) [
- { (pmoved_len_bytes ~loc dest src len) with pred_name = [ "moved"] } ;
- { (presult_dest ~loc t dest) with pred_name = [ "result"] }
- ]
-
-let generate_spec _t { svar = vi } loc =
- let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
- | [ dest ; src ; len ] -> dest, src, len
- | _ -> unexpected "ill-formed fundec in specification generation"
- in
- let t = cdest.vtype in
- let dest = cvar_to_tvar cdest in
- let src = cvar_to_tvar csrc in
- let len = cvar_to_tvar clen in
- let requires = generate_requires loc dest src len in
- let assigns = generate_assigns loc t dest src len in
- let ensures = generate_ensures loc t dest src len in
- make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-
-let generate_function_type t =
- let dt = ptr_of t in
- let st = ptr_of (const_of t) in
- let params = [
- ("dest", dt, []) ;
- ("src", st, []) ;
- ("len", size_t (), [])
- ] in
- TFun(dt, Some params, false, [])
-
-let generate_prototype t =
- let fun_type = generate_function_type t in
- let name = function_name ^ "_" ^ (string_of_typ t) in
- name, fun_type
-
-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 well_typed_call _ret = function
- | [ dest ; src ; len ] ->
- (Cil.isIntegralType (Cil.typeOf len)) &&
- (Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src)) &&
- (not (Cil.isVoidType (type_from_arg dest))) &&
- (Cil.isCompleteType (type_from_arg dest))
- | _ -> false
-
-let key_from_call _ret = function
- | [ dest ; _ ; _ ] -> type_from_arg dest
- | _ -> unexpected "trying to generate a key on an ill-typed call"
-
-let retype_args override_key = function
- | [ dest ; src ; len ] ->
- let dest = Cil.stripCasts dest in
- let src = Cil.stripCasts src in
- assert (
- Cil_datatype.Typ.equal (type_from_arg dest) override_key &&
- Cil_datatype.Typ.equal (type_from_arg src) override_key
- ) ;
- [ dest ; src ; len ]
- | _ -> unexpected "trying to retype arguments on an ill-typed call"
-
-let args_for_original _t args = args
+let requires = memcpy_memmove_common_requires
+let assigns = memcpy_memmove_common_assigns
+let ensures = memcpy_memmove_common_ensures "moved"
+let generate_spec = mem2s_spec ~requires ~assigns ~ensures
+
+module Function =
+struct
+ let name = function_name
+ let prototype () =
+ Ptr,
+ [
+ ("dest", Ptr, Strip);
+ ("src" , CPtr, Strip);
+ ("len", Data (Basic_blocks.size_t()), Id)
+ ]
+ let well_typed = Mem_utils.mem2s_typing
+end
+module Memmove_base = Mem_utils.Make(Function)
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
let function_name = function_name
- let well_typed_call = well_typed_call
- let key_from_call = key_from_call
- let retype_args = retype_args
- let generate_prototype = generate_prototype
+ let well_typed_call = Memmove_base.well_typed_call
+ let key_from_call = Memmove_base.key_from_call
+ let retype_args = Memmove_base.retype_args
+ let generate_prototype = Memmove_base.generate_prototype
let generate_spec = generate_spec
- let args_for_original = args_for_original
+ let args_for_original _ = Extlib.id
end)
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index 393f6ae626bc5595188e3a252395c8e845b391c6..1538ba32be03820bce1499f1dc1d25cdc35be6ff 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -68,7 +68,7 @@ let pset_len_bytes_to_zero ?loc ptr bytes_len =
let value = match Logic_utils.unroll_type t.term_type with
| Ctype(TPtr(_)) -> term Tnull t.term_type
| Ctype(TFloat(_)) -> treal ?loc 0.
- | Ctype(TInt(_)) -> tinteger ?loc 0
+ | Ctype(TInt(_) | TEnum (_)) -> tinteger ?loc 0
| _ -> unexpected "non atomic type during equality generation"
in
prel ?loc (Req, t, value)
@@ -89,15 +89,18 @@ let pset_len_bytes_all_bits_to_one ?loc ptr bytes_len =
papp ?loc ((find_nan_for_type t.term_type), [], [t])
| Ctype(TPtr(_)) ->
pnot ?loc (pvalid_read ?loc (here_label, t))
- | Ctype(TInt(kind, _)) | Ctype(TEnum({ ekind = kind }, _)) ->
+ | Ctype((TInt(kind, _) | TEnum({ ekind = kind }, _)) as typ) ->
let is_signed = Cil.isSigned kind in
let bits = Cil.bitsSizeOfInt kind in
- let value = if is_signed then
- Cil.min_signed_number bits
+ let value =
+ if is_signed then
+ let zero = tinteger ?loc 0 in
+ let zero = Logic_utils.mk_cast ?loc typ zero in
+ term (TUnOp(BNot, zero)) t.term_type
else
- Cil.max_unsigned_number bits
+ let value = Cil.max_unsigned_number bits in
+ term ?loc (TConst (Integer (value,None))) Linteger
in
- let value = term ?loc (TConst (Integer (value,None))) Linteger in
prel ?loc (Req, t, value)
| _ ->
unexpected "non atomic type during equality generation"
@@ -175,12 +178,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
@@ -198,23 +195,26 @@ let rec contains_union_type t =
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
+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
+ | Value_of t , _ when contains_union_type t -> false
+ | Value_of t , _ when Cil.isVoidType t -> false
+ | Value_of 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)
+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
+ | _ , _ -> 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 +246,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 Mem_utils.exp_type_of_pointed ptr with
+ | Value_of t -> base_char_type t
+ | _ -> 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 ]
| _ ->
diff --git a/src/plugins/instantiate/tests/api/external_instantiator_registration.ml b/src/plugins/instantiate/tests/api/external_instantiator_registration.ml
index b800bd1efbdd4bd92fe985fab4771f1f001c95cd..aa3c9b5c6a425206aeae937f7d69d88e2f9db39c 100644
--- a/src/plugins/instantiate/tests/api/external_instantiator_registration.ml
+++ b/src/plugins/instantiate/tests/api/external_instantiator_registration.ml
@@ -1,12 +1,12 @@
let function_name = "mine"
-let well_typed_call _ = function
+let well_typed_call _ _ = function
| [ e ] ->
let t = Cil.typeOf(Cil.stripCasts e) in
not (Cil.isVoidPtrType t) && Cil.isPointerType t
| _ -> false
-let key_from_call _ = function
+let key_from_call _ _ = function
| [ e ] ->
let t = Cil.typeOf(Cil.stripCasts e) in
Cil.typeOf_pointed t
diff --git a/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle b/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle
index 8aacf1fa7571bddc9c3fb5e630e1213db9a447bd..b260fc61afd6d08b2f133412781ca83183fc8f50 100644
--- a/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle
+++ b/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle
@@ -11,16 +11,16 @@ void foo(void)
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
diff --git a/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle b/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle
index cc08c601aac8ee1d7015befe833d0946ebe43eb9..d84cec92ebc1968177fac95b8d64c5fa172c3976 100644
--- a/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle
+++ b/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle
@@ -3,16 +3,16 @@
#include "stddef.h"
#include "string.h"
#include "strings.h"
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
diff --git a/src/plugins/instantiate/tests/plugin/ast_clear.c b/src/plugins/instantiate/tests/plugin/ast_clear.c
new file mode 100644
index 0000000000000000000000000000000000000000..d3dfbb6ad2a2fb83924f23cba30589f680d415e9
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/ast_clear.c
@@ -0,0 +1,9 @@
+/* run.config
+ OPT: -instantiate -then -pp-annot
+*/
+
+#include <string.h>
+
+int foo(char* s1, char* s2, size_t len){
+ return memcmp(s1, s2, len) ;
+}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/plugin/needs_global.i b/src/plugins/instantiate/tests/plugin/needs_global.i
new file mode 100644
index 0000000000000000000000000000000000000000..dfd53797477e08a50c44b80b06ea9743a7a73614
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/needs_global.i
@@ -0,0 +1,14 @@
+/* run.config
+ OPT: -load-script tests/plugin/needs_globals.ml -instantiate -check -print
+*/
+
+int i ; // needed for already_one specifciation
+void already_one(void* parameter) ;
+
+void needs_new(void* parameter) ;
+
+void foo(void){
+ int *i ;
+ already_one(i);
+ needs_new(i);
+}
diff --git a/src/plugins/instantiate/tests/plugin/needs_globals.ml b/src/plugins/instantiate/tests/plugin/needs_globals.ml
new file mode 100644
index 0000000000000000000000000000000000000000..506da455fdb5b23a60a0d994dc2fcfb0e268c021
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/needs_globals.ml
@@ -0,0 +1,80 @@
+let well_typed_call _ _ = function
+ | [ e ] ->
+ let t = Cil.typeOf(Cil.stripCasts e) in
+ not (Cil.isVoidPtrType t) && Cil.isPointerType t
+ | _ -> false
+
+let key_from_call _ _ = function
+ | [ e ] -> Cil.typeOf_pointed (Cil.typeOf(Cil.stripCasts e))
+ | _ -> assert false
+
+let retype_args _ = function
+ | [ e ] -> [ Cil.stripCasts e ]
+ | _ -> assert false
+
+let generate_function_type t =
+ let params = [("x", Cil_types.TPtr(t, []), [])] in
+ Cil_types.TFun(Cil.voidType, Some params, false, [])
+
+let generate_prototype function_name t =
+ let fun_type = generate_function_type t in
+ let name = function_name ^ "_" ^ match t with
+ | Cil_types.TInt(_) -> "int"
+ | _ -> assert false (* nothing else in our test *)
+ in
+ name, fun_type
+
+let generate_spec needed _ _ _ =
+ let open Cil_types in
+ let open Logic_const in
+ let open Instantiate.Global_context in
+ let make () =
+ let vi = Cil.makeVarinfo ~ghost:true true false needed Cil.floatType in
+ vi.vstorage <- Extern ;
+ vi
+ in
+ let vi = get_variable needed make in
+ let t = tvar (Cil.cvar_to_lvar vi) in
+ let assigns =
+ Cil_types.Writes [ Logic_const.new_identified_term t, From [] ]
+ in {
+ spec_behavior = [ {
+ b_name = Cil.default_behavior_name ;
+ b_requires = [] ;
+ b_assumes = [] ;
+ b_post_cond = [] ;
+ b_assigns = assigns ;
+ b_allocation = FreeAllocAny ;
+ b_extended = []
+ } ] ;
+ spec_variant = None ;
+ spec_terminates = None ;
+ spec_complete_behaviors = [] ;
+ spec_disjoint_behaviors = [] ;
+ }
+
+let () = Instantiate.Transform.register (module struct
+ module Hashtbl = Cil_datatype.Typ.Hashtbl
+ type override_key = Hashtbl.key
+
+ let function_name = "already_one"
+ let well_typed_call = well_typed_call
+ let key_from_call = key_from_call
+ let retype_args = retype_args
+ let generate_prototype = generate_prototype function_name
+ let generate_spec = generate_spec "i"
+ let args_for_original _ = Extlib.id
+ end)
+
+let () = Instantiate.Transform.register (module struct
+ module Hashtbl = Cil_datatype.Typ.Hashtbl
+ type override_key = Hashtbl.key
+
+ let function_name = "needs_new"
+ let well_typed_call = well_typed_call
+ let key_from_call = key_from_call
+ let retype_args = retype_args
+ let generate_prototype = generate_prototype function_name
+ let generate_spec = generate_spec "j"
+ let args_for_original _ = Extlib.id
+ end)
diff --git a/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle b/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1a8c67bb4f4a92cf3d5a5f39514eb119d0d7c121
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle
@@ -0,0 +1,2 @@
+[kernel] Parsing tests/plugin/ast_clear.c (with preprocessing)
+[kernel] Parsing tests/plugin/ast_clear.c (with preprocessing)
diff --git a/src/plugins/instantiate/tests/plugin/oracle/needs_global.res.oracle b/src/plugins/instantiate/tests/plugin/oracle/needs_global.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0b7e5b4ccb788b009ffd587ae9e1b13389cd66d0
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/oracle/needs_global.res.oracle
@@ -0,0 +1,34 @@
+[kernel] Parsing tests/plugin/needs_global.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ ghost extern float j; */
+
+int i;
+void already_one(void *parameter);
+
+void needs_new(void *parameter);
+
+/*@ assigns j;
+ assigns j \from \nothing; */
+void needs_new_int(int *x)
+{
+ needs_new((void *)x);
+ return;
+}
+
+/*@ assigns i;
+ assigns i \from \nothing; */
+void already_one_int(int *x)
+{
+ already_one((void *)x);
+ return;
+}
+
+void foo(void)
+{
+ int *i_0;
+ already_one_int(i_0);
+ needs_new_int(i_0);
+ return;
+}
+
+
diff --git a/src/plugins/instantiate/tests/stdlib/calloc.c b/src/plugins/instantiate/tests/stdlib/calloc.c
index 87b1f9338ccb5ecdd99d339551a383459f8305bc..d87508ad415bcf21b677949b5429c8b8b376fc97 100644
--- a/src/plugins/instantiate/tests/stdlib/calloc.c
+++ b/src/plugins/instantiate/tests/stdlib/calloc.c
@@ -11,8 +11,11 @@ struct Flex {
int f[] ;
} ;
+enum E { A, B, C };
+
int main(void){
int* pi = calloc(10, sizeof(int)) ;
+ enum E* pe = calloc(10, sizeof(enum E)) ;
float* pf = calloc(10, sizeof(float)) ;
struct X* px = calloc(10, sizeof(struct X)) ;
char* pc = calloc(10, sizeof(char)) ;
diff --git a/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c b/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
new file mode 100644
index 0000000000000000000000000000000000000000..21498c2ef2b5ab29516316267bc33c5af6d46bbd
--- /dev/null
+++ b/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
@@ -0,0 +1,12 @@
+#include <stddef.h>
+
+void* malloc(size_t s);
+void* calloc(size_t num, size_t size);
+void free(void* ptr);
+
+void foo(void){
+ int * p = malloc(sizeof(int));
+ int * q = calloc(2, sizeof(int));
+ free(p);
+ free(q);
+}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index 28d42c036e394314e15f148be188d770b46886e9..1670641826813ce9b10d06d60f85849cf9e55a57 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
-[instantiate] tests/stdlib/calloc.c:21: Warning: Ignore call: not well typed
-[instantiate] tests/stdlib/calloc.c:22: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/calloc.c:24: Warning:
+ calloc instantiator cannot replace call
+[instantiate] tests/stdlib/calloc.c:25: Warning:
+ calloc instantiator cannot replace call
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -12,6 +14,11 @@ struct Flex {
char c ;
int f[] ;
};
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
requires only_one: num ≡ 1;
@@ -216,6 +223,43 @@ float *calloc_float(size_t num, size_t size)
return __retres;
}
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+enum E *calloc_e_E(size_t num, size_t size)
+{
+ enum E *__retres;
+ __retres = (enum E *)calloc(num,size);
+ return __retres;
+}
+
/*@ requires correct_size: 0 ≡ size % 4;
assigns \result, __fc_heap_status;
assigns \result \from __fc_heap_status, num, size;
@@ -257,6 +301,7 @@ int main(void)
{
int __retres;
int *pi = calloc_int((unsigned int)10,sizeof(int));
+ enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E));
float *pf = calloc_float((unsigned int)10,sizeof(float));
struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
char *pc = calloc_char((unsigned int)10,sizeof(char));
@@ -283,6 +328,11 @@ struct Flex {
char c ;
int f[] ;
};
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
requires only_one: num ≡ 1;
@@ -490,6 +540,44 @@ float *calloc_float(size_t num, size_t size)
return __retres;
}
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+enum E *calloc_e_E(size_t num, size_t size)
+{
+ enum E *__retres;
+ __retres = (enum E *)calloc(num,size);
+ return __retres;
+}
+
/*@ requires correct_size: 0 ≡ size % 4;
assigns \result, __fc_heap_status;
assigns \result \from __fc_heap_status, num, size;
@@ -532,6 +620,7 @@ int main(void)
{
int __retres;
int *pi = calloc_int((unsigned int)10,sizeof(int));
+ enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E));
float *pf = calloc_float((unsigned int)10,sizeof(float));
struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
char *pc = calloc_char((unsigned int)10,sizeof(char));
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
index cfdb769ed8d5e5412d854f0a741ba18d912fcfaf..a0671fe0bc81d0cf757f8660830d2cf9ab1898c8 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing tests/stdlib/free.c (with preprocessing)
-[instantiate] tests/stdlib/free.c:13: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/free.c:13: Warning:
+ free instantiator cannot replace call
/* Generated by Frama-C */
#include "stdlib.h"
struct incomplete;
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index 6cec0abadff6e4e4fd12bfb6d6629c04e09816a6..9aff502467ca08d49dc7d2f346e2e05c6894c995 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[instantiate] tests/stdlib/malloc.c:23: Warning: Ignore call: not well typed
-[instantiate] tests/stdlib/malloc.c:24: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:23: Warning:
+ malloc instantiator cannot replace call
+[instantiate] tests/stdlib/malloc.c:24: Warning:
+ malloc instantiator cannot replace call
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..baa036c870fb4e23d59d27155db86156ea9f5bfb
--- /dev/null
+++ b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle
@@ -0,0 +1,253 @@
+[kernel] Parsing tests/stdlib/no_fc_stdlib.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stddef.h"
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(ℤ i)
+ reads __fc_heap_status;
+
+ axiom never_allocable{L}:
+ ∀ ℤ i; i < 0 ∧ i > 4294967295 ⇒ ¬is_allocable(i);
+
+ }
+
+*/
+void *malloc(size_t s);
+
+void *calloc(size_t num, size_t size);
+
+void free(void *ptr);
+
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_int(int *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *calloc_int(size_t num, size_t size)
+{
+ int *__retres;
+ __retres = (int *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,size);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *malloc_int(size_t size)
+{
+ int *__retres;
+ __retres = (int *)malloc(size);
+ return __retres;
+}
+
+void foo(void)
+{
+ int *p = malloc_int(sizeof(int));
+ int *q = calloc_int((unsigned int)2,sizeof(int));
+ free_int(p);
+ free_int(q);
+ return;
+}
+
+
+[kernel] Parsing tests/stdlib/result/no_fc_stdlib.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stddef.h"
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(ℤ i)
+ reads __fc_heap_status;
+
+ axiom never_allocable{L}:
+ ∀ ℤ i; i < 0 ∧ i > 4294967295 ⇒ ¬is_allocable(i);
+
+ }
+
+*/
+void *malloc(size_t s);
+
+void *calloc(size_t num, size_t size);
+
+void free(void *ptr);
+
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(\old(ptr));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_int(int *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *calloc_int(size_t num, size_t size)
+{
+ int *__retres;
+ __retres = (int *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *malloc_int(size_t size)
+{
+ int *__retres;
+ __retres = (int *)malloc(size);
+ return __retres;
+}
+
+void foo(void)
+{
+ int *p = malloc_int(sizeof(int));
+ int *q = calloc_int((unsigned int)2,sizeof(int));
+ free_int(p);
+ free_int(q);
+ return;
+}
+
+
diff --git a/src/plugins/instantiate/tests/string/memcmp.c b/src/plugins/instantiate/tests/string/memcmp.c
index 404692f9eb118b24ffa7716dceb72b990d973d2e..d8d958e45ed65cd76e23e500c531d6f498ab8c88 100644
--- a/src/plugins/instantiate/tests/string/memcmp.c
+++ b/src/plugins/instantiate/tests/string/memcmp.c
@@ -34,4 +34,11 @@ int with_void(void *s1, void *s2, int n){
struct incomplete ;
int with_incomplete(struct incomplete* s1, struct incomplete* s2, int n){
return memcmp(s1, s2, n);
-}
\ No newline at end of file
+}
+
+void with_null_or_int(int p[10]){
+ memcmp(NULL, p, 10 * sizeof(int));
+ memcmp(p, NULL, 10 * sizeof(int));
+ memcmp((int const*)42, p, 10 * sizeof(int));
+ memcmp(p, (int const*)42, 10 * sizeof(int));
+}
diff --git a/src/plugins/instantiate/tests/string/memcpy.c b/src/plugins/instantiate/tests/string/memcpy.c
index f2c6c03d864470e963082de31044b103dde3a930..fda5fadb75810c7a18c2549b8541046d80c68d79 100644
--- a/src/plugins/instantiate/tests/string/memcpy.c
+++ b/src/plugins/instantiate/tests/string/memcpy.c
@@ -41,4 +41,11 @@ struct incomplete ;
void with_incomplete(struct incomplete* src, struct incomplete* dest, int n){
struct incomplete* res = memcpy(dest, src, n);
memcpy(src, res, n);
-}
\ No newline at end of file
+}
+
+void with_null_or_int(int p[10]){
+ memcpy(NULL, p, 10 * sizeof(int));
+ memcpy(p, NULL, 10 * sizeof(int));
+ memcpy((int*)42, p, 10 * sizeof(int));
+ memcpy(p, (int*)42, 10 * sizeof(int));
+}
diff --git a/src/plugins/instantiate/tests/string/memmove.c b/src/plugins/instantiate/tests/string/memmove.c
index a40698297fd597433f1ced51585f2c1176b285f7..72a5e891aeeffcfa3ec18fc5cbf372aa43734916 100644
--- a/src/plugins/instantiate/tests/string/memmove.c
+++ b/src/plugins/instantiate/tests/string/memmove.c
@@ -42,3 +42,10 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n){
struct incomplete *res = memmove(dest, src, n);
memmove(src, res, n);
}
+
+void with_null_or_int(int p[10]){
+ memmove(NULL, p, 10 * sizeof(int));
+ memmove(p, NULL, 10 * sizeof(int));
+ memmove((int*)42, p, 10 * sizeof(int));
+ memmove(p, (int*)42, 10 * sizeof(int));
+}
diff --git a/src/plugins/instantiate/tests/string/memset_0.c b/src/plugins/instantiate/tests/string/memset_0.c
index ffd73cad6a70f0b48b2e47fa34756d3a982456b3..bb58f3d9c3af3350257485bb6242ba931f89da4b 100644
--- a/src/plugins/instantiate/tests/string/memset_0.c
+++ b/src/plugins/instantiate/tests/string/memset_0.c
@@ -27,6 +27,12 @@ void integer(int dest[10]){
memset(res, 0, 10 * sizeof(int));
}
+enum E { A, B, C } ;
+void with_enum(enum E dest[10]){
+ enum E * res = memset(dest, 0, 10 * sizeof(enum E));
+ memset(res, 0, 10 * sizeof(enum E));
+}
+
void floats(float dest[10]){
float * res = memset(dest, 0, 10 * sizeof(float));
memset(res, 0, 10 * sizeof(float));
@@ -56,3 +62,8 @@ void with_void(void* dest){
void* res = memset(dest, 0, 10);
memset(res, 0, 10);
}
+
+void with_null_or_int(void){
+ memset(NULL, 0, 10);
+ memset((int*) 42, 0, 10);
+}
diff --git a/src/plugins/instantiate/tests/string/memset_FF.c b/src/plugins/instantiate/tests/string/memset_FF.c
index 17c8260b5165b3f8b6ff0fdfd04a2c5c4eabc653..68f3253fc58737341f77805794f8a567b6d000ed 100644
--- a/src/plugins/instantiate/tests/string/memset_FF.c
+++ b/src/plugins/instantiate/tests/string/memset_FF.c
@@ -27,6 +27,12 @@ void integer(int dest[10]){
memset(res, 0xFF, 10 * sizeof(int));
}
+enum E { A, B, C } ;
+void with_enum(enum E dest[10]){
+ enum E * res = memset(dest, 0xFF, 10 * sizeof(enum E));
+ memset(res, 0xFF, 10 * sizeof(enum E));
+}
+
void unsigned_integer(unsigned dest[10]){
unsigned * res = memset(dest, 0xFF, 10 * sizeof(unsigned));
memset(res, 0xFF, 10 * sizeof(unsigned));
@@ -82,3 +88,8 @@ void with_void(void* dest){
void* res = memset(dest, 0xFF, 10);
memset(res, 0xFF, 10);
}
+
+void with_null_or_int(void){
+ memset(NULL, 0xFF, 10);
+ memset((int*) 42, 0xFF, 10);
+}
diff --git a/src/plugins/instantiate/tests/string/memset_value.c b/src/plugins/instantiate/tests/string/memset_value.c
index 432b8ed6a6d3aa03bbb2d99e449641a6e4ac7d1c..ad966713db9b11cef6c1ed3941f92062589730d1 100644
--- a/src/plugins/instantiate/tests/string/memset_value.c
+++ b/src/plugins/instantiate/tests/string/memset_value.c
@@ -27,6 +27,12 @@ void integer(int dest[10], int value){
memset(res, value, 10 * sizeof(int));
}
+enum E { A, B, C } ;
+void with_enum(enum E dest[10], int value){
+ enum E * res = memset(dest, value, 10 * sizeof(enum E));
+ memset(res, value, 10 * sizeof(enum E));
+}
+
void with_named(named dest[10], int value){
named * res = memset(dest, value, 10 * sizeof(named));
memset(res, value, 10 * sizeof(named));
@@ -55,4 +61,9 @@ void with_void(void* dest, int value){
void with_incomplete(struct incomplete* dest, int value){
struct incomplete * res = memset(dest, value, 10);
memset(res, value, 10);
-}
\ No newline at end of file
+}
+
+void with_null_or_int(int value){
+ memset(NULL, value, 10);
+ memset((int*) 42, value, 10);
+}
diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index 18ada799c0a1e0f5e274988851be469c4bc793bc..1f82bcd57b000001f672deb6a8e1f9f34dd3f699 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -1,6 +1,16 @@
[kernel] Parsing tests/string/memcmp.c (with preprocessing)
-[instantiate] tests/string/memcmp.c:31: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcmp.c:36: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcmp.c:31: Warning:
+ memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:36: Warning:
+ memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:40: Warning:
+ memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:41: Warning:
+ memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:42: Warning:
+ memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:43: Warning:
+ memcmp instantiator cannot replace call
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -159,6 +169,17 @@ int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
return tmp;
}
+void with_null_or_int(int * /*[10]*/ p)
+{
+ memcmp((void const *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+ memcmp((void const *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+ memcmp((void const *)((int const *)42),(void const *)p,
+ (unsigned int)10 * sizeof(int));
+ memcmp((void const *)p,(void const *)((int const *)42),
+ (unsigned int)10 * sizeof(int));
+ return;
+}
+
[kernel] Parsing tests/string/result/memcmp.c (with preprocessing)
/* Generated by Frama-C */
@@ -328,4 +349,15 @@ int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
return tmp;
}
+void with_null_or_int(int *p)
+{
+ memcmp((void const *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+ memcmp((void const *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+ memcmp((void const *)((int const *)42),(void const *)p,
+ (unsigned int)10 * sizeof(int));
+ memcmp((void const *)p,(void const *)((int const *)42),
+ (unsigned int)10 * sizeof(int));
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 05681aeb44ef741834b203dad7dc77150b910d34..899dd8afefc6053b12a354ddcec1ba03c5f71842 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -1,8 +1,20 @@
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
-[instantiate] tests/string/memcpy.c:36: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:37: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:42: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:43: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcpy.c:36: Warning:
+ memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:37: Warning:
+ memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:42: Warning:
+ memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:43: Warning:
+ memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:47: Warning:
+ memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:48: Warning:
+ memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:49: Warning:
+ memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:50: Warning:
+ memcpy instantiator cannot replace call
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -13,16 +25,16 @@ struct X {
};
typedef int named;
struct incomplete;
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
@@ -53,16 +65,16 @@ void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: len % 8 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 8;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 8 ≡ 0;
requires
valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 8;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 8;
@@ -86,16 +98,16 @@ void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
@@ -119,17 +131,17 @@ void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: len % 40 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 40;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
\let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 40;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 40;
@@ -173,6 +185,15 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
return;
}
+void with_null_or_int(int * /*[10]*/ p)
+{
+ memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+ memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+ memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
+ memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+ return;
+}
+
[kernel] Parsing tests/string/result/memcpy.c (with preprocessing)
/* Generated by Frama-C */
@@ -185,16 +206,16 @@ struct X {
};
typedef int named;
struct incomplete;
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 4;
@@ -228,16 +249,16 @@ void with_named(named *src, named *dest)
return;
}
-/*@ requires aligned_end: len % 8 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 8;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 8 ≡ 0;
requires
valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 8;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 8;
@@ -264,16 +285,16 @@ void structure(struct X *src, struct X *dest)
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 4;
@@ -299,17 +320,17 @@ void pointers(int **src, int **dest)
return;
}
-/*@ requires aligned_end: len % 40 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 40;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
\let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 40;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 40;
@@ -356,4 +377,13 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
return;
}
+void with_null_or_int(int *p)
+{
+ memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+ memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+ memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
+ memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index 15c80507c4a17b1b2c366d5ce5cccfacb4008a46..f327581499bdc3f2393d4bd573a08d587761e1df 100644
--- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
@@ -1,8 +1,20 @@
[kernel] Parsing tests/string/memmove.c (with preprocessing)
-[instantiate] tests/string/memmove.c:36: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:37: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:42: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:43: Warning: Ignore call: not well typed
+[instantiate] tests/string/memmove.c:36: Warning:
+ memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:37: Warning:
+ memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:42: Warning:
+ memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:43: Warning:
+ memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:47: Warning:
+ memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:48: Warning:
+ memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:49: Warning:
+ memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:50: Warning:
+ memmove instantiator cannot replace call
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -157,6 +169,15 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
return;
}
+void with_null_or_int(int * /*[10]*/ p)
+{
+ memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+ memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+ memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
+ memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+ return;
+}
+
[kernel] Parsing tests/string/result/memmove.c (with preprocessing)
/* Generated by Frama-C */
@@ -324,4 +345,13 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
return;
}
+void with_null_or_int(int *p)
+{
+ memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+ memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+ memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
+ memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
index 1b7efe66ddfaf3924b521e046ee4ebff7779483e..dae2db7eba374181cfa6fe5705cbcd211dfeaed5 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -1,6 +1,12 @@
[kernel] Parsing tests/string/memset_0.c (with preprocessing)
-[instantiate] tests/string/memset_0.c:56: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_0.c:57: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_0.c:62: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_0.c:63: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_0.c:67: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_0.c:68: Warning:
+ memset instantiator cannot replace call
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -10,6 +16,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -111,6 +122,32 @@ void integer(int * /*[10]*/ dest)
return;
}
+/*@ requires aligned_end: len % 4 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+ ensures
+ set_content:
+ \let __fc_len = len / 4;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 0;
+ ensures result: \result ≡ ptr;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+enum E *memset_e_E_0(enum E *ptr, size_t len)
+{
+ enum E *__retres;
+ __retres = (enum E *)memset((void *)ptr,0,len);
+ return __retres;
+}
+
+void with_enum(enum E * /*[10]*/ dest)
+{
+ enum E *res = memset_e_E_0(dest,(unsigned int)10 * sizeof(enum E));
+ memset_e_E_0(res,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
@@ -233,6 +270,13 @@ void with_void(void *dest)
return;
}
+void with_null_or_int(void)
+{
+ memset((void *)0,0,(unsigned int)10);
+ memset((void *)((int *)42),0,(unsigned int)10);
+ return;
+}
+
[kernel] Parsing tests/string/result/memset_0.c (with preprocessing)
/* Generated by Frama-C */
@@ -244,6 +288,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -350,6 +399,32 @@ void integer(int *dest)
return;
}
+/*@ requires aligned_end: len % 4 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+ ensures
+ set_content:
+ \let __fc_len = \old(len) / 4;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 0;
+ ensures result: \result ≡ \old(ptr);
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+enum E *memset_e_E_0(enum E *ptr, size_t len)
+{
+ enum E *__retres;
+ __retres = (enum E *)memset((void *)ptr,0,len);
+ return __retres;
+}
+
+void with_enum(enum E *dest)
+{
+ enum E *res = memset_e_E_0(dest,(unsigned int)10 * sizeof(enum E));
+ memset_e_E_0(res,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
@@ -473,4 +548,11 @@ void with_void(void *dest)
return;
}
+void with_null_or_int(void)
+{
+ memset((void *)0,0,(unsigned int)10);
+ memset((void *)((int *)42),0,(unsigned int)10);
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
index ffe160d7caa31fe89b889cdcc11c09f58f3192ab..137dd1c21a070c374f27367c3e82beb2b47a79aa 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -1,6 +1,12 @@
[kernel] Parsing tests/string/memset_FF.c (with preprocessing)
-[instantiate] tests/string/memset_FF.c:82: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_FF.c:83: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_FF.c:88: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_FF.c:89: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_FF.c:93: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_FF.c:94: Warning:
+ memset instantiator cannot replace call
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -10,6 +16,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -92,7 +103,7 @@ void nested_chars(char (* /*[10]*/ dest)[10])
ensures
set_content:
\let __fc_len = len / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -2147483648;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((int)0);
ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 4 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
@@ -112,6 +123,32 @@ void integer(int * /*[10]*/ dest)
return;
}
+/*@ requires aligned_end: len % 4 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+ ensures
+ set_content:
+ \let __fc_len = len / 4;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 4294967295;
+ ensures result: \result ≡ ptr;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+enum E *memset_e_E_FF(enum E *ptr, size_t len)
+{
+ enum E *__retres;
+ __retres = (enum E *)memset((void *)ptr,255,len);
+ return __retres;
+}
+
+void with_enum(enum E * /*[10]*/ dest)
+{
+ enum E *res = memset_e_E_FF(dest,(unsigned int)10 * sizeof(enum E));
+ memset_e_E_FF(res,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
@@ -145,7 +182,7 @@ void unsigned_integer(unsigned int * /*[10]*/ dest)
ensures
set_content:
\let __fc_len = len / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -2147483648;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((long)0);
ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 4 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
@@ -198,8 +235,7 @@ void unsigned_long_integer(unsigned long * /*[10]*/ dest)
ensures
set_content:
\let __fc_len = len / 8;
- ∀ ℤ j0;
- 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -9223372036854775808;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((long long)0);
ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
@@ -289,7 +325,7 @@ void with_named(named * /*[10]*/ dest)
\let __fc_len = len / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
- (ptr + j0)->x ≡ -2147483648 ∧ (ptr + j0)->y ≡ -2147483648;
+ (ptr + j0)->x ≡ ~((int)0) ∧ (ptr + j0)->y ≡ ~((int)0);
ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
@@ -343,7 +379,7 @@ void pointers(int ** /*[10]*/ dest)
\let __fc_len = len / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
- (∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ -2147483648);
+ (∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ ~((int)0));
ensures result: \result ≡ ptr;
assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1] \from \nothing;
@@ -371,6 +407,13 @@ void with_void(void *dest)
return;
}
+void with_null_or_int(void)
+{
+ memset((void *)0,0xFF,(unsigned int)10);
+ memset((void *)((int *)42),0xFF,(unsigned int)10);
+ return;
+}
+
[kernel] Parsing tests/string/result/memset_FF.c (with preprocessing)
/* Generated by Frama-C */
@@ -382,6 +425,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -469,7 +517,7 @@ void nested_chars(char (*dest)[10])
ensures
set_content:
\let __fc_len = \old(len) / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -2147483648;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((int)0);
ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 4 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
@@ -489,6 +537,32 @@ void integer(int *dest)
return;
}
+/*@ requires aligned_end: len % 4 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+ ensures
+ set_content:
+ \let __fc_len = \old(len) / 4;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 4294967295;
+ ensures result: \result ≡ \old(ptr);
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+enum E *memset_e_E_FF(enum E *ptr, size_t len)
+{
+ enum E *__retres;
+ __retres = (enum E *)memset((void *)ptr,255,len);
+ return __retres;
+}
+
+void with_enum(enum E *dest)
+{
+ enum E *res = memset_e_E_FF(dest,(unsigned int)10 * sizeof(enum E));
+ memset_e_E_FF(res,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
@@ -522,7 +596,7 @@ void unsigned_integer(unsigned int *dest)
ensures
set_content:
\let __fc_len = \old(len) / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -2147483648;
+ ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((long)0);
ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 4 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
@@ -576,7 +650,7 @@ void unsigned_long_integer(unsigned long *dest)
set_content:
\let __fc_len = \old(len) / 8;
∀ ℤ j0;
- 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -9223372036854775808;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((long long)0);
ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
@@ -666,8 +740,8 @@ void with_named(named *dest)
\let __fc_len = \old(len) / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
- (\old(ptr) + j0)->x ≡ -2147483648 ∧
- (\old(ptr) + j0)->y ≡ -2147483648;
+ (\old(ptr) + j0)->x ≡ ~((int)0) ∧
+ (\old(ptr) + j0)->y ≡ ~((int)0);
ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
@@ -722,7 +796,7 @@ void pointers(int **dest)
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
- 0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ -2147483648);
+ 0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ ~((int)0));
ensures result: \result ≡ \old(ptr);
assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1] \from \nothing;
@@ -750,4 +824,11 @@ void with_void(void *dest)
return;
}
+void with_null_or_int(void)
+{
+ memset((void *)0,0xFF,(unsigned int)10);
+ memset((void *)((int *)42),0xFF,(unsigned int)10);
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
index f71268da3aab3046b86c67795177069ebc7de2f2..7185fe7a66598d4ad182720f927ea6e5f4ed4a8b 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/string/memset_nested_union.c (with preprocessing)
[instantiate] tests/string/memset_nested_union.c:10: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
index 462fc372857d8a254614e0759e958ffd2d99b85d..5ece8370f6baf098afc773974cb82a40f53df732 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -1,32 +1,40 @@
[kernel] Parsing tests/string/memset_value.c (with preprocessing)
[instantiate] tests/string/memset_value.c:26: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
[instantiate] tests/string/memset_value.c:27: Warning:
- Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:31: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
[instantiate] tests/string/memset_value.c:32: Warning:
- Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:36: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:33: Warning:
+ memset instantiator cannot replace call
[instantiate] tests/string/memset_value.c:37: Warning:
- Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:41: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:38: Warning:
+ memset instantiator cannot replace call
[instantiate] tests/string/memset_value.c:42: Warning:
- Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:46: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:43: Warning:
+ memset instantiator cannot replace call
[instantiate] tests/string/memset_value.c:47: Warning:
- Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:51: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:48: Warning:
+ memset instantiator cannot replace call
[instantiate] tests/string/memset_value.c:52: Warning:
- Ignore call: not well typed
-[instantiate] tests/string/memset_value.c:56: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:53: Warning:
+ memset instantiator cannot replace call
[instantiate] tests/string/memset_value.c:57: Warning:
- Ignore call: not well typed
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:58: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:62: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:63: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:67: Warning:
+ memset instantiator cannot replace call
+[instantiate] tests/string/memset_value.c:68: Warning:
+ memset instantiator cannot replace call
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -36,6 +44,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
@@ -119,6 +132,13 @@ void integer(int * /*[10]*/ dest, int value)
return;
}
+void with_enum(enum E * /*[10]*/ dest, int value)
+{
+ enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E));
+ memset((void *)res,value,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
void with_named(named * /*[10]*/ dest, int value)
{
named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named));
@@ -163,6 +183,13 @@ void with_incomplete(struct incomplete *dest, int value)
return;
}
+void with_null_or_int(int value)
+{
+ memset((void *)0,value,(unsigned int)10);
+ memset((void *)((int *)42),value,(unsigned int)10);
+ return;
+}
+
[kernel] Parsing tests/string/result/memset_value.c (with preprocessing)
/* Generated by Frama-C */
@@ -174,6 +201,11 @@ struct X {
int y ;
};
typedef int named;
+enum E {
+ A = 0,
+ B = 1,
+ C = 2
+};
struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
@@ -262,6 +294,13 @@ void integer(int *dest, int value)
return;
}
+void with_enum(enum E *dest, int value)
+{
+ enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E));
+ memset((void *)res,value,(unsigned int)10 * sizeof(enum E));
+ return;
+}
+
void with_named(named *dest, int value)
{
named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named));
@@ -306,4 +345,11 @@ void with_incomplete(struct incomplete *dest, int value)
return;
}
+void with_null_or_int(int value)
+{
+ memset((void *)0,value,(unsigned int)10);
+ memset((void *)((int *)42),value,(unsigned int)10);
+ return;
+}
+
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 28f7a1ca81145cb2e7b414d21a0218b59ec6905f..590ee506dbdb151d26053806b4baa26e4f15d373 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -29,12 +29,6 @@ let register (module G: Generator_sig) =
let module Instantiator = Make_instantiator(G) in
Hashtbl.add base G.function_name (module Instantiator)
-let mark_as_computed () =
- let mark_as_computed _ instantiator =
- let module I = (val instantiator: Instantiator) in I.mark_as_computed ()
- in
- Hashtbl.iter mark_as_computed base
-
let get_kfs () =
let get_kfs _ instantiator =
let module I = (val instantiator: Instantiator) in
@@ -43,6 +37,14 @@ let get_kfs () =
in
Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base []
+let clear () =
+ Global_context.clear () ;
+ let clear _ instantiator =
+ let module I = (val instantiator: Instantiator) in
+ I.clear ()
+ in
+ Hashtbl.iter clear base
+
module VISet = Cil_datatype.Varinfo.Hptset
class transformer = object(self)
@@ -53,9 +55,9 @@ class transformer = object(self)
method! vfile _ =
let post f =
+ f.globals <- (Global_context.globals (Cil.CurrentLoc.get())) @ f.globals ;
Ast.mark_as_changed () ;
Ast.mark_as_grown () ;
- mark_as_computed () ;
f
in
Cil.DoChildrenPost post
@@ -90,14 +92,15 @@ class transformer = object(self)
method private replace_call (lval, fct, args) =
try
let module I = (val (self#find_enabled_instantiator fct): Instantiator) in
- if I.well_typed_call lval args then
- let key = I.key_from_call lval args in
+ if I.well_typed_call lval fct args then
+ let key = I.key_from_call lval fct args in
let fundec = I.get_override key in
let new_args = I.retype_args key args in
Queue.add fundec used_instantiator_last_kf ;
(fundec.svar), new_args
else begin
- Options.warning ~current:true "Ignore call: not well typed" ;
+ Options.warning
+ ~current:true "%s instantiator cannot replace call" fct.vname ;
(fct, args)
end
with
@@ -158,5 +161,7 @@ let compute_statuses_all_kfs () =
List.iter compute_comp_disj_statuses kfs
let transform file =
+ clear () ;
Visitor.visitFramacFile (new transformer) file ;
+ File.reorder_ast () ;
compute_statuses_all_kfs ()
diff --git a/tests/syntax/ast_init.ml b/tests/syntax/ast_init.ml
index b0520cc04b97cac07a59159c9c944fd6722c539a..f0e57935a236f696af9949647edb7ec78d06fb81 100644
--- a/tests/syntax/ast_init.ml
+++ b/tests/syntax/ast_init.ml
@@ -8,6 +8,7 @@ let apply _ =
(fun b -> b.bstmts <-
Cil.mkStmtOneInstr (Skip (Cil_datatype.Stmt.loc s)) :: b.bstmts)
l;
+ File.must_recompute_cfg (Kernel_function.get_definition f) ;
Ast.mark_as_grown ()
let () = Ast.apply_after_computed apply