From 8dda36f2b740176af3aab24dbe5343a512fec728 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 26 Mar 2020 09:41:28 +0100
Subject: [PATCH] [Instantiate] Better failure messages
---
src/plugins/instantiate/Makefile.in | 2 +-
src/plugins/instantiate/basic_blocks.ml | 36 +++++++++----------
src/plugins/instantiate/stdlib/basic_alloc.ml | 4 ++-
src/plugins/instantiate/stdlib/calloc.ml | 14 ++++----
src/plugins/instantiate/stdlib/free.ml | 6 ++--
src/plugins/instantiate/stdlib/malloc.ml | 6 ++--
src/plugins/instantiate/string/memcmp.ml | 8 +++--
src/plugins/instantiate/string/memcpy.ml | 8 +++--
src/plugins/instantiate/string/memmove.ml | 8 +++--
src/plugins/instantiate/string/memset.ml | 28 +++++++++------
src/plugins/instantiate/transform.ml | 4 ++-
11 files changed, 73 insertions(+), 51 deletions(-)
diff --git a/src/plugins/instantiate/Makefile.in b/src/plugins/instantiate/Makefile.in
index 843525c882d..144f5c7128e 100644
--- a/src/plugins/instantiate/Makefile.in
+++ b/src/plugins/instantiate/Makefile.in
@@ -55,7 +55,7 @@ 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)
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index c525eb2cd2b..660db8c83c0 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 96ab43c06e5..41679ef1d11 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 e1cc1460c39..86eada6103d 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
@@ -143,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 7e00ccdb12e..7ef4c509bb2 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 9cc215a7711..16521b530ae 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
@@ -82,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 e493cbb3939..633294db95b 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
@@ -103,7 +105,7 @@ let well_typed_call _ret = function
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 ] ->
@@ -114,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 02d06b3d5ea..d0db608eef1 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
@@ -109,7 +111,7 @@ let well_typed_call _ret = function
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 ] ->
@@ -120,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 75aef926971..6481c423a1f 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
@@ -103,7 +105,7 @@ let well_typed_call _ret = function
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 ] ->
@@ -114,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 79c0fd60bbe..393f6ae626b 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"
@@ -67,7 +69,7 @@ let pset_len_bytes_to_zero ?loc ptr bytes_len =
| 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
@@ -210,7 +215,7 @@ let key_from_call _ret = function
(type_from_arg ptr), None
| [ 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) ;
@@ -239,7 +244,7 @@ let generate_prototype = function
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
@@ -255,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
@@ -264,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/transform.ml b/src/plugins/instantiate/transform.ml
index 7ef4a276a17..28f7a1ca811 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -126,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 ;
@@ -133,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 =
--
GitLab