diff --git a/src/plugins/instantiate/Makefile.in b/src/plugins/instantiate/Makefile.in
index d316b8c7c15c26f85da43d2099680ac6d968b801..144f5c7128e6ee8400c61832f24d3ae069027a0a 100644
--- a/src/plugins/instantiate/Makefile.in
+++ b/src/plugins/instantiate/Makefile.in
@@ -55,14 +55,14 @@ PLUGIN_EXTRA_DIRS:=\
stdlib
PLUGIN_CMI :=
PLUGIN_CMO := \
- basic_blocks options instantiator_builder transform register \
+ options basic_blocks instantiator_builder transform register \
$(SRC_STRING) \
$(SRC_STDLIB)
PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
#PLUGIN_NO_DEFAULT_TEST := no
-PLUGIN_TESTS_DIRS := string stdlib options api
+PLUGIN_TESTS_DIRS := string stdlib options api plugin
################
# Generic part #
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index c525eb2cd2b72e1beb49cf07e646bfcdd73504c4..660db8c83c08e4939599cbd5819d41428f31515f 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -73,7 +73,8 @@ let rec string_of_typ_aux = function
| TComp (ci, _, _) -> "un_" ^ ci.cname
| TArray (t, Some e, _, _) ->
"arr" ^ (string_of_exp e) ^ "_" ^ string_of_typ t
- | _ -> assert false
+ | t ->
+ Options.fatal "unsupported type %a" Cil_printer.pp_typ t
and string_of_typ t = string_of_typ_aux (Cil.unrollType t)
and string_of_exp e = Format.asprintf "%a" Cil_printer.pp_exp e
@@ -111,9 +112,10 @@ let tplus ?loc t1 t2 =
let tdivide ?loc t1 t2 =
term ?loc (TBinOp(Div, t1, t2)) t1.term_type
-let ttype_of_pointed = function
+let ttype_of_pointed t =
+ match Logic_utils.unroll_type t with
| Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Ctype t
- | _ -> assert false
+ | _ -> Options.fatal "ttype_of_pointed on a non pointer type"
let tbuffer_range ?loc ptr len =
let last = tminus ?loc len (tinteger ?loc 1) in
@@ -139,9 +141,9 @@ and tunref_range_unfold ?loc lval typ =
let taccess ?loc ptr offset =
let get_lval = function
| TLval(lval) -> lval
- | _ -> assert false
+ | _ -> Options.fatal "unexpected non-lvalue on call to taccess"
in
- match ptr.term_type with
+ match Logic_utils.unroll_type ptr.term_type with
| Ctype(TPtr(_)) ->
let address = tplus ?loc ptr offset in
let lval = TLval(TMem(address), TNoOffset) in
@@ -150,19 +152,15 @@ let taccess ?loc ptr offset =
let lval = get_lval ptr.term_node in
let lval = addTermOffsetLval (TIndex(offset, TNoOffset)) lval in
term ?loc (TLval lval) (ttype_of_pointed ptr.term_type)
- | _ -> assert false
+ | _ -> Options.fatal "taccess on a non pointer type"
let sizeofpointed = function
| Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Cil.bytesSizeOf t
- | _ -> assert false
+ | _ -> Options.fatal "size_of_pointed on a non pointer type"
let sizeof = function
| Ctype t -> Cil.bytesSizeOf t
- | _ -> assert false
-
-let unroll_logic_type = function
- | Ctype t -> Ctype (Cil.unrollType t)
- | t -> t
+ | _ -> Options.fatal "sizeof on a non C type"
let tunref_range_bytes_len ?loc ptr bytes_len =
let sizeof = sizeofpointed ptr.term_type in
@@ -218,7 +216,7 @@ and pall_elems_eq ?loc depth t1 t2 len =
let eq = peq_unfold ?loc (depth+1) t1_acc t2_acc in
pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
and peq_unfold ?loc depth t1 t2 =
- match unroll_logic_type t1.term_type with
+ match Logic_utils.unroll_type t1.term_type with
| Ctype(TArray(_, Some len, _, _)) ->
let len = Logic_utils.expr_to_term ~cast:false len in
pall_elems_eq ?loc depth t1 t2 len
@@ -234,12 +232,14 @@ and pall_elems_pred ?loc depth t1 len pred =
let eq = punfold_pred ?loc depth t1_acc pred in
pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
and punfold_pred ?loc ?(dyn_len = None) depth t1 pred =
- match unroll_logic_type t1.term_type with
+ match Logic_utils.unroll_type t1.term_type with
| Ctype(TArray(_, opt_len, _, _)) ->
- let len = match opt_len, dyn_len with
+ let len =
+ match opt_len, dyn_len with
| Some len, None -> Logic_utils.expr_to_term ~cast:false len
| _ , Some len -> len
- | None, None -> assert false
+ | None, None ->
+ Options.fatal "Unfolding array: cannot find a length"
in
pall_elems_pred ?loc (depth+1) t1 len pred
| Ctype(TComp(ci, _, _)) ->
@@ -253,9 +253,9 @@ and pall_fields_pred ?loc ?(flex_mem_len=None) depth t1 ci pred =
punfold_pred ?loc ~dyn_len depth term pred
in
let rec eqs_fields = function
+ | [] -> []
| [ x ] -> [ eq flex_mem_len x ]
| x :: l -> let x' = eq None x in x' :: (eqs_fields l)
- | _ -> assert false
in
pands (eqs_fields ci.cfields)
@@ -263,7 +263,7 @@ let punfold_flexible_struct_pred ?loc the_struct bytes_len pred =
let struct_len = tinteger ?loc (sizeof the_struct.term_type) in
let ci = match the_struct.term_type with
| Ctype(TComp(ci, _, _) as t) when Cil.has_flexible_array_member t -> ci
- | _ -> assert false
+ | _ -> Options.fatal "Unfolding flexible on a non flexible structure"
in
let flex_type = Ctype (Extlib.last ci.cfields).ftype in
let flex_len = tminus bytes_len struct_len in
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index 96ab43c06e59c55f07d81a053663d33b760b9a0c..41679ef1d11045cfaef1aff637ec7b4f1de63409 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -25,12 +25,14 @@ open Basic_blocks
open Cil_types
open Extlib
+let unexpected = Options.fatal "Stdlib.Basic_alloc: unexpected: %s"
+
let valid_size ?loc typ size =
let p = match typ with
| TComp (ci, _, _) when Cil.has_flexible_array_member typ ->
let elem = match (last ci.cfields).ftype with
| TArray(t, _ , _, _) -> tinteger ?loc (Cil.bytesSizeOf t)
- | _ -> assert false
+ | _ -> unexpected "non array last field on flexible structure"
in
let base = tinteger ?loc (Cil.bytesSizeOf typ) in
let flex = tminus ?loc size base in
diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
index 1ea994392c6c840d0e183a6db74bf9d53e4f2fc3..86eada6103dfa765956508a1e25c231a346199d9 100644
--- a/src/plugins/instantiate/stdlib/calloc.ml
+++ b/src/plugins/instantiate/stdlib/calloc.ml
@@ -27,13 +27,15 @@ open Logic_const
let function_name = "calloc"
+let unexpected = Options.fatal "Stdlib.Calloc: unexpected: %s"
+
let pset_len_to_zero ?loc alloc_type num size =
let eq_simpl_value ?loc t =
- let value = match t.term_type with
+ 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
- | _ -> assert false
+ | _ -> unexpected "non atomic type during equality generation"
in
prel ?loc (Req, t, value)
in
@@ -62,9 +64,9 @@ let generate_requires ?loc alloc_type num size =
let pinitialized_len ?loc alloc_type num size =
let result = tresult ?loc (ptr_of alloc_type) in
let initialized ?loc t =
- let t = match t.term_node, t.term_type with
+ let t = match t.term_node, Logic_utils.unroll_type t.term_type with
| TLval (lv), Ctype t -> taddrof ?loc lv (Ctype (ptr_of t))
- | _ -> assert false
+ | _ -> unexpected "non lvalue or non c-type during initialized generation"
in
pinitialized ?loc (here_label, t)
in
@@ -108,7 +110,7 @@ let make_behavior_no_allocation loc alloc_type num size =
let generate_spec alloc_type { svar = vi } loc =
let (cnum, csize) = match Cil.getFormalsDecl vi with
| [ cnum ; csize ] -> cnum, csize
- | _ -> assert false
+ | _ -> unexpected "ill-formed fundec in specification generation"
in
let num = tlogic_coerce ~loc (cvar_to_tvar cnum) Linteger in
let size = tlogic_coerce ~loc (cvar_to_tvar csize) Linteger in
@@ -133,7 +135,8 @@ let well_typed_call ret args =
match ret, args with
| Some ret, [ _ ; _ ] ->
let t = Cil.typeOfLval ret in
- Cil.isPointerType t && not (Cil.isVoidPtrType t)
+ Cil.isPointerType t && not (Cil.isVoidPtrType t) &&
+ Cil.isCompleteType (Cil.typeOf_pointed t)
| _ -> false
let key_from_call ret _ =
@@ -142,7 +145,7 @@ let key_from_call 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 -> assert false
+ | None -> 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 7e00ccdb12e8bb6ab5160d40152dc5876e1ab94d..7ef4c509bb20f13e505b79ab71a2feabc99d5436 100644
--- a/src/plugins/instantiate/stdlib/free.ml
+++ b/src/plugins/instantiate/stdlib/free.ml
@@ -25,6 +25,8 @@ open Basic_alloc
open Cil_types
open Logic_const
+let unexpected = Options.fatal "Stdlib.Free: unexpected: %s"
+
let function_name = "free"
let null_pointer ?loc ptr =
@@ -63,7 +65,7 @@ let make_behavior_no_deallocation loc ptr =
let generate_spec _typ { svar = vi } loc =
let ptr = match Cil.getFormalsDecl vi with
| [ ptr ] -> cvar_to_tvar ptr
- | _ -> assert false
+ | _ -> unexpected "ill-formed fundec in specification generation"
in
let requires = generate_requires loc ptr in
let assigns = generate_global_assigns ptr in
@@ -95,7 +97,7 @@ let key_from_call _ret args =
let ptr_t = Cil.unrollTypeDeep (Cil.typeOf ptr) in
let ptr_t = Cil.type_remove_qualifier_attributes_deep ptr_t in
Cil.typeOf_pointed ptr_t
- | _ -> assert false
+ | _ -> unexpected "trying to generate a key on an ill-typed call"
let retype_args _typ args = List.map Cil.stripCasts args
let args_for_original _typ args = args
diff --git a/src/plugins/instantiate/stdlib/malloc.ml b/src/plugins/instantiate/stdlib/malloc.ml
index a6debf251e1080313e96210b5a0ecc0404fa29b9..16521b530aebe5561a445c1e30216d24b338feef 100644
--- a/src/plugins/instantiate/stdlib/malloc.ml
+++ b/src/plugins/instantiate/stdlib/malloc.ml
@@ -27,6 +27,8 @@ open Logic_const
let function_name = "malloc"
+let unexpected = Options.fatal "Stdlib.Malloc: unexpected: %s"
+
let generate_global_assigns loc ptr_type size =
let assigns_result = assigns_result ~loc ptr_type [ size ] in
let assigns_heap = assigns_heap [ size ] in
@@ -49,7 +51,7 @@ let make_behavior_no_allocation loc ptr_type size =
let generate_spec alloc_typ { svar = vi } loc =
let (csize) = match Cil.getFormalsDecl vi with
| [ size ] -> size
- | _ -> assert false
+ | _ -> unexpected "ill-formed fundec in specification generation"
in
let size = tlogic_coerce ~loc (cvar_to_tvar csize) Linteger in
let requires = [ valid_size ~loc alloc_typ size ] in
@@ -72,7 +74,8 @@ let well_typed_call ret args =
match ret, args with
| Some ret, [ _ ] ->
let t = Cil.typeOfLval ret in
- Cil.isPointerType t && not (Cil.isVoidPtrType t)
+ Cil.isPointerType t && not (Cil.isVoidPtrType t) &&
+ Cil.isCompleteType (Cil.typeOf_pointed t)
| _ -> false
let key_from_call ret _ =
@@ -81,7 +84,7 @@ let key_from_call 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 -> assert false
+ | None -> 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/memcmp.ml b/src/plugins/instantiate/string/memcmp.ml
index 813ab06065ffd8950c70eee109e2c9f264d69a64..633294db95b177f66c5f927cfc794f8e7dcc04c3 100644
--- a/src/plugins/instantiate/string/memcmp.ml
+++ b/src/plugins/instantiate/string/memcmp.ml
@@ -26,6 +26,8 @@ open Basic_blocks
let function_name = "memcmp"
+let unexpected = Options.fatal "String.Memcmp: unexpected: %s"
+
let generate_requires loc s1 s2 len =
List.map new_predicate [
{ (pcorrect_len_bytes ~loc s1.term_type len)
@@ -63,7 +65,7 @@ let generate_ensures loc s1 s2 len =
let generate_spec _t { svar = vi } loc =
let (c_s1, c_s2, clen) = match Cil.getFormalsDecl vi with
| [ s1 ; s2 ; len ] -> s1, s2, len
- | _ -> assert false
+ | _ -> unexpected "ill-formed fundec in specification generation"
in
let s1 = cvar_to_tvar c_s1 in
let s2 = cvar_to_tvar c_s2 in
@@ -97,12 +99,13 @@ 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)))
+ (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
- | _ -> failwith "Call to Memmove.key_from_call on an ill-typed call"
+ | _ -> unexpected "trying to generate a key on an ill-typed call"
let retype_args override_key = function
| [ s1 ; s2 ; len ] ->
@@ -113,7 +116,7 @@ let retype_args override_key = function
Cil_datatype.Typ.equal (type_from_arg s2) override_key
) ;
[ s1 ; s2 ; len ]
- | _ -> failwith "Call to Memmove.retype_args on an ill-typed call"
+ | _ -> unexpected "trying to retype arguments on an ill-typed call"
let args_for_original _t args = args
diff --git a/src/plugins/instantiate/string/memcpy.ml b/src/plugins/instantiate/string/memcpy.ml
index 6be6f6664ba02549639d9674ce51f19f7875e8a2..d0db608eef172febd0665fb56a38d9543131e16a 100644
--- a/src/plugins/instantiate/string/memcpy.ml
+++ b/src/plugins/instantiate/string/memcpy.ml
@@ -26,6 +26,8 @@ open Basic_blocks
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
@@ -67,7 +69,7 @@ let generate_ensures loc t dest src len =
let generate_spec _t { svar = vi } loc =
let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
| [ dest ; src ; len ] -> dest, src, len
- | _ -> assert false
+ | _ -> unexpected "ill-formed fundec in specification generation"
in
let t = cdest.vtype in
let dest = cvar_to_tvar cdest in
@@ -103,12 +105,13 @@ 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)))
+ (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
- | _ -> failwith "Call to Memcpy.key_from_call on an ill-typed call"
+ | _ -> unexpected "trying to generate a key on an ill-typed call"
let retype_args override_key = function
| [ dest ; src ; len ] ->
@@ -119,7 +122,7 @@ let retype_args override_key = function
Cil_datatype.Typ.equal (type_from_arg src) override_key
) ;
[ dest ; src ; len ]
- | _ -> failwith "Call to Memcpy.retype_args on an ill-typed call"
+ | _ -> unexpected "trying to retype arguments on an ill-typed call"
let args_for_original _t args = args
diff --git a/src/plugins/instantiate/string/memmove.ml b/src/plugins/instantiate/string/memmove.ml
index 97c3dcb1c577525df2f2caccc210a574cf54a81c..6481c423a1ff763ac83f433f801d5872b1d75876 100644
--- a/src/plugins/instantiate/string/memmove.ml
+++ b/src/plugins/instantiate/string/memmove.ml
@@ -26,6 +26,8 @@ open Basic_blocks
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)
@@ -61,7 +63,7 @@ let generate_ensures loc t dest src len =
let generate_spec _t { svar = vi } loc =
let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
| [ dest ; src ; len ] -> dest, src, len
- | _ -> assert false
+ | _ -> unexpected "ill-formed fundec in specification generation"
in
let t = cdest.vtype in
let dest = cvar_to_tvar cdest in
@@ -97,12 +99,13 @@ 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)))
+ (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
- | _ -> failwith "Call to Memmove.key_from_call on an ill-typed call"
+ | _ -> unexpected "trying to generate a key on an ill-typed call"
let retype_args override_key = function
| [ dest ; src ; len ] ->
@@ -113,7 +116,7 @@ let retype_args override_key = function
Cil_datatype.Typ.equal (type_from_arg src) override_key
) ;
[ dest ; src ; len ]
- | _ -> failwith "Call to Memmove.retype_args on an ill-typed call"
+ | _ -> unexpected "trying to retype arguments on an ill-typed call"
let args_for_original _t args = args
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index f1935a41528667bcf05f6313dd1e226bf04b5279..393f6ae626bc5595188e3a252395c8e845b391c6 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -27,6 +27,8 @@ open Basic_blocks
let function_name = "memset"
type key = (typ * int option)
+let unexpected = Options.fatal "String.Memset: unexpected: %s"
+
module With_collection = struct
module OptIntInfo = struct
let module_name = String.capitalize_ascii "Instantiate.Memset.OptInt.Datatype"
@@ -63,11 +65,11 @@ let pset_len_bytes_to_value ?loc ptr value bytes_len =
let pset_len_bytes_to_zero ?loc ptr bytes_len =
let eq_value ?loc t =
- let value = match t.term_type with
+ 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
- | _ -> assert false
+ | _ -> unexpected "non atomic type during equality generation"
in
prel ?loc (Req, t, value)
in
@@ -82,7 +84,7 @@ let pset_len_bytes_all_bits_to_one ?loc ptr bytes_len =
in
let find_nan_for_type t = List.find (of_type t) nans in
let all_bits_to_one ?loc t =
- match t.term_type with
+ match Logic_utils.unroll_type t.term_type with
| Ctype(TFloat(_)) ->
papp ?loc ((find_nan_for_type t.term_type), [], [t])
| Ctype(TPtr(_)) ->
@@ -97,7 +99,8 @@ let pset_len_bytes_all_bits_to_one ?loc ptr bytes_len =
in
let value = term ?loc (TConst (Integer (value,None))) Linteger in
prel ?loc (Req, t, value)
- | _ -> assert false
+ | _ ->
+ unexpected "non atomic type during equality generation"
in
plet_len_div_size ?loc ptr.term_type bytes_len
(fun len -> punfold_all_elems_pred ?loc ptr len all_bits_to_one)
@@ -110,7 +113,7 @@ let generate_requires loc ptr value len =
[ { (pcorrect_len_bytes ~loc ptr.term_type len)
with pred_name = ["aligned_end"] } ]
| Some value ->
- let low, up = match value.term_type with
+ let low, up = match Logic_utils.unroll_type value.term_type with
| Ctype(TInt((IChar|ISChar|IUChar) as kind, _)) ->
let bits = bitsSizeOfInt kind in
let plus_one = Integer.add (Integer.of_int 1) in
@@ -121,7 +124,8 @@ let generate_requires loc ptr value len =
in
let integer ?loc i = term ?loc (TConst (Integer (i, None))) Linteger in
(integer ~loc low), (integer ~loc up)
- | _ -> assert false
+ | _ ->
+ unexpected "non atomic type during value bounds generation"
in
[ { (pbounds_incl_excl ~loc low value up)
with pred_name = [ "in_bounds_value" ] } ]
@@ -149,7 +153,8 @@ let generate_ensures e loc t ptr value len =
[ { (pset_len_bytes_to_zero ~loc ptr len) with pred_name } ]
| Some 255, None ->
[ { (pset_len_bytes_all_bits_to_one ~loc ptr len) with pred_name }]
- | _ -> assert false
+ | _ ->
+ unexpected "ill-formed key in ensure generation"
in
List.map (fun p -> Normal, new_predicate p) (content @ [
{ (presult_ptr ~loc t ptr) with pred_name = [ "result"] }
@@ -159,7 +164,7 @@ let generate_spec (_t, e) { svar = vi } loc =
let (cptr, cvalue, clen) = match Cil.getFormalsDecl vi with
| [ ptr ; value ; len ] -> ptr, (Some value), len
| [ ptr ; len ] -> ptr, None, len
- | _ -> assert false
+ | _ -> unexpected "ill-formed fundec in specification generation"
in
let t = cptr.vtype in
let ptr = cvar_to_tvar cptr in
@@ -183,14 +188,21 @@ let memset_value e =
| Const(CInt64(ni, _, _)) when Integer.equal ni ff -> Some 255
| _ -> None
-let is_union_type = function
- | TComp({ cstruct = false }, _, _) -> true
+let rec contains_union_type t =
+ match Cil.unrollType t with
+ | TComp({ cstruct = false }, _, _) ->
+ true
+ | TComp({ cfields = fields }, _, _) ->
+ List.exists contains_union_type (List.map (fun f -> f.ftype) fields)
+ | TArray(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 is_union_type (type_from_arg ptr) -> false
+ | [ 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
@@ -201,9 +213,9 @@ let well_typed_call _ret = function
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 (is_union_type (type_from_arg ptr)) ->
+ | [ ptr ; value ; _ ] when not (contains_union_type (type_from_arg ptr)) ->
(type_from_arg ptr), (memset_value value)
- | _ -> failwith "Call to Memset.key_from_call on an ill-typed call"
+ | _ -> unexpected "trying to generate a key on an ill-typed call"
let char_prototype t =
assert (any_char_composed_type t) ;
@@ -226,13 +238,13 @@ let generate_prototype = function
let name = function_name ^ "_" ^ (string_of_typ t) in
let fun_type = char_prototype t in
name, fun_type
- | t, Some x when not (is_union_type t) && (x = 0 || x = 255) ->
+ | t, Some x when not (contains_union_type t) && (x = 0 || x = 255) ->
let ext = if x = 0 then "_0" else if x = 255 then "_FF" else assert false in
let name = function_name ^ "_" ^ (string_of_typ t) ^ ext in
let fun_type = non_char_prototype t in
name, fun_type
| _, _ ->
- failwith "Call to Memset.generate_prototype on an ill-typed call"
+ unexpected "trying to generate a prototype on an ill-typed call"
let retype_args (t, e) args =
match e, args with
@@ -248,7 +260,7 @@ let retype_args (t, e) args =
assert (match memset_value v with Some x when x = fv -> true | _ -> false) ;
[ ptr ; n ]
| _ ->
- failwith "Call to Memset.retype_args on an ill-typed call"
+ unexpected "trying to retype arguments on an ill-typed call"
let args_for_original (_t , e) args =
match e with
@@ -257,7 +269,8 @@ let args_for_original (_t , e) args =
let loc = Cil_datatype.Location.unknown in
match args with
| [ ptr ; len ] -> [ ptr ; (Cil.integer ~loc n) ; len]
- | _ -> assert false
+ | _ ->
+ unexpected "wrong number of arguments replacing call"
let () = Transform.register (module struct
module Hashtbl = With_collection.Hashtbl
diff --git a/src/plugins/instantiate/tests/plugin/function_pointers.i b/src/plugins/instantiate/tests/plugin/function_pointers.i
new file mode 100644
index 0000000000000000000000000000000000000000..8f27dd1ab187cf20f3fd5572383a80d7e5be4dd9
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/function_pointers.i
@@ -0,0 +1,6 @@
+/* run.config
+ OPT: -instantiate
+*/
+void foo(void (* bar)()){
+ (*bar)();
+}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/plugin/oracle/function_pointers.res.oracle b/src/plugins/instantiate/tests/plugin/oracle/function_pointers.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bcf3d3f77fabccbae301b3acbca35d6ddb1a4eeb
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/oracle/function_pointers.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/plugin/function_pointers.i (no preprocessing)
diff --git a/src/plugins/instantiate/tests/stdlib/calloc.c b/src/plugins/instantiate/tests/stdlib/calloc.c
index 77be4d292f1d7befca278b4210ea6335c805fed1..87b1f9338ccb5ecdd99d339551a383459f8305bc 100644
--- a/src/plugins/instantiate/tests/stdlib/calloc.c
+++ b/src/plugins/instantiate/tests/stdlib/calloc.c
@@ -19,4 +19,5 @@ int main(void){
int (*pa) [10] = calloc(10, sizeof(int[10])) ;
struct Flex* f = calloc(1, sizeof(struct Flex) + 3 * sizeof(int)) ;
void *v = calloc(10, sizeof(char));
+ struct incomplete* inc = calloc(10, 10);
}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/stdlib/free.c b/src/plugins/instantiate/tests/stdlib/free.c
index 40cab4f547cfcf9ab66b7e278c3a0cce9ddd6c00..e61ed8864c1d2657e6dc1f65a0d047735b3a2d6b 100644
--- a/src/plugins/instantiate/tests/stdlib/free.c
+++ b/src/plugins/instantiate/tests/stdlib/free.c
@@ -11,4 +11,7 @@ void baz(int (*x) [10]){
}
void with_void(void * x){
free(x);
+}
+void with_incomplete(struct incomplete* t){
+ free(t);
}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/stdlib/malloc.c b/src/plugins/instantiate/tests/stdlib/malloc.c
index 0d5aa4ea04a70e739cf3a4b5e5125baf2b2b1197..00a07820a9ac4377c39826e16538d62e6f8c2322 100644
--- a/src/plugins/instantiate/tests/stdlib/malloc.c
+++ b/src/plugins/instantiate/tests/stdlib/malloc.c
@@ -11,6 +11,8 @@ struct Flex {
int f[] ;
} ;
+struct incomplete ;
+
int main(void){
int* pi = malloc(sizeof(int) * 10) ;
float* pf = malloc(sizeof(float) * 10) ;
@@ -19,4 +21,5 @@ int main(void){
int (*pa) [10] = malloc(sizeof(int[10]) * 10) ;
struct Flex* f = malloc(sizeof(struct Flex) + 3 * sizeof(int)) ;
void *v = malloc(sizeof(char) * 10);
+ struct incomplete* inc = malloc(10);
}
\ 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 5fb370ab29a192623a74034cbf0923e31191b163..28d42c036e394314e15f148be188d770b46886e9 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -1,5 +1,6 @@
[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
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -11,6 +12,7 @@ struct Flex {
char c ;
int f[] ;
};
+struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
requires only_one: num ≡ 1;
assigns \result, __fc_heap_status;
@@ -263,15 +265,13 @@ int main(void)
calloc_st_Flex((unsigned int)1,
sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = calloc((unsigned int)10,sizeof(char));
+ struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
__retres = 0;
return __retres;
}
[kernel] Parsing tests/stdlib/result/calloc.c (with preprocessing)
-[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
-[kernel] tests/stdlib/calloc.c:14: Warning:
- def'n of func main at tests/stdlib/calloc.c:14 (sum 6403) conflicts with the one at tests/stdlib/result/calloc.c:252 (sum 8177); keeping the one at tests/stdlib/result/calloc.c:252.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -283,6 +283,7 @@ struct Flex {
char c ;
int f[] ;
};
+struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
requires only_one: num ≡ 1;
assigns \result, __fc_heap_status;
@@ -539,6 +540,7 @@ int main(void)
calloc_st_Flex((unsigned int)1,
sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = calloc((unsigned int)10,sizeof(char));
+ struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
index 1e764fcd7c62f75f1a4160cd430d760db327f29a..cfdb769ed8d5e5412d854f0a741ba18d912fcfaf 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
@@ -2,6 +2,7 @@
[instantiate] tests/stdlib/free.c:13: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
+struct incomplete;
/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status, ptr;
@@ -104,19 +105,43 @@ void with_void(void *x)
return;
}
+/*@ 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_st_incomplete(struct incomplete *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+void with_incomplete(struct incomplete *t)
+{
+ free_st_incomplete(t);
+ return;
+}
+
[kernel] Parsing tests/stdlib/result/free.c (with preprocessing)
-[kernel] Parsing tests/stdlib/free.c (with preprocessing)
-[kernel] tests/stdlib/free.c:3: Warning:
- dropping duplicate def'n of func foo at tests/stdlib/free.c:3 in favor of that at tests/stdlib/result/free.c:29
-[kernel] tests/stdlib/free.c:6: Warning:
- dropping duplicate def'n of func bar at tests/stdlib/free.c:6 in favor of that at tests/stdlib/result/free.c:61
-[kernel] tests/stdlib/free.c:9: Warning:
- dropping duplicate def'n of func baz at tests/stdlib/free.c:9 in favor of that at tests/stdlib/result/free.c:93
-[kernel] tests/stdlib/free.c:12: Warning:
- dropping duplicate def'n of func with_void at tests/stdlib/free.c:12 in favor of that at tests/stdlib/result/free.c:99
/* Generated by Frama-C */
#include "stdlib.h"
+struct incomplete;
/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status, ptr;
@@ -219,4 +244,36 @@ void with_void(void *x)
return;
}
+/*@ 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_st_incomplete(struct incomplete *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+void with_incomplete(struct incomplete *t)
+{
+ free_st_incomplete(t);
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index feb0c41909dd4a6cb6b7de4c4ec3dac49cd07869..6cec0abadff6e4e4fd12bfb6d6629c04e09816a6 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[instantiate] tests/stdlib/malloc.c:21: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:23: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:24: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -11,6 +12,7 @@ struct Flex {
char c ;
int f[] ;
};
+struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
assigns \result, __fc_heap_status;
assigns \result \from __fc_heap_status, size;
@@ -208,15 +210,13 @@ int main(void)
struct Flex *f =
malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = malloc(sizeof(char) * (unsigned int)10);
+ struct incomplete *inc = malloc((unsigned int)10);
__retres = 0;
return __retres;
}
[kernel] Parsing tests/stdlib/result/malloc.c (with preprocessing)
-[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[kernel] tests/stdlib/malloc.c:14: Warning:
- def'n of func main at tests/stdlib/malloc.c:14 (sum 6403) conflicts with the one at tests/stdlib/result/malloc.c:198 (sum 8177); keeping the one at tests/stdlib/result/malloc.c:198.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -228,6 +228,7 @@ struct Flex {
char c ;
int f[] ;
};
+struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
assigns \result, __fc_heap_status;
assigns \result \from __fc_heap_status, size;
@@ -425,6 +426,7 @@ int main(void)
struct Flex *f =
malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = malloc(sizeof(char) * (unsigned int)10);
+ struct incomplete *inc = malloc((unsigned int)10);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/instantiate/tests/stdlib/test_config b/src/plugins/instantiate/tests/stdlib/test_config
index dba5b7b5f4a3904ab10ba039dce5bee0734e2101..cc295b086555e3e3854cbe0f8013b3f96f464c7d 100644
--- a/src/plugins/instantiate/tests/stdlib/test_config
+++ b/src/plugins/instantiate/tests/stdlib/test_config
@@ -1 +1 @@
-OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file
+OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c -ocode="" -print
diff --git a/src/plugins/instantiate/tests/string/memcmp.c b/src/plugins/instantiate/tests/string/memcmp.c
index 004f004f222223440c8a3221832d494ecd8541ce..404692f9eb118b24ffa7716dceb72b990d973d2e 100644
--- a/src/plugins/instantiate/tests/string/memcmp.c
+++ b/src/plugins/instantiate/tests/string/memcmp.c
@@ -29,4 +29,9 @@ int nested(int (*s1)[10], int (*s2)[10], int n){
int with_void(void *s1, void *s2, int n){
return memcmp(s1, s2, 10) ;
+}
+
+struct incomplete ;
+int with_incomplete(struct incomplete* s1, struct incomplete* s2, int n){
+ return memcmp(s1, s2, n);
}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/string/memcpy.c b/src/plugins/instantiate/tests/string/memcpy.c
index 4f245bbbd068b03d854f4dbf7571693be07af82f..f2c6c03d864470e963082de31044b103dde3a930 100644
--- a/src/plugins/instantiate/tests/string/memcpy.c
+++ b/src/plugins/instantiate/tests/string/memcpy.c
@@ -36,3 +36,9 @@ void with_void(void *src, void *dest, int n){
void *res = memcpy(dest, src, n);
memcpy(src, res, n);
}
+
+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
diff --git a/src/plugins/instantiate/tests/string/memmove.c b/src/plugins/instantiate/tests/string/memmove.c
index 9fca890b0e18cd35a23f399ee9bf2d86262e6e65..a40698297fd597433f1ced51585f2c1176b285f7 100644
--- a/src/plugins/instantiate/tests/string/memmove.c
+++ b/src/plugins/instantiate/tests/string/memmove.c
@@ -36,3 +36,9 @@ void with_void(void *src, void *dest, int n){
void *res = memmove(dest, src, n);
memmove(src, res, n);
}
+
+struct incomplete ;
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n){
+ struct incomplete *res = memmove(dest, src, n);
+ memmove(src, res, n);
+}
diff --git a/src/plugins/instantiate/tests/string/memset_nested_typedef.c b/src/plugins/instantiate/tests/string/memset_nested_typedef.c
new file mode 100644
index 0000000000000000000000000000000000000000..2e01be12e5c6560ef86b35bbcd997ead76b61e00
--- /dev/null
+++ b/src/plugins/instantiate/tests/string/memset_nested_typedef.c
@@ -0,0 +1,9 @@
+#include <string.h>
+
+typedef unsigned t;
+struct X { t s_addr; };
+
+void test() {
+ struct X x;
+ memset(&x, 0, sizeof(x));
+}
diff --git a/src/plugins/instantiate/tests/string/memset_nested_union.c b/src/plugins/instantiate/tests/string/memset_nested_union.c
new file mode 100644
index 0000000000000000000000000000000000000000..ea236b94e159c2eeb62dc5bad8fc822c6b6c28d2
--- /dev/null
+++ b/src/plugins/instantiate/tests/string/memset_nested_union.c
@@ -0,0 +1,11 @@
+#include <string.h>
+
+union U {
+ int x ;
+ unsigned y ;
+};
+struct X { union U u ; };
+void test() {
+ struct X x;
+ memset(&x, 0, sizeof(x));
+}
diff --git a/src/plugins/instantiate/tests/string/memset_value.c b/src/plugins/instantiate/tests/string/memset_value.c
index 25f04a59ff02c4378a30f44a82d1ffa81758f895..432b8ed6a6d3aa03bbb2d99e449641a6e4ac7d1c 100644
--- a/src/plugins/instantiate/tests/string/memset_value.c
+++ b/src/plugins/instantiate/tests/string/memset_value.c
@@ -51,3 +51,8 @@ void with_void(void* dest, int value){
void* res = memset(dest, value, 10);
memset(res, value, 10);
}
+
+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
diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index 9a3d0e6381121a41265d270e492b2b5ffca83dc7..18ada799c0a1e0f5e274988851be469c4bc793bc 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -1,5 +1,6 @@
[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
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -9,6 +10,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
@@ -150,21 +152,15 @@ int with_void(void *s1, void *s2, int n)
return tmp;
}
+int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
+{
+ int tmp;
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
+ return tmp;
+}
+
[kernel] Parsing tests/string/result/memcmp.c (with preprocessing)
-[kernel] Parsing tests/string/memcmp.c (with preprocessing)
-[kernel] tests/string/memcmp.c:10: Warning:
- def'n of func integer at tests/string/memcmp.c:10 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:34 (sum 1972); keeping the one at tests/string/result/memcmp.c:34.
-[kernel] tests/string/memcmp.c:14: Warning:
- def'n of func with_named at tests/string/memcmp.c:14 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:41 (sum 1972); keeping the one at tests/string/result/memcmp.c:41.
-[kernel] tests/string/memcmp.c:18: Warning:
- def'n of func structure at tests/string/memcmp.c:18 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:72 (sum 1972); keeping the one at tests/string/result/memcmp.c:72.
-[kernel] tests/string/memcmp.c:22: Warning:
- def'n of func pointers at tests/string/memcmp.c:22 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:103 (sum 1972); keeping the one at tests/string/result/memcmp.c:103.
-[kernel] tests/string/memcmp.c:26: Warning:
- def'n of func nested at tests/string/memcmp.c:26 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:137 (sum 1974); keeping the one at tests/string/result/memcmp.c:137.
-[kernel] tests/string/memcmp.c:30: Warning:
- def'n of func with_void at tests/string/memcmp.c:30 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:144 (sum 1974); keeping the one at tests/string/result/memcmp.c:144.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -174,6 +170,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
@@ -324,4 +321,11 @@ int with_void(void *s1, void *s2, int n)
return tmp;
}
+int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
+{
+ int tmp;
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
+ return tmp;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 63bd23cf23c207e89a094717492cd87246acb3c0..05681aeb44ef741834b203dad7dc77150b910d34 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -1,6 +1,8 @@
[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
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -10,6 +12,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -162,21 +165,16 @@ void with_void(void *src, void *dest, int n)
return;
}
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
+{
+ struct incomplete *res =
+ memcpy((void *)dest,(void const *)src,(unsigned int)n);
+ memcpy((void *)src,(void const *)res,(unsigned int)n);
+ return;
+}
+
[kernel] Parsing tests/string/result/memcpy.c (with preprocessing)
-[kernel] Parsing tests/string/memcpy.c (with preprocessing)
-[kernel] tests/string/memcpy.c:10: Warning:
- dropping duplicate def'n of func integer at tests/string/memcpy.c:10 in favor of that at tests/string/result/memcpy.c:36
-[kernel] tests/string/memcpy.c:15: Warning:
- dropping duplicate def'n of func with_named at tests/string/memcpy.c:15 in favor of that at tests/string/result/memcpy.c:43
-[kernel] tests/string/memcpy.c:20: Warning:
- dropping duplicate def'n of func structure at tests/string/memcpy.c:20 in favor of that at tests/string/result/memcpy.c:76
-[kernel] tests/string/memcpy.c:25: Warning:
- dropping duplicate def'n of func pointers at tests/string/memcpy.c:25 in favor of that at tests/string/result/memcpy.c:109
-[kernel] tests/string/memcpy.c:30: Warning:
- dropping duplicate def'n of func nested at tests/string/memcpy.c:30 in favor of that at tests/string/result/memcpy.c:147
-[kernel] tests/string/memcpy.c:35: Warning:
- dropping duplicate def'n of func with_void at tests/string/memcpy.c:35 in favor of that at tests/string/result/memcpy.c:155
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -186,6 +184,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -349,4 +348,12 @@ void with_void(void *src, void *dest, int n)
return;
}
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
+{
+ struct incomplete *res =
+ memcpy((void *)dest,(void const *)src,(unsigned int)n);
+ memcpy((void *)src,(void const *)res,(unsigned int)n);
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index 6023a30c6bf1db32b311e1cc205aa6780273e26c..15c80507c4a17b1b2c366d5ce5cccfacb4008a46 100644
--- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
@@ -1,6 +1,8 @@
[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
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -10,6 +12,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -146,21 +149,16 @@ void with_void(void *src, void *dest, int n)
return;
}
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
+{
+ struct incomplete *res =
+ memmove((void *)dest,(void const *)src,(unsigned int)n);
+ memmove((void *)src,(void const *)res,(unsigned int)n);
+ return;
+}
+
[kernel] Parsing tests/string/result/memmove.c (with preprocessing)
-[kernel] Parsing tests/string/memmove.c (with preprocessing)
-[kernel] tests/string/memmove.c:10: Warning:
- dropping duplicate def'n of func integer at tests/string/memmove.c:10 in favor of that at tests/string/result/memmove.c:32
-[kernel] tests/string/memmove.c:15: Warning:
- dropping duplicate def'n of func with_named at tests/string/memmove.c:15 in favor of that at tests/string/result/memmove.c:39
-[kernel] tests/string/memmove.c:20: Warning:
- dropping duplicate def'n of func structure at tests/string/memmove.c:20 in favor of that at tests/string/result/memmove.c:68
-[kernel] tests/string/memmove.c:25: Warning:
- dropping duplicate def'n of func pointers at tests/string/memmove.c:25 in favor of that at tests/string/result/memmove.c:97
-[kernel] tests/string/memmove.c:30: Warning:
- dropping duplicate def'n of func nested at tests/string/memmove.c:30 in favor of that at tests/string/result/memmove.c:131
-[kernel] tests/string/memmove.c:35: Warning:
- dropping duplicate def'n of func with_void at tests/string/memmove.c:35 in favor of that at tests/string/result/memmove.c:139
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -170,6 +168,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -317,4 +316,12 @@ void with_void(void *src, void *dest, int n)
return;
}
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
+{
+ struct incomplete *res =
+ memmove((void *)dest,(void const *)src,(unsigned int)n);
+ memmove((void *)src,(void const *)res,(unsigned int)n);
+ 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 8936d80df52ddcdaf70d3aa9dcf6f9a2c97edf53..1b7efe66ddfaf3924b521e046ee4ebff7779483e 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -235,27 +235,6 @@ void with_void(void *dest)
[kernel] Parsing tests/string/result/memset_0.c (with preprocessing)
-[kernel] Parsing tests/string/memset_0.c (with preprocessing)
-[kernel] tests/string/memset_0.c:10: Warning:
- dropping duplicate def'n of func chars at tests/string/memset_0.c:10 in favor of that at tests/string/result/memset_0.c:26
-[kernel] tests/string/memset_0.c:15: Warning:
- dropping duplicate def'n of func uchars at tests/string/memset_0.c:15 in favor of that at tests/string/result/memset_0.c:50
-[kernel] tests/string/memset_0.c:20: Warning:
- dropping duplicate def'n of func nested_chars at tests/string/memset_0.c:20 in favor of that at tests/string/result/memset_0.c:78
-[kernel] tests/string/memset_0.c:25: Warning:
- dropping duplicate def'n of func integer at tests/string/memset_0.c:25 in favor of that at tests/string/result/memset_0.c:104
-[kernel] tests/string/memset_0.c:30: Warning:
- dropping duplicate def'n of func floats at tests/string/memset_0.c:30 in favor of that at tests/string/result/memset_0.c:130
-[kernel] tests/string/memset_0.c:35: Warning:
- dropping duplicate def'n of func with_named at tests/string/memset_0.c:35 in favor of that at tests/string/result/memset_0.c:137
-[kernel] tests/string/memset_0.c:40: Warning:
- dropping duplicate def'n of func structure at tests/string/memset_0.c:40 in favor of that at tests/string/result/memset_0.c:164
-[kernel] tests/string/memset_0.c:45: Warning:
- dropping duplicate def'n of func pointers at tests/string/memset_0.c:45 in favor of that at tests/string/result/memset_0.c:190
-[kernel] tests/string/memset_0.c:50: Warning:
- dropping duplicate def'n of func nested at tests/string/memset_0.c:50 in favor of that at tests/string/result/memset_0.c:218
-[kernel] tests/string/memset_0.c:55: Warning:
- dropping duplicate def'n of func with_void at tests/string/memset_0.c:55 in favor of that at tests/string/result/memset_0.c:226
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
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 c64a99baf967de3fff4386486b4b06d1687f0959..ffe160d7caa31fe89b889cdcc11c09f58f3192ab 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -373,37 +373,6 @@ void with_void(void *dest)
[kernel] Parsing tests/string/result/memset_FF.c (with preprocessing)
-[kernel] Parsing tests/string/memset_FF.c (with preprocessing)
-[kernel] tests/string/memset_FF.c:10: Warning:
- dropping duplicate def'n of func chars at tests/string/memset_FF.c:10 in favor of that at tests/string/result/memset_FF.c:26
-[kernel] tests/string/memset_FF.c:15: Warning:
- dropping duplicate def'n of func uchars at tests/string/memset_FF.c:15 in favor of that at tests/string/result/memset_FF.c:50
-[kernel] tests/string/memset_FF.c:20: Warning:
- dropping duplicate def'n of func nested_chars at tests/string/memset_FF.c:20 in favor of that at tests/string/result/memset_FF.c:79
-[kernel] tests/string/memset_FF.c:25: Warning:
- dropping duplicate def'n of func integer at tests/string/memset_FF.c:25 in favor of that at tests/string/result/memset_FF.c:105
-[kernel] tests/string/memset_FF.c:30: Warning:
- dropping duplicate def'n of func unsigned_integer at tests/string/memset_FF.c:30 in favor of that at tests/string/result/memset_FF.c:131
-[kernel] tests/string/memset_FF.c:35: Warning:
- dropping duplicate def'n of func long_integer at tests/string/memset_FF.c:35 in favor of that at tests/string/result/memset_FF.c:158
-[kernel] tests/string/memset_FF.c:40: Warning:
- dropping duplicate def'n of func unsigned_long_integer at tests/string/memset_FF.c:40 in favor of that at tests/string/result/memset_FF.c:184
-[kernel] tests/string/memset_FF.c:45: Warning:
- dropping duplicate def'n of func long_long_integer at tests/string/memset_FF.c:45 in favor of that at tests/string/result/memset_FF.c:212
-[kernel] tests/string/memset_FF.c:50: Warning:
- dropping duplicate def'n of func unsigned_long_long_integer at tests/string/memset_FF.c:50 in favor of that at tests/string/result/memset_FF.c:240
-[kernel] tests/string/memset_FF.c:56: Warning:
- dropping duplicate def'n of func floats at tests/string/memset_FF.c:56 in favor of that at tests/string/result/memset_FF.c:267
-[kernel] tests/string/memset_FF.c:61: Warning:
- dropping duplicate def'n of func with_named at tests/string/memset_FF.c:61 in favor of that at tests/string/result/memset_FF.c:274
-[kernel] tests/string/memset_FF.c:66: Warning:
- dropping duplicate def'n of func structure at tests/string/memset_FF.c:66 in favor of that at tests/string/result/memset_FF.c:302
-[kernel] tests/string/memset_FF.c:71: Warning:
- dropping duplicate def'n of func pointers at tests/string/memset_FF.c:71 in favor of that at tests/string/result/memset_FF.c:328
-[kernel] tests/string/memset_FF.c:76: Warning:
- dropping duplicate def'n of func nested at tests/string/memset_FF.c:76 in favor of that at tests/string/result/memset_FF.c:356
-[kernel] tests/string/memset_FF.c:81: Warning:
- dropping duplicate def'n of func with_void at tests/string/memset_FF.c:81 in favor of that at tests/string/result/memset_FF.c:364
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c99bbab555ac56acc73b2c2e68315465b5fcd36d
--- /dev/null
+++ b/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle
@@ -0,0 +1,72 @@
+[kernel] Parsing tests/string/memset_nested_typedef.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
+typedef unsigned int t;
+struct X {
+ t s_addr ;
+};
+/*@ 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)->s_addr ≡ 0;
+ ensures result: \result ≡ ptr;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns \result \from ptr;
+ */
+struct X *memset_st_X_0(struct X *ptr, size_t len)
+{
+ struct X *__retres;
+ __retres = (struct X *)memset((void *)ptr,0,len);
+ return __retres;
+}
+
+void test(void)
+{
+ struct X x;
+ memset_st_X_0(& x,sizeof(x));
+ return;
+}
+
+
+[kernel] Parsing tests/string/result/memset_nested_typedef.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
+typedef unsigned int t;
+struct X {
+ t s_addr ;
+};
+/*@ 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)->s_addr ≡ 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;
+ */
+struct X *memset_st_X_0(struct X *ptr, size_t len)
+{
+ struct X *__retres;
+ __retres = (struct X *)memset((void *)ptr,0,len);
+ return __retres;
+}
+
+void test(void)
+{
+ struct X x;
+ memset_st_X_0(& x,sizeof(x));
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..f71268da3aab3046b86c67795177069ebc7de2f2
--- /dev/null
+++ b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
@@ -0,0 +1,42 @@
+[kernel] Parsing tests/string/memset_nested_union.c (with preprocessing)
+[instantiate] tests/string/memset_nested_union.c:10: Warning:
+ Ignore call: not well typed
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
+union U {
+ int x ;
+ unsigned int y ;
+};
+struct X {
+ union U u ;
+};
+void test(void)
+{
+ struct X x;
+ memset((void *)(& x),0,sizeof(x));
+ return;
+}
+
+
+[kernel] Parsing tests/string/result/memset_nested_union.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
+union U {
+ int x ;
+ unsigned int y ;
+};
+struct X {
+ union U u ;
+};
+void test(void)
+{
+ struct X x;
+ memset((void *)(& x),0,sizeof(x));
+ return;
+}
+
+
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 26ed27864cc376fc2578df1e457c44cec81850ec..462fc372857d8a254614e0759e958ffd2d99b85d 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -23,6 +23,10 @@
Ignore call: not well typed
[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
+[instantiate] tests/string/memset_value.c:57: Warning:
+ Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -32,6 +36,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -151,27 +156,15 @@ void with_void(void *dest, int value)
return;
}
+void with_incomplete(struct incomplete *dest, int value)
+{
+ struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
+ memset((void *)res,value,(unsigned int)10);
+ return;
+}
+
[kernel] Parsing tests/string/result/memset_value.c (with preprocessing)
-[kernel] Parsing tests/string/memset_value.c (with preprocessing)
-[kernel] tests/string/memset_value.c:10: Warning:
- dropping duplicate def'n of func chars at tests/string/memset_value.c:10 in favor of that at tests/string/result/memset_value.c:26
-[kernel] tests/string/memset_value.c:15: Warning:
- dropping duplicate def'n of func uchars at tests/string/memset_value.c:15 in favor of that at tests/string/result/memset_value.c:50
-[kernel] tests/string/memset_value.c:20: Warning:
- dropping duplicate def'n of func nested_chars at tests/string/memset_value.c:20 in favor of that at tests/string/result/memset_value.c:78
-[kernel] tests/string/memset_value.c:25: Warning:
- dropping duplicate def'n of func integer at tests/string/memset_value.c:25 in favor of that at tests/string/result/memset_value.c:85
-[kernel] tests/string/memset_value.c:30: Warning:
- dropping duplicate def'n of func with_named at tests/string/memset_value.c:30 in favor of that at tests/string/result/memset_value.c:92
-[kernel] tests/string/memset_value.c:35: Warning:
- dropping duplicate def'n of func structure at tests/string/memset_value.c:35 in favor of that at tests/string/result/memset_value.c:99
-[kernel] tests/string/memset_value.c:40: Warning:
- dropping duplicate def'n of func pointers at tests/string/memset_value.c:40 in favor of that at tests/string/result/memset_value.c:107
-[kernel] tests/string/memset_value.c:45: Warning:
- dropping duplicate def'n of func nested at tests/string/memset_value.c:45 in favor of that at tests/string/result/memset_value.c:114
-[kernel] tests/string/memset_value.c:50: Warning:
- dropping duplicate def'n of func with_void at tests/string/memset_value.c:50 in favor of that at tests/string/result/memset_value.c:122
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -181,6 +174,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -305,4 +299,11 @@ void with_void(void *dest, int value)
return;
}
+void with_incomplete(struct incomplete *dest, int value)
+{
+ struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
+ memset((void *)res,value,(unsigned int)10);
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/string/test_config b/src/plugins/instantiate/tests/string/test_config
index dba5b7b5f4a3904ab10ba039dce5bee0734e2101..0bfb957513347953e1c1eb05f79e0722c5fcaa2f 100644
--- a/src/plugins/instantiate/tests/string/test_config
+++ b/src/plugins/instantiate/tests/string/test_config
@@ -1 +1 @@
-OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file
+OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c -ocode="" -print
\ No newline at end of file
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 6324749d9de154de754e55cfb735f76934c1f267..28f7a1ca81145cb2e7b414d21a0218b59ec6905f 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -104,7 +104,8 @@ class transformer = object(self)
| Not_found -> (fct, args)
method! vinst = function
- | Call(_) | Local_init(_, ConsInit(_, _, Plain_func), _) ->
+ | Call(_, { enode = Lval((Var _), NoOffset)} , _, _)
+ | Local_init(_, ConsInit(_ , _, Plain_func), _) ->
let change = function
| [ Call(r, ({ enode = Lval((Var f), NoOffset) } as e), args, loc) ] ->
let f, args = self#replace_call (r, f, args) in
@@ -125,6 +126,7 @@ let compute_call_preconditions_statuses kf =
let stmt = Kernel_function.find_first_stmt kf in
let _ = Kernel_function.find_all_enclosing_blocks stmt in
match stmt.skind with
+ | Instr (Local_init(_, ConsInit(fct, _, Plain_func), _))
| Instr (Call(_, { enode = Lval ((Var fct), NoOffset) }, _, _)) ->
let called_kf = Globals.Functions.get fct in
Statuses_by_call.setup_all_preconditions_proxies called_kf ;
@@ -132,7 +134,8 @@ let compute_call_preconditions_statuses kf =
~warn_missing:true called_kf stmt
in
List.iter (fun (_, p) -> validate_property p) reqs ;
- | _ -> assert false
+ | _ ->
+ Options.fatal "Transformation: unexpected instruction kind on precondition"
let compute_postconditions_statuses kf =
let posts bhv =