diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 8c05dec02008ff757e793a7f2ae32a355f3dae04..a890cf521e219a4627dfb9be7669b19ef11f0a94 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -34,6 +34,21 @@ let term_to_exp_ref
: (kernel_function -> Env.t -> term -> exp * Env.t) ref
= Extlib.mk_fun "term_to_exp_ref"
+let gmp_to_sizet_ref
+ : (loc:location ->
+ name:string ->
+ ?check_lower_bound:bool ->
+ ?pp:term ->
+ kernel_function ->
+ Env.t ->
+ term ->
+ exp * Env.t) ref
+ =
+ let func ~loc:_ ~name:_ ?check_lower_bound:_ ?pp:_ _kf _env _t =
+ Extlib.mk_labeled_fun "gmp_to_sizet_ref"
+ in
+ ref func
+
(*****************************************************************************)
(****************************** Ranges Elimination ***************************)
(*****************************************************************************)
@@ -139,33 +154,8 @@ let call ~loc kf name ctx env t =
The case where [!(0 <= size <= SIZE_MAX)] is an UB ==> guard against it.
Since the case [0 <= size] is already checked before calling this function,
only [size <= SIZE_MAX] is added as a guard. *)
-let gmp_to_sizet ~loc kf env size p =
- let sizet = Cil.(theMachine.typeOfSizeOf) in
- (* The guard *)
- let sizet_max = Logic_const.tint
- ~loc (Cil.max_unsigned_number (Cil.bitsSizeOf sizet))
- in
- let guard = Logic_const.prel ~loc (Rle, size, sizet_max) in
- Typing.type_named_predicate ~must_clear:false guard;
- let guard, env = !predicate_to_exp_ref kf env guard in
- (* Translate term [size] into an exp of type [size_t] *)
- let size, env = !term_to_exp_ref kf env size in
- let _, e, env = Env.new_var
- ~loc
- ~name:"size"
- env
- kf
- None
- sizet
- (fun vi _ ->
- [ Smart_stmt.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf guard p;
- Smart_stmt.rtl_call ~loc
- ~result:(Cil.var vi)
- ~prefix:""
- "__gmpz_get_ui"
- [ size ] ])
- in
- e, env
+let gmp_to_sizet ~loc ?pp kf env size _p =
+ !gmp_to_sizet_ref ~loc ~name:"offset" ~check_lower_bound:false ?pp kf env size
(* Take a term of the form [ptr + r] where [ptr] is an address and [r] a range
offset, and return a tuple [(ptr, size, env)] where [ptr] is the address of
@@ -246,7 +236,19 @@ let range_to_ptr_and_size ~loc kf env ptr r p =
Typing.type_term ~use_gmp_opt:false size_term;
let size, env = match Typing.get_number_ty size_term with
| Typing.Gmpz ->
- gmp_to_sizet ~loc kf env size_term p
+ (* Start by translating [size_term] to an expression so that the full term
+ with [\let] is not passed around. *)
+ let size_e, env = !term_to_exp_ref kf env size_term in
+ (* Since translating a GMP code should always produce a C variable, we
+ can reuse it as a term for the function [gmp_to_sizet]. *)
+ let cvar_term =
+ match size_e.enode with
+ | Lval (Var vi, NoOffset) -> Cil.cvar_to_term ~loc vi
+ | _ ->
+ Options.fatal
+ "translation to GMP code should always return a C variable"
+ in
+ gmp_to_sizet ~loc ~pp:size_term kf env cvar_term p
| Typing.(C_integer _ | C_float _) ->
!term_to_exp_ref kf env size_term
| Typing.(Rational | Real | Nan) ->
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.mli b/src/plugins/e-acsl/src/code_generator/memory_translate.mli
index 184c81404cf3c5611b7ae49116f781a75fd7bf70..e5e0ced77456cf1391e0723b48f5102c32ae5ad8 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.mli
@@ -60,3 +60,13 @@ val predicate_to_exp_ref:
val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
+
+val gmp_to_sizet_ref:
+ (loc:location ->
+ name:string ->
+ ?check_lower_bound:bool ->
+ ?pp:term ->
+ kernel_function ->
+ Env.t ->
+ term ->
+ exp * Env.t) ref
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 0141cf409140d2affe193f72bdf4993aab124345..2d42a0c8fa0c0b5deafc1eccdb528832c9f0362d 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1149,6 +1149,78 @@ and translate_predicate ?pred_to_print kf env p =
let predicate_to_exp_without_rte ?name kf env p =
predicate_to_exp ?name kf env p (* forget optional argument ?rte *)
+let gmp_to_sizet ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
+ let pp = match pp with Some size_pp -> size_pp | None -> t in
+ let sizet = Cil.(theMachine.typeOfSizeOf) in
+ let stmts = [] in
+ (* Lower guard *)
+ let stmts, env =
+ if check_lower_bound then begin
+ let zero_term = Cil.lzero ~loc () in
+ let pred_name = Format.sprintf "%s_greater_or_eq_than_0" name in
+ let lower_guard_pp = Logic_const.prel ~loc (Rge, pp, zero_term) in
+ let lower_guard_pp =
+ { lower_guard_pp with
+ pred_name = pred_name :: lower_guard_pp.pred_name }
+ in
+ let lower_guard = Logic_const.prel ~loc (Rge, t, zero_term) in
+ Typing.type_named_predicate ~must_clear:false lower_guard;
+ let lower_guard, env = predicate_to_exp kf env lower_guard in
+ let assertion =
+ Smart_stmt.runtime_check
+ ~pred_kind:Assert
+ Smart_stmt.RTE
+ kf
+ lower_guard
+ lower_guard_pp
+ in
+ assertion :: stmts, env
+ end
+ else stmts, env
+ in
+ (* Upper guard *)
+ let sizet_max =
+ Logic_const.tint ~loc (Cil.max_unsigned_number (Cil.bitsSizeOf sizet))
+ in
+ let pred_name = Format.sprintf "%s_lesser_or_eq_than_SIZE_MAX" name in
+ let upper_guard_pp = Logic_const.prel ~loc (Rle, pp, sizet_max) in
+ let upper_guard_pp =
+ { upper_guard_pp with
+ pred_name = pred_name :: upper_guard_pp.pred_name }
+ in
+ let upper_guard = Logic_const.prel ~loc (Rle, t, sizet_max) in
+ Typing.type_named_predicate ~must_clear:false upper_guard;
+ let upper_guard, env = predicate_to_exp kf env upper_guard in
+ let assertion =
+ Smart_stmt.runtime_check
+ ~pred_kind:Assert
+ Smart_stmt.RTE
+ kf
+ upper_guard
+ upper_guard_pp
+ in
+ let stmts = assertion :: stmts in
+ (* Translate term [t] into an exp of type [size_t] *)
+ let gmp_e, env = term_to_exp kf env t in
+ let _, e, env = Env.new_var
+ ~loc
+ ~name:"size"
+ env
+ kf
+ None
+ sizet
+ (fun vi _ ->
+ let rtl_call =
+ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var vi)
+ ~prefix:""
+ "__gmpz_get_ui"
+ [ gmp_e ]
+ in
+ List.rev (rtl_call :: stmts))
+ in
+ e, env
+
let () =
Loops.term_to_exp_ref := term_to_exp;
Loops.translate_predicate_ref := translate_predicate;
@@ -1158,6 +1230,7 @@ let () =
At_with_lscope.predicate_to_exp_ref := predicate_to_exp_without_rte;
Memory_translate.term_to_exp_ref := term_to_exp;
Memory_translate.predicate_to_exp_ref := predicate_to_exp_without_rte;
+ Memory_translate.gmp_to_sizet_ref := gmp_to_sizet;
Logic_functions.term_to_exp_ref := term_to_exp;
Logic_functions.predicate_to_exp_ref := predicate_to_exp_without_rte;
Logic_array.translate_rte_ref := translate_rte
diff --git a/src/plugins/e-acsl/src/code_generator/translate.mli b/src/plugins/e-acsl/src/code_generator/translate.mli
index 0e738036d651f90899d4933d13def123d07841e8..f5e814dfaf1bd73ea7ba8de4e57915db290d3bf1 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate.mli
@@ -63,6 +63,22 @@ val translate_rte_annots:
(** Translate the given RTE annotations into runtime checks in the given
environment. *)
+val gmp_to_sizet:
+ loc:location ->
+ name:string ->
+ ?check_lower_bound:bool ->
+ ?pp:term ->
+ kernel_function ->
+ Env.t ->
+ term ->
+ exp * Env.t
+(** Translate the given GMP integer to an expression of type [size_t]. RTE
+ checks are generated to ensure that the GMP value holds in this type.
+ The parameter [name] is used to generate relevant predicate names.
+ If [check_lower_bound] is set to [false], then the GMP value is assumed to
+ be positive.
+ If [pp] is provided, this term is used in the messages of the RTE checks. *)
+
exception No_simple_term_translation of term
(** Exceptin raised if [untyped_term_to_exp] would generate new statements in
the environment *)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
index 379095819663d4d5c9ea19235966217930c73bea..152d6087e0c65af8113b81075ad7742310cf426b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
@@ -463,9 +463,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_mpz_t __gen_e_acsl_if;
__e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_le_2;
- __e_acsl_mpz_t __gen_e_acsl_size_3;
- int __gen_e_acsl_le_3;
- unsigned long __gen_e_acsl_size_4;
+ unsigned long __gen_e_acsl_size_3;
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& ptr),(size_t)8);
__gmpz_init_set_si(__gen_e_acsl_sizeof,8L);
@@ -504,16 +502,12 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_init_set_ui(__gen_e_acsl__4,18446744073709551615UL);
__gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __gmpz_init_set(__gen_e_acsl_size_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
- __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,1,"RTE","g",
- "\\valid(ptr + (0 .. size - 1))",
+ "offset_lesser_or_eq_than_SIZE_MAX:\n (\\let size = sizeof(long) * (((size - 1) - 0) + 1); size <= 0? 0: size) <=\n 18446744073709551615",
"tests/memory/ranges_in_builtins.c",7);
- __gen_e_acsl_size_4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 8 * 0),
- __gen_e_acsl_size_4,(void *)ptr,
+ __gen_e_acsl_size_3,(void *)ptr,
(void *)(& ptr));
__e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","g",
"\\valid(ptr + (0 .. size - 1))",
@@ -529,104 +523,89 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_clear(__gen_e_acsl_mul);
__gmpz_clear(__gen_e_acsl_if);
__gmpz_clear(__gen_e_acsl__4);
- __gmpz_clear(__gen_e_acsl_size_3);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_size_8;
- __gmpz_init_set_ui(__gen_e_acsl_size_8,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_8));
- __gmpz_clear(__gen_e_acsl_size_8);
}
{
- __e_acsl_mpz_t __gen_e_acsl_size_6;
- __gmpz_init_set_ui(__gen_e_acsl_size_6,size);
+ __e_acsl_mpz_t __gen_e_acsl_size_5;
+ __gmpz_init_set_ui(__gen_e_acsl_size_5,size);
__gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
- __gmpz_clear(__gen_e_acsl_size_6);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
+ __gmpz_clear(__gen_e_acsl_size_5);
}
__gen_e_acsl_at = ptr;
g(ptr,size);
{
- __e_acsl_mpz_t __gen_e_acsl_size_5;
+ __e_acsl_mpz_t __gen_e_acsl_size_4;
__e_acsl_mpz_t __gen_e_acsl_sizeof_2;
- __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__5;
__e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl__6;
__e_acsl_mpz_t __gen_e_acsl_sub_3;
__e_acsl_mpz_t __gen_e_acsl_add_3;
__e_acsl_mpz_t __gen_e_acsl_mul_2;
- int __gen_e_acsl_le_4;
+ int __gen_e_acsl_le_3;
__e_acsl_mpz_t __gen_e_acsl_if_2;
- __e_acsl_mpz_t __gen_e_acsl__9;
- int __gen_e_acsl_le_5;
- __e_acsl_mpz_t __gen_e_acsl_size_7;
- int __gen_e_acsl_le_6;
- unsigned long __gen_e_acsl_size_9;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ int __gen_e_acsl_le_4;
+ unsigned long __gen_e_acsl_size_6;
int __gen_e_acsl_valid_2;
__gmpz_init_set_si(__gen_e_acsl_sizeof_2,8L);
- __gmpz_init_set_si(__gen_e_acsl__6,1L);
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_init_set_si(__gen_e_acsl__6,0L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__gmpz_init(__gen_e_acsl_mul_2);
__gmpz_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_init_set(__gen_e_acsl_size_5,
+ __gmpz_init_set(__gen_e_acsl_size_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
- __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
- if (__gen_e_acsl_le_4 <= 0) {
- __e_acsl_mpz_t __gen_e_acsl__8;
- __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ if (__gen_e_acsl_le_3 <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
__gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __gmpz_clear(__gen_e_acsl__8);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_clear(__gen_e_acsl__7);
}
else __gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
- __gmpz_init_set_ui(__gen_e_acsl__9,18446744073709551615UL);
- __gen_e_acsl_le_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- __gmpz_init_set(__gen_e_acsl_size_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
- __gen_e_acsl_le_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
- __e_acsl_assert(__gen_e_acsl_le_5 <= 0,1,"RTE","g",
- "\\valid(\\old(ptr) + (0 .. \\old(size) + 1))",
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
+ __gmpz_init_set_ui(__gen_e_acsl__8,18446744073709551615UL);
+ __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __e_acsl_assert(__gen_e_acsl_le_4 <= 0,1,"RTE","g",
+ "offset_lesser_or_eq_than_SIZE_MAX:\n (\\let size = sizeof(long) * (((\\old(size) + 1) - 0) + 1);\n size <= 0? 0: size)\n <= 18446744073709551615",
"tests/memory/ranges_in_builtins.c",8);
- __gen_e_acsl_size_9 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+ __gen_e_acsl_size_6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)__gen_e_acsl_at +
8 * 0),
- __gen_e_acsl_size_9,
+ __gen_e_acsl_size_6,
(void *)__gen_e_acsl_at,
(void *)(& __gen_e_acsl_at));
__e_acsl_assert(! __gen_e_acsl_valid_2,1,"Postcondition","g",
"!\\valid(\\old(ptr) + (0 .. \\old(size) + 1))",
"tests/memory/ranges_in_builtins.c",8);
__e_acsl_delete_block((void *)(& ptr));
- __gmpz_clear(__gen_e_acsl_size_5);
+ __gmpz_clear(__gen_e_acsl_size_4);
__gmpz_clear(__gen_e_acsl_sizeof_2);
- __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__5);
__gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl_sub_3);
__gmpz_clear(__gen_e_acsl_add_3);
__gmpz_clear(__gen_e_acsl_mul_2);
__gmpz_clear(__gen_e_acsl_if_2);
- __gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl_size_7);
+ __gmpz_clear(__gen_e_acsl__8);
__gmpz_clear(__gen_e_acsl_at_2);
return;
}
@@ -651,9 +630,7 @@ void __gen_e_acsl_f(char *s, long n)
__e_acsl_mpz_t __gen_e_acsl_if;
__e_acsl_mpz_t __gen_e_acsl__6;
int __gen_e_acsl_le_2;
- __e_acsl_mpz_t __gen_e_acsl_size_2;
- int __gen_e_acsl_le_3;
- unsigned long __gen_e_acsl_size_3;
+ unsigned long __gen_e_acsl_size_2;
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& s),(size_t)8);
__gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
@@ -694,16 +671,12 @@ void __gen_e_acsl_f(char *s, long n)
__gmpz_init_set_ui(__gen_e_acsl__6,18446744073709551615UL);
__gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- __gmpz_init_set(__gen_e_acsl_size_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
- __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,1,"RTE","f",
- "\\valid(s + (3 .. n + 1000))",
+ "offset_lesser_or_eq_than_SIZE_MAX:\n (\\let size = sizeof(char) * (((n + 1000) - 3) + 1); size <= 0? 0: size) <=\n 18446744073709551615",
"tests/memory/ranges_in_builtins.c",5);
- __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_size_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
__gen_e_acsl_valid = __e_acsl_valid((void *)(s + 1 * 3),
- __gen_e_acsl_size_3,(void *)s,
+ __gen_e_acsl_size_2,(void *)s,
(void *)(& s));
__e_acsl_assert(! __gen_e_acsl_valid,1,"Precondition","f",
"!\\valid(s + (3 .. n + 1000))",
@@ -721,7 +694,6 @@ void __gen_e_acsl_f(char *s, long n)
__gmpz_clear(__gen_e_acsl__4);
__gmpz_clear(__gen_e_acsl_if);
__gmpz_clear(__gen_e_acsl__6);
- __gmpz_clear(__gen_e_acsl_size_2);
}
f(s,n);
__e_acsl_delete_block((void *)(& s));
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
index 8852be6a5f86f34777d18630a81b2c6ce7bc3df7..1c942fd837e8066e8d5ee869ce6051ed1308b305 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
@@ -8,8 +8,6 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/memory/ranges_in_builtins.c:7: Warning:
function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning:
- function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
[eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning: