From 632573a2a52c080e1d6dac221f91b0e7fc1a959e Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 22 Mar 2016 10:09:22 +0100
Subject: [PATCH] [typing] infer type of intervals wrt context: reduce the
number of generated casts
---
src/plugins/e-acsl/new_typing.ml | 56 ++-
src/plugins/e-acsl/new_typing.mli | 6 +-
src/plugins/e-acsl/quantif.ml | 2 +-
.../oracle/block_length.res.oracle | 2 +-
.../e-acsl-runtime/oracle/gen_base_addr.c | 24 +-
.../e-acsl-runtime/oracle/gen_block_length.c | 351 ++++--------------
.../oracle/initialized.res.oracle | 4 +-
.../e-acsl-runtime/oracle/vector.res.oracle | 4 +-
.../tests/gmp/oracle/comparison.1.res.oracle | 1 +
.../e-acsl/tests/gmp/oracle/gen_comparison2.c | 48 +--
.../tests/gmp/oracle/gen_integer_constant2.c | 6 +-
.../e-acsl/tests/gmp/oracle/gen_longlong.c | 6 +-
.../e-acsl/tests/gmp/oracle/gen_longlong2.c | 6 +-
.../e-acsl/tests/gmp/oracle/gen_not2.c | 4 +-
.../gmp/oracle/integer_constant.1.res.oracle | 3 +-
.../tests/gmp/oracle/longlong.0.res.oracle | 10 +-
.../tests/gmp/oracle/longlong.1.res.oracle | 10 +-
.../e-acsl/tests/gmp/oracle/not.1.res.oracle | 1 +
src/plugins/e-acsl/translate.ml | 12 +-
19 files changed, 191 insertions(+), 365 deletions(-)
diff --git a/src/plugins/e-acsl/new_typing.ml b/src/plugins/e-acsl/new_typing.ml
index a7ae7dbb5ba..f47671881fe 100644
--- a/src/plugins/e-acsl/new_typing.ml
+++ b/src/plugins/e-acsl/new_typing.ml
@@ -41,6 +41,10 @@ type integer_ty =
| C_type of ikind
| Other
+let gmp = Gmp
+let c_int = C_type IInt
+let ikind ik = C_type ik
+
let join ty1 ty2 = match ty1, ty2 with
| Other, Other -> Other
| Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
@@ -59,8 +63,6 @@ let typ_of_integer_ty = function
| C_type ik -> TInt(ik, [])
| Other -> Options.fatal "[typing] not an integer type"
-let c_int = C_type IInt
-
let size_t () = match Cil.theMachine.Cil.typeOfSizeOf with
| TInt(kind, _) -> C_type kind
| _ -> assert false
@@ -132,16 +134,18 @@ end
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
-let ty_of_interv i =
+let ty_of_interv ~ctx i =
let open Interval in
let is_pos = Integer.ge i.lower Integer.zero in
try
let lkind = Cil.intKindForValue i.lower is_pos in
let ukind = Cil.intKindForValue i.upper is_pos in
let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
- (* int whenever possible to prevent superfluous casts in the generated
+ (* ctx type whenever possible to prevent superfluous casts in the generated
code *)
- if Cil.intTypeIncluded kind IInt then c_int else C_type kind
+ (match ctx with
+ | Gmp | Other -> C_type kind
+ | C_type ik -> if Cil.intTypeIncluded kind ik then ctx else C_type kind)
with Cil.Not_representable ->
Gmp
@@ -174,7 +178,7 @@ let rec type_term env ~ctx t =
| TAlignOf _ ->
(try
let i = Interval.infer env t in
- ty_of_interv i
+ ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
@@ -182,7 +186,7 @@ let rec type_term env ~ctx t =
(try
let i = Interval.infer env t in
type_term_lval env tlv;
- ty_of_interv i
+ ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
@@ -193,7 +197,7 @@ let rec type_term env ~ctx t =
let i = Interval.infer env t in
(* [t'] must be typed, but it is a pointer *)
ignore (type_term env ~ctx:Other t');
- ty_of_interv i
+ ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
@@ -203,14 +207,14 @@ let rec type_term env ~ctx t =
(* [t1] and [t2] must be typed, but they are pointers *)
ignore (type_term env ~ctx:Other t1);
ignore (type_term env ~ctx:Other t2);
- ty_of_interv i
+ ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
| TUnOp (_, t') ->
let i = Interval.infer env t in
let i' = Interval.infer env t' in
- let ctx = mk_ctx (ty_of_interv (Interval.join i i')) in
+ let ctx = mk_ctx (ty_of_interv ~ctx (Interval.join i i')) in
ignore (type_term env ~ctx t');
ctx
@@ -218,7 +222,9 @@ let rec type_term env ~ctx t =
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
- let ctx = mk_ctx (ty_of_interv (Interval.join i (Interval.join i1 i2))) in
+ let ctx =
+ mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)))
+ in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
ctx
@@ -228,7 +234,7 @@ let rec type_term env ~ctx t =
try
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
- mk_ctx (ty_of_interv (Interval.join i1 i2))
+ mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
@@ -244,7 +250,7 @@ let rec type_term env ~ctx t =
(* both operands fit in an int. *)
ignore (type_term env ~ctx:c_int t1);
ignore (type_term env ~ctx:c_int t2);
- ty_of_interv (Interval.join i1 i2)
+ ty_of_interv ~ctx (Interval.join i1 i2)
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
| TBinOp (BXor, _, _) -> Error.not_yet "bitwise xor"
@@ -258,7 +264,7 @@ let rec type_term env ~ctx t =
(* nothing to do more: [i] is already more precise than what we could
infer from the arguments of the cast. Also, do not type the internal
term: possibly it is not even an integer *)
- let ty = ty_of_interv i in
+ let ty = ty_of_interv ~ctx i in
ignore (type_term env ~ctx:ty t');
ty
with Interval.Not_an_integer ->
@@ -273,7 +279,7 @@ let rec type_term env ~ctx t =
try
let i2 = Interval.infer env t2 in
let i3 = Interval.infer env t3 in
- mk_ctx (ty_of_interv (Interval.join i (Interval.join i2 i3)))
+ mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)))
with Interval.Not_an_integer ->
Other
in
@@ -288,7 +294,7 @@ let rec type_term env ~ctx t =
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
- let ty = ty_of_interv (Interval.join i (Interval.join i1 i2)) in
+ let ty = ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)) in
ignore (type_term env ~ctx:ty t1);
ignore (type_term env ~ctx:ty t2);
ty
@@ -361,7 +367,7 @@ let rec type_predicate_named env p =
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
let i = Interval.join i1 i2 in
- mk_ctx (ty_of_interv i)
+ mk_ctx (ty_of_interv ~ctx:c_int i)
with Interval.Not_an_integer ->
Other
in
@@ -409,7 +415,21 @@ let rec type_predicate_named env p =
| _ -> assert false
in
let i = Interval.join i1 i2 in
- let ctx = mk_ctx (ty_of_interv i) in
+ let ctx = match x.lv_type with
+ | Linteger -> Gmp
+ | Ctype ty ->
+ (match Cil.unrollType ty with
+ | TInt(ik, _) -> C_type ik
+ | ty ->
+ Options.fatal "unexpected type %a for quantified variable %a"
+ Printer.pp_typ ty
+ Printer.pp_logic_var x)
+ | lty ->
+ Options.fatal "unexpected type %a for quantified variable %a"
+ Printer.pp_logic_type lty
+ Printer.pp_logic_var x
+ in
+ let ctx = mk_ctx (ty_of_interv ~ctx i) in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
Interval.Env.add x i env)
diff --git a/src/plugins/e-acsl/new_typing.mli b/src/plugins/e-acsl/new_typing.mli
index ee77469207b..aeb35c701be 100644
--- a/src/plugins/e-acsl/new_typing.mli
+++ b/src/plugins/e-acsl/new_typing.mli
@@ -30,11 +30,15 @@ open Cil_types
(** {2 Datatypes} *)
(******************************************************************************)
-type integer_ty =
+type integer_ty = private
| Gmp
| C_type of ikind
| Other
+val gmp: integer_ty
+val c_int: integer_ty
+val ikind: ikind -> integer_ty
+
val typ_of_integer_ty: integer_ty -> typ
val join: integer_ty -> integer_ty -> integer_ty
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index ddc097dc46c..bce6ad891ef 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -214,7 +214,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
let tlv = Logic_const.tvar ~loc llv in
let guard = Logic_const.term ~loc (TBinOp(bop2, tlv, t2)) Linteger in
- New_typing.type_term ~ctx:(New_typing.C_type IInt) guard;
+ New_typing.type_term ~ctx:New_typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
let guard_blk, env =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
index 33f7f62f158..554caab3fd5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
@@ -13,10 +13,10 @@ FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns claus
FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/block_length.c:45:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/block_length.c:46:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/block_length.c:48:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/block_length.c:54:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
index 14aba6b8cd0..8363cb460ba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
@@ -48,7 +48,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_3;
void *__gen_e_acsl_base_addr_4;
- __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[(unsigned long)3]));
+ __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[3]));
__gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)PA);
__e_acsl_assert(__gen_e_acsl_base_addr_3 == __gen_e_acsl_base_addr_4,
(char *)"Assertion",(char *)"main",
@@ -69,8 +69,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_7;
void *__gen_e_acsl_base_addr_8;
- __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + (unsigned long)2));
- __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[(unsigned long)3]));
+ __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + 2));
+ __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3]));
__e_acsl_assert(__gen_e_acsl_base_addr_7 == __gen_e_acsl_base_addr_8,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(PA+2) == \\base_addr(&A[3])",17);
@@ -99,7 +99,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_11;
void *__gen_e_acsl_base_addr_12;
- __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[(unsigned long)3]));
+ __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[3]));
__gen_e_acsl_base_addr_12 = __e_acsl_base_addr((void *)pa);
__e_acsl_assert(__gen_e_acsl_base_addr_11 == __gen_e_acsl_base_addr_12,
(char *)"Assertion",(char *)"main",
@@ -121,7 +121,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_15;
void *__gen_e_acsl_base_addr_16;
- __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + (unsigned long)2));
+ __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + 2));
__gen_e_acsl_base_addr_16 = __e_acsl_base_addr((void *)(a));
__e_acsl_assert(__gen_e_acsl_base_addr_15 == __gen_e_acsl_base_addr_16,
(char *)"Assertion",(char *)"main",
@@ -145,7 +145,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_19;
void *__gen_e_acsl_base_addr_20;
- __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + (unsigned long)2));
+ __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + 2));
__gen_e_acsl_base_addr_20 = __e_acsl_base_addr((void *)(& l));
__e_acsl_assert(__gen_e_acsl_base_addr_19 == __gen_e_acsl_base_addr_20,
(char *)"Assertion",(char *)"main",
@@ -195,8 +195,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_27;
void *__gen_e_acsl_base_addr_28;
- __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + (unsigned long)1));
- __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + (unsigned long)5));
+ __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + 1));
+ __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5));
__e_acsl_assert(__gen_e_acsl_base_addr_27 == __gen_e_acsl_base_addr_28,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(p+1) == \\base_addr(pd+5)",45);
@@ -205,8 +205,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_29;
void *__gen_e_acsl_base_addr_30;
- __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + (unsigned long)11));
- __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + (unsigned long)1));
+ __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + 11));
+ __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1));
__e_acsl_assert(__gen_e_acsl_base_addr_29 == __gen_e_acsl_base_addr_30,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(p+11) == \\base_addr(pd+1)",46);
@@ -217,7 +217,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_31;
void *__gen_e_acsl_base_addr_32;
- __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + (unsigned long)5));
+ __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 5));
__gen_e_acsl_base_addr_32 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_31 == __gen_e_acsl_base_addr_32,
(char *)"Assertion",(char *)"main",
@@ -227,7 +227,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_33;
void *__gen_e_acsl_base_addr_34;
- __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - (unsigned long)5));
+ __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - 5));
__gen_e_acsl_base_addr_34 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_33 == __gen_e_acsl_base_addr_34,
(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c
index 151a794d210..7de3d4ff48c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c
@@ -42,77 +42,38 @@ int main(void)
/*@ assert \block_length((int *)A) ≡ sizeof(A); */
{
unsigned long __gen_e_acsl_block_length;
- mpz_t __gen_e_acsl_block_length_2;
- mpz_t __gen_e_acsl_sizeof;
- int __gen_e_acsl_eq;
__gen_e_acsl_block_length = __e_acsl_block_length((void *)(A));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_2,__gen_e_acsl_block_length);
- __gmpz_init_set_si(__gen_e_acsl_sizeof,16L);
- __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_2),
- (__mpz_struct const *)(__gen_e_acsl_sizeof));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(__gen_e_acsl_block_length == 16,(char *)"Assertion",
+ (char *)"main",
(char *)"\\block_length((int *)A) == sizeof(A)",15);
- __gmpz_clear(__gen_e_acsl_block_length_2);
- __gmpz_clear(__gen_e_acsl_sizeof);
}
/*@ assert \block_length(&A[3]) ≡ sizeof(A); */
{
- unsigned long __gen_e_acsl_block_length_3;
- mpz_t __gen_e_acsl_block_length_4;
- mpz_t __gen_e_acsl_sizeof_2;
- int __gen_e_acsl_eq_2;
- __gen_e_acsl_block_length_3 = __e_acsl_block_length((void *)(& A[3]));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_4,
- __gen_e_acsl_block_length_3);
- __gmpz_init_set_si(__gen_e_acsl_sizeof_2,16L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_4),
- (__mpz_struct const *)(__gen_e_acsl_sizeof_2));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_2;
+ __gen_e_acsl_block_length_2 = __e_acsl_block_length((void *)(& A[3]));
+ __e_acsl_assert(__gen_e_acsl_block_length_2 == 16,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&A[3]) == sizeof(A)",16);
- __gmpz_clear(__gen_e_acsl_block_length_4);
- __gmpz_clear(__gen_e_acsl_sizeof_2);
}
/*@ assert \block_length(PA) ≡ sizeof(A); */
{
- unsigned long __gen_e_acsl_block_length_5;
- mpz_t __gen_e_acsl_block_length_6;
- mpz_t __gen_e_acsl_sizeof_3;
- int __gen_e_acsl_eq_3;
- __gen_e_acsl_block_length_5 = __e_acsl_block_length((void *)PA);
- __gmpz_init_set_ui(__gen_e_acsl_block_length_6,
- __gen_e_acsl_block_length_5);
- __gmpz_init_set_si(__gen_e_acsl_sizeof_3,16L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_6),
- (__mpz_struct const *)(__gen_e_acsl_sizeof_3));
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_3;
+ __gen_e_acsl_block_length_3 = __e_acsl_block_length((void *)PA);
+ __e_acsl_assert(__gen_e_acsl_block_length_3 == 16,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(PA) == sizeof(A)",
17);
- __gmpz_clear(__gen_e_acsl_block_length_6);
- __gmpz_clear(__gen_e_acsl_sizeof_3);
}
PA ++;
/*@ assert \block_length(PA+1) ≡ \block_length(&A[1]); */
{
- unsigned long __gen_e_acsl_block_length_7;
- mpz_t __gen_e_acsl_block_length_8;
- unsigned long __gen_e_acsl_block_length_9;
- mpz_t __gen_e_acsl_block_length_10;
- int __gen_e_acsl_eq_4;
- __gen_e_acsl_block_length_7 = __e_acsl_block_length((void *)(PA + 1));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_8,
- __gen_e_acsl_block_length_7);
- __gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(& A[1]));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_10,
- __gen_e_acsl_block_length_9);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_8),
- (__mpz_struct const *)(__gen_e_acsl_block_length_10));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
- (char *)"main",
+ unsigned long __gen_e_acsl_block_length_4;
+ unsigned long __gen_e_acsl_block_length_5;
+ __gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(PA + 1));
+ __gen_e_acsl_block_length_5 = __e_acsl_block_length((void *)(& A[1]));
+ __e_acsl_assert(__gen_e_acsl_block_length_4 == __gen_e_acsl_block_length_5,
+ (char *)"Assertion",(char *)"main",
(char *)"\\block_length(PA+1) == \\block_length(&A[1])",
19);
- __gmpz_clear(__gen_e_acsl_block_length_8);
- __gmpz_clear(__gen_e_acsl_block_length_10);
}
__e_acsl_initialize((void *)(a),sizeof(int));
a[0] = 1;
@@ -126,81 +87,40 @@ int main(void)
pa = (int *)(& a);
/*@ assert \block_length((int *)a) ≡ sizeof(a); */
{
- unsigned long __gen_e_acsl_block_length_11;
- mpz_t __gen_e_acsl_block_length_12;
- mpz_t __gen_e_acsl_sizeof_4;
- int __gen_e_acsl_eq_5;
- __gen_e_acsl_block_length_11 = __e_acsl_block_length((void *)(a));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_12,
- __gen_e_acsl_block_length_11);
- __gmpz_init_set_si(__gen_e_acsl_sizeof_4,16L);
- __gen_e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_12),
- (__mpz_struct const *)(__gen_e_acsl_sizeof_4));
- __e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_6;
+ __gen_e_acsl_block_length_6 = __e_acsl_block_length((void *)(a));
+ __e_acsl_assert(__gen_e_acsl_block_length_6 == 16,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length((int *)a) == sizeof(a)",24);
- __gmpz_clear(__gen_e_acsl_block_length_12);
- __gmpz_clear(__gen_e_acsl_sizeof_4);
}
/*@ assert \block_length(&a[3]) ≡ sizeof(a); */
{
- unsigned long __gen_e_acsl_block_length_13;
- mpz_t __gen_e_acsl_block_length_14;
- mpz_t __gen_e_acsl_sizeof_5;
- int __gen_e_acsl_eq_6;
- __gen_e_acsl_block_length_13 = __e_acsl_block_length((void *)(& a[3]));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_14,
- __gen_e_acsl_block_length_13);
- __gmpz_init_set_si(__gen_e_acsl_sizeof_5,16L);
- __gen_e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_14),
- (__mpz_struct const *)(__gen_e_acsl_sizeof_5));
- __e_acsl_assert(__gen_e_acsl_eq_6 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_7;
+ __gen_e_acsl_block_length_7 = __e_acsl_block_length((void *)(& a[3]));
+ __e_acsl_assert(__gen_e_acsl_block_length_7 == 16,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&a[3]) == sizeof(a)",25);
- __gmpz_clear(__gen_e_acsl_block_length_14);
- __gmpz_clear(__gen_e_acsl_sizeof_5);
}
/*@ assert \block_length(pa) ≡ sizeof(a); */
{
- unsigned long __gen_e_acsl_block_length_15;
- mpz_t __gen_e_acsl_block_length_16;
- mpz_t __gen_e_acsl_sizeof_6;
- int __gen_e_acsl_eq_7;
- __gen_e_acsl_block_length_15 = __e_acsl_block_length((void *)pa);
- __gmpz_init_set_ui(__gen_e_acsl_block_length_16,
- __gen_e_acsl_block_length_15);
- __gmpz_init_set_si(__gen_e_acsl_sizeof_6,16L);
- __gen_e_acsl_eq_7 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_16),
- (__mpz_struct const *)(__gen_e_acsl_sizeof_6));
- __e_acsl_assert(__gen_e_acsl_eq_7 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_8;
+ __gen_e_acsl_block_length_8 = __e_acsl_block_length((void *)pa);
+ __e_acsl_assert(__gen_e_acsl_block_length_8 == 16,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(pa) == sizeof(a)",
26);
- __gmpz_clear(__gen_e_acsl_block_length_16);
- __gmpz_clear(__gen_e_acsl_sizeof_6);
}
__e_acsl_full_init((void *)(& pa));
pa ++;
/*@ assert \block_length(pa+1) ≡ \block_length(&a[1]); */
{
- unsigned long __gen_e_acsl_block_length_17;
- mpz_t __gen_e_acsl_block_length_18;
- unsigned long __gen_e_acsl_block_length_19;
- mpz_t __gen_e_acsl_block_length_20;
- int __gen_e_acsl_eq_8;
- __gen_e_acsl_block_length_17 = __e_acsl_block_length((void *)(pa + 1));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_18,
- __gen_e_acsl_block_length_17);
- __gen_e_acsl_block_length_19 = __e_acsl_block_length((void *)(& a[1]));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_20,
- __gen_e_acsl_block_length_19);
- __gen_e_acsl_eq_8 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_18),
- (__mpz_struct const *)(__gen_e_acsl_block_length_20));
- __e_acsl_assert(__gen_e_acsl_eq_8 == 0,(char *)"Assertion",
- (char *)"main",
+ unsigned long __gen_e_acsl_block_length_9;
+ unsigned long __gen_e_acsl_block_length_10;
+ __gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(pa + 1));
+ __gen_e_acsl_block_length_10 = __e_acsl_block_length((void *)(& a[1]));
+ __e_acsl_assert(__gen_e_acsl_block_length_9 == __gen_e_acsl_block_length_10,
+ (char *)"Assertion",(char *)"main",
(char *)"\\block_length(pa+1) == \\block_length(&a[1])",
28);
- __gmpz_clear(__gen_e_acsl_block_length_18);
- __gmpz_clear(__gen_e_acsl_block_length_20);
}
__e_acsl_full_init((void *)(& l));
l = (long)4;
@@ -208,236 +128,113 @@ int main(void)
pl = (char *)(& l);
/*@ assert \block_length(&l) ≡ sizeof(long); */
{
- unsigned long __gen_e_acsl_block_length_21;
- mpz_t __gen_e_acsl_block_length_22;
- mpz_t __gen_e_acsl_sizeof_7;
- int __gen_e_acsl_eq_9;
- __gen_e_acsl_block_length_21 = __e_acsl_block_length((void *)(& l));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_22,
- __gen_e_acsl_block_length_21);
- __gmpz_init_set_si(__gen_e_acsl_sizeof_7,8L);
- __gen_e_acsl_eq_9 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_22),
- (__mpz_struct const *)(__gen_e_acsl_sizeof_7));
- __e_acsl_assert(__gen_e_acsl_eq_9 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_11;
+ __gen_e_acsl_block_length_11 = __e_acsl_block_length((void *)(& l));
+ __e_acsl_assert(__gen_e_acsl_block_length_11 == 8,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&l) == sizeof(long)",34);
- __gmpz_clear(__gen_e_acsl_block_length_22);
- __gmpz_clear(__gen_e_acsl_sizeof_7);
}
/*@ assert \block_length(pl) ≡ sizeof(long); */
{
- unsigned long __gen_e_acsl_block_length_23;
- mpz_t __gen_e_acsl_block_length_24;
- mpz_t __gen_e_acsl_sizeof_8;
- int __gen_e_acsl_eq_10;
- __gen_e_acsl_block_length_23 = __e_acsl_block_length((void *)pl);
- __gmpz_init_set_ui(__gen_e_acsl_block_length_24,
- __gen_e_acsl_block_length_23);
- __gmpz_init_set_si(__gen_e_acsl_sizeof_8,8L);
- __gen_e_acsl_eq_10 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_24),
- (__mpz_struct const *)(__gen_e_acsl_sizeof_8));
- __e_acsl_assert(__gen_e_acsl_eq_10 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_12;
+ __gen_e_acsl_block_length_12 = __e_acsl_block_length((void *)pl);
+ __e_acsl_assert(__gen_e_acsl_block_length_12 == 8,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(pl) == sizeof(long)",35);
- __gmpz_clear(__gen_e_acsl_block_length_24);
- __gmpz_clear(__gen_e_acsl_sizeof_8);
}
/*@ assert \block_length(pl+7) ≡ sizeof(long); */
{
- unsigned long __gen_e_acsl_block_length_25;
- mpz_t __gen_e_acsl_block_length_26;
- mpz_t __gen_e_acsl_sizeof_9;
- int __gen_e_acsl_eq_11;
- __gen_e_acsl_block_length_25 = __e_acsl_block_length((void *)(pl + 7));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_26,
- __gen_e_acsl_block_length_25);
- __gmpz_init_set_si(__gen_e_acsl_sizeof_9,8L);
- __gen_e_acsl_eq_11 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_26),
- (__mpz_struct const *)(__gen_e_acsl_sizeof_9));
- __e_acsl_assert(__gen_e_acsl_eq_11 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_13;
+ __gen_e_acsl_block_length_13 = __e_acsl_block_length((void *)(pl + 7));
+ __e_acsl_assert(__gen_e_acsl_block_length_13 == 8,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(pl+7) == sizeof(long)",36);
- __gmpz_clear(__gen_e_acsl_block_length_26);
- __gmpz_clear(__gen_e_acsl_sizeof_9);
}
__e_acsl_full_init((void *)(& pi));
pi = (int *)(& l);
/*@ assert \block_length(pi) ≡ \block_length(&l); */
{
- unsigned long __gen_e_acsl_block_length_27;
- mpz_t __gen_e_acsl_block_length_28;
- unsigned long __gen_e_acsl_block_length_29;
- mpz_t __gen_e_acsl_block_length_30;
- int __gen_e_acsl_eq_12;
- __gen_e_acsl_block_length_27 = __e_acsl_block_length((void *)pi);
- __gmpz_init_set_ui(__gen_e_acsl_block_length_28,
- __gen_e_acsl_block_length_27);
- __gen_e_acsl_block_length_29 = __e_acsl_block_length((void *)(& l));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_30,
- __gen_e_acsl_block_length_29);
- __gen_e_acsl_eq_12 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_28),
- (__mpz_struct const *)(__gen_e_acsl_block_length_30));
- __e_acsl_assert(__gen_e_acsl_eq_12 == 0,(char *)"Assertion",
- (char *)"main",
+ unsigned long __gen_e_acsl_block_length_14;
+ unsigned long __gen_e_acsl_block_length_15;
+ __gen_e_acsl_block_length_14 = __e_acsl_block_length((void *)pi);
+ __gen_e_acsl_block_length_15 = __e_acsl_block_length((void *)(& l));
+ __e_acsl_assert(__gen_e_acsl_block_length_14 == __gen_e_acsl_block_length_15,
+ (char *)"Assertion",(char *)"main",
(char *)"\\block_length(pi) == \\block_length(&l)",38);
- __gmpz_clear(__gen_e_acsl_block_length_28);
- __gmpz_clear(__gen_e_acsl_block_length_30);
}
__e_acsl_full_init((void *)(& pi));
pi ++;
/*@ assert \block_length(pi) ≡ \block_length(&l); */
{
- unsigned long __gen_e_acsl_block_length_31;
- mpz_t __gen_e_acsl_block_length_32;
- unsigned long __gen_e_acsl_block_length_33;
- mpz_t __gen_e_acsl_block_length_34;
- int __gen_e_acsl_eq_13;
- __gen_e_acsl_block_length_31 = __e_acsl_block_length((void *)pi);
- __gmpz_init_set_ui(__gen_e_acsl_block_length_32,
- __gen_e_acsl_block_length_31);
- __gen_e_acsl_block_length_33 = __e_acsl_block_length((void *)(& l));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_34,
- __gen_e_acsl_block_length_33);
- __gen_e_acsl_eq_13 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_32),
- (__mpz_struct const *)(__gen_e_acsl_block_length_34));
- __e_acsl_assert(__gen_e_acsl_eq_13 == 0,(char *)"Assertion",
- (char *)"main",
+ unsigned long __gen_e_acsl_block_length_16;
+ unsigned long __gen_e_acsl_block_length_17;
+ __gen_e_acsl_block_length_16 = __e_acsl_block_length((void *)pi);
+ __gen_e_acsl_block_length_17 = __e_acsl_block_length((void *)(& l));
+ __e_acsl_assert(__gen_e_acsl_block_length_16 == __gen_e_acsl_block_length_17,
+ (char *)"Assertion",(char *)"main",
(char *)"\\block_length(pi) == \\block_length(&l)",40);
- __gmpz_clear(__gen_e_acsl_block_length_32);
- __gmpz_clear(__gen_e_acsl_block_length_34);
}
size = (unsigned long)12;
__e_acsl_full_init((void *)(& p));
p = (char *)__gen_e_acsl_malloc(size);
/*@ assert \block_length(p) ≡ size; */
{
- unsigned long __gen_e_acsl_block_length_35;
- mpz_t __gen_e_acsl_block_length_36;
- mpz_t __gen_e_acsl_size;
- int __gen_e_acsl_eq_14;
- __gen_e_acsl_block_length_35 = __e_acsl_block_length((void *)p);
- __gmpz_init_set_ui(__gen_e_acsl_block_length_36,
- __gen_e_acsl_block_length_35);
- __gmpz_init_set_ui(__gen_e_acsl_size,size);
- __gen_e_acsl_eq_14 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_36),
- (__mpz_struct const *)(__gen_e_acsl_size));
- __e_acsl_assert(__gen_e_acsl_eq_14 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_18;
+ __gen_e_acsl_block_length_18 = __e_acsl_block_length((void *)p);
+ __e_acsl_assert(__gen_e_acsl_block_length_18 == size,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(p) == size",45);
- __gmpz_clear(__gen_e_acsl_block_length_36);
- __gmpz_clear(__gen_e_acsl_size);
}
/*@ assert \block_length(p+11) ≡ size; */
{
- unsigned long __gen_e_acsl_block_length_37;
- mpz_t __gen_e_acsl_block_length_38;
- mpz_t __gen_e_acsl_size_2;
- int __gen_e_acsl_eq_15;
- __gen_e_acsl_block_length_37 = __e_acsl_block_length((void *)(p + 11));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_38,
- __gen_e_acsl_block_length_37);
- __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
- __gen_e_acsl_eq_15 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_38),
- (__mpz_struct const *)(__gen_e_acsl_size_2));
- __e_acsl_assert(__gen_e_acsl_eq_15 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_19;
+ __gen_e_acsl_block_length_19 = __e_acsl_block_length((void *)(p + 11));
+ __e_acsl_assert(__gen_e_acsl_block_length_19 == size,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(p+11) == size",46);
- __gmpz_clear(__gen_e_acsl_block_length_38);
- __gmpz_clear(__gen_e_acsl_size_2);
}
__e_acsl_full_init((void *)(& p));
p += 5;
/*@ assert \block_length(p+5) ≡ \block_length(p-5); */
{
- unsigned long __gen_e_acsl_block_length_39;
- mpz_t __gen_e_acsl_block_length_40;
- unsigned long __gen_e_acsl_block_length_41;
- mpz_t __gen_e_acsl_block_length_42;
- int __gen_e_acsl_eq_16;
- __gen_e_acsl_block_length_39 = __e_acsl_block_length((void *)(p + 5));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_40,
- __gen_e_acsl_block_length_39);
- __gen_e_acsl_block_length_41 = __e_acsl_block_length((void *)(p - 5));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_42,
- __gen_e_acsl_block_length_41);
- __gen_e_acsl_eq_16 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_40),
- (__mpz_struct const *)(__gen_e_acsl_block_length_42));
- __e_acsl_assert(__gen_e_acsl_eq_16 == 0,(char *)"Assertion",
- (char *)"main",
+ unsigned long __gen_e_acsl_block_length_20;
+ unsigned long __gen_e_acsl_block_length_21;
+ __gen_e_acsl_block_length_20 = __e_acsl_block_length((void *)(p + 5));
+ __gen_e_acsl_block_length_21 = __e_acsl_block_length((void *)(p - 5));
+ __e_acsl_assert(__gen_e_acsl_block_length_20 == __gen_e_acsl_block_length_21,
+ (char *)"Assertion",(char *)"main",
(char *)"\\block_length(p+5) == \\block_length(p-5)",48);
- __gmpz_clear(__gen_e_acsl_block_length_40);
- __gmpz_clear(__gen_e_acsl_block_length_42);
}
size = (unsigned long)30 * sizeof(long);
__e_acsl_full_init((void *)(& q));
q = (long *)__gen_e_acsl_malloc(size);
/*@ assert \block_length(q) ≡ size; */
{
- unsigned long __gen_e_acsl_block_length_43;
- mpz_t __gen_e_acsl_block_length_44;
- mpz_t __gen_e_acsl_size_3;
- int __gen_e_acsl_eq_17;
- __gen_e_acsl_block_length_43 = __e_acsl_block_length((void *)q);
- __gmpz_init_set_ui(__gen_e_acsl_block_length_44,
- __gen_e_acsl_block_length_43);
- __gmpz_init_set_ui(__gen_e_acsl_size_3,size);
- __gen_e_acsl_eq_17 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_44),
- (__mpz_struct const *)(__gen_e_acsl_size_3));
- __e_acsl_assert(__gen_e_acsl_eq_17 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_22;
+ __gen_e_acsl_block_length_22 = __e_acsl_block_length((void *)q);
+ __e_acsl_assert(__gen_e_acsl_block_length_22 == size,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(q) == size",54);
- __gmpz_clear(__gen_e_acsl_block_length_44);
- __gmpz_clear(__gen_e_acsl_size_3);
}
__e_acsl_full_init((void *)(& q));
q += 4;
/*@ assert \block_length(q) ≡ size; */
{
- unsigned long __gen_e_acsl_block_length_45;
- mpz_t __gen_e_acsl_block_length_46;
- mpz_t __gen_e_acsl_size_4;
- int __gen_e_acsl_eq_18;
- __gen_e_acsl_block_length_45 = __e_acsl_block_length((void *)q);
- __gmpz_init_set_ui(__gen_e_acsl_block_length_46,
- __gen_e_acsl_block_length_45);
- __gmpz_init_set_ui(__gen_e_acsl_size_4,size);
- __gen_e_acsl_eq_18 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_46),
- (__mpz_struct const *)(__gen_e_acsl_size_4));
- __e_acsl_assert(__gen_e_acsl_eq_18 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_23;
+ __gen_e_acsl_block_length_23 = __e_acsl_block_length((void *)q);
+ __e_acsl_assert(__gen_e_acsl_block_length_23 == size,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(q) == size",56);
- __gmpz_clear(__gen_e_acsl_block_length_46);
- __gmpz_clear(__gen_e_acsl_size_4);
}
/*@ assert \block_length(&ZERO) ≡ 0; */
{
- unsigned long __gen_e_acsl_block_length_47;
- mpz_t __gen_e_acsl_block_length_48;
- mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq_19;
- __gen_e_acsl_block_length_47 = __e_acsl_block_length((void *)(& ZERO));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_48,
- __gen_e_acsl_block_length_47);
- __gmpz_init_set_si(__gen_e_acsl_,(long)0);
- __gen_e_acsl_eq_19 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_48),
- (__mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq_19 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_24;
+ __gen_e_acsl_block_length_24 = __e_acsl_block_length((void *)(& ZERO));
+ __e_acsl_assert(__gen_e_acsl_block_length_24 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(&ZERO) == 0",60);
- __gmpz_clear(__gen_e_acsl_block_length_48);
- __gmpz_clear(__gen_e_acsl_);
}
/*@ assert \block_length(&zero) ≡ 0; */
{
- unsigned long __gen_e_acsl_block_length_49;
- mpz_t __gen_e_acsl_block_length_50;
- mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq_20;
- __gen_e_acsl_block_length_49 = __e_acsl_block_length((void *)(& zero));
- __gmpz_init_set_ui(__gen_e_acsl_block_length_50,
- __gen_e_acsl_block_length_49);
- __gmpz_init_set_si(__gen_e_acsl__2,(long)0);
- __gen_e_acsl_eq_20 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_50),
- (__mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_eq_20 == 0,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_25;
+ __gen_e_acsl_block_length_25 = __e_acsl_block_length((void *)(& zero));
+ __e_acsl_assert(__gen_e_acsl_block_length_25 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(&zero) == 0",61);
- __gmpz_clear(__gen_e_acsl_block_length_50);
- __gmpz_clear(__gen_e_acsl__2);
}
__retres = 0;
__e_acsl_delete_block((void *)(& ZERO));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
index 5887eacd773..5be3ab147a5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
@@ -26,13 +26,15 @@ FRAMAC_SHARE/libc/stdlib.h:213:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:213:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index c8caafe3a83..8ea825d52a8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -5,13 +5,15 @@ tests/e-acsl-runtime/vector.c:28:[e-acsl] warning: E-ACSL construct `complete be
Ignoring annotation.
tests/e-acsl-runtime/vector.c:28:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
index bbd8afb45e9..5b573d17ea2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
@@ -15,6 +15,7 @@
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
+[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_neg
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
index 778c9c3e56a..10820363da0 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
@@ -41,7 +41,7 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_le;
__gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
__gen_e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_3),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_le <= 0,(char *)"Assertion",(char *)"main",
@@ -55,7 +55,7 @@ int main(void)
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_ge;
__gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init_set_si(__gen_e_acsl__2,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
__gen_e_acsl_ge = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_3),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_ge >= 0,(char *)"Assertion",(char *)"main",
@@ -72,8 +72,8 @@ int main(void)
mpz_t __gen_e_acsl__3;
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_lt_2;
- __gmpz_init_set_si(__gen_e_acsl__3,(long)5);
- __gmpz_init_set_si(__gen_e_acsl__4,(long)18);
+ __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)5);
+ __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)18);
__gen_e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__3),
(__mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_lt_2 < 0,(char *)"Assertion",(char *)"main",
@@ -86,8 +86,8 @@ int main(void)
mpz_t __gen_e_acsl__5;
mpz_t __gen_e_acsl__6;
int __gen_e_acsl_gt_2;
- __gmpz_init_set_si(__gen_e_acsl__5,(long)32);
- __gmpz_init_set_si(__gen_e_acsl__6,(long)3);
+ __gmpz_init_set_ui(__gen_e_acsl__5,(unsigned long)32);
+ __gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)3);
__gen_e_acsl_gt_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__5),
(__mpz_struct const *)(__gen_e_acsl__6));
__e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
@@ -100,8 +100,8 @@ int main(void)
mpz_t __gen_e_acsl__7;
mpz_t __gen_e_acsl__8;
int __gen_e_acsl_le_2;
- __gmpz_init_set_si(__gen_e_acsl__7,(long)12);
- __gmpz_init_set_si(__gen_e_acsl__8,(long)13);
+ __gmpz_init_set_ui(__gen_e_acsl__7,(unsigned long)12);
+ __gmpz_init_set_ui(__gen_e_acsl__8,(unsigned long)13);
__gen_e_acsl_le_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__7),
(__mpz_struct const *)(__gen_e_acsl__8));
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,(char *)"Assertion",
@@ -114,8 +114,8 @@ int main(void)
mpz_t __gen_e_acsl__9;
mpz_t __gen_e_acsl__10;
int __gen_e_acsl_ge_2;
- __gmpz_init_set_si(__gen_e_acsl__9,(long)123);
- __gmpz_init_set_si(__gen_e_acsl__10,(long)12);
+ __gmpz_init_set_ui(__gen_e_acsl__9,(unsigned long)123);
+ __gmpz_init_set_ui(__gen_e_acsl__10,(unsigned long)12);
__gen_e_acsl_ge_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__9),
(__mpz_struct const *)(__gen_e_acsl__10));
__e_acsl_assert(__gen_e_acsl_ge_2 >= 0,(char *)"Assertion",
@@ -127,7 +127,7 @@ int main(void)
{
mpz_t __gen_e_acsl__11;
int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl__11,(long)0xff);
+ __gmpz_init_set_ui(__gen_e_acsl__11,(unsigned long)0xff);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__11),
(__mpz_struct const *)(__gen_e_acsl__11));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
@@ -139,8 +139,8 @@ int main(void)
mpz_t __gen_e_acsl__12;
mpz_t __gen_e_acsl__13;
int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl__12,(long)1);
- __gmpz_init_set_si(__gen_e_acsl__13,(long)2);
+ __gmpz_init_set_ui(__gen_e_acsl__12,(unsigned long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__13,(unsigned long)2);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__12),
(__mpz_struct const *)(__gen_e_acsl__13));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
@@ -154,10 +154,10 @@ int main(void)
mpz_t __gen_e_acsl_neg;
mpz_t __gen_e_acsl__15;
int __gen_e_acsl_lt_3;
- __gmpz_init_set_si(__gen_e_acsl__14,(long)5);
+ __gmpz_init_set_ui(__gen_e_acsl__14,(unsigned long)5);
__gmpz_init(__gen_e_acsl_neg);
__gmpz_neg(__gen_e_acsl_neg,(__mpz_struct const *)(__gen_e_acsl__14));
- __gmpz_init_set_si(__gen_e_acsl__15,(long)18);
+ __gmpz_init_set_ui(__gen_e_acsl__15,(unsigned long)18);
__gen_e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg),
(__mpz_struct const *)(__gen_e_acsl__15));
__e_acsl_assert(__gen_e_acsl_lt_3 < 0,(char *)"Assertion",(char *)"main",
@@ -172,8 +172,8 @@ int main(void)
mpz_t __gen_e_acsl__17;
mpz_t __gen_e_acsl_neg_2;
int __gen_e_acsl_gt_3;
- __gmpz_init_set_si(__gen_e_acsl__16,(long)32);
- __gmpz_init_set_si(__gen_e_acsl__17,(long)3);
+ __gmpz_init_set_ui(__gen_e_acsl__16,(unsigned long)32);
+ __gmpz_init_set_ui(__gen_e_acsl__17,(unsigned long)3);
__gmpz_init(__gen_e_acsl_neg_2);
__gmpz_neg(__gen_e_acsl_neg_2,(__mpz_struct const *)(__gen_e_acsl__17));
__gen_e_acsl_gt_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__16),
@@ -190,10 +190,10 @@ int main(void)
mpz_t __gen_e_acsl_neg_3;
mpz_t __gen_e_acsl__19;
int __gen_e_acsl_le_3;
- __gmpz_init_set_si(__gen_e_acsl__18,(long)12);
+ __gmpz_init_set_ui(__gen_e_acsl__18,(unsigned long)12);
__gmpz_init(__gen_e_acsl_neg_3);
__gmpz_neg(__gen_e_acsl_neg_3,(__mpz_struct const *)(__gen_e_acsl__18));
- __gmpz_init_set_si(__gen_e_acsl__19,(long)13);
+ __gmpz_init_set_ui(__gen_e_acsl__19,(unsigned long)13);
__gen_e_acsl_le_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_3),
(__mpz_struct const *)(__gen_e_acsl__19));
__e_acsl_assert(__gen_e_acsl_le_3 <= 0,(char *)"Assertion",
@@ -208,8 +208,8 @@ int main(void)
mpz_t __gen_e_acsl__21;
mpz_t __gen_e_acsl_neg_4;
int __gen_e_acsl_ge_3;
- __gmpz_init_set_si(__gen_e_acsl__20,(long)123);
- __gmpz_init_set_si(__gen_e_acsl__21,(long)12);
+ __gmpz_init_set_ui(__gen_e_acsl__20,(unsigned long)123);
+ __gmpz_init_set_ui(__gen_e_acsl__21,(unsigned long)12);
__gmpz_init(__gen_e_acsl_neg_4);
__gmpz_neg(__gen_e_acsl_neg_4,(__mpz_struct const *)(__gen_e_acsl__21));
__gen_e_acsl_ge_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__20),
@@ -225,7 +225,7 @@ int main(void)
mpz_t __gen_e_acsl__22;
mpz_t __gen_e_acsl_neg_5;
int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__22,(long)0xff);
+ __gmpz_init_set_ui(__gen_e_acsl__22,(unsigned long)0xff);
__gmpz_init(__gen_e_acsl_neg_5);
__gmpz_neg(__gen_e_acsl_neg_5,(__mpz_struct const *)(__gen_e_acsl__22));
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_5),
@@ -241,8 +241,8 @@ int main(void)
mpz_t __gen_e_acsl__24;
mpz_t __gen_e_acsl_neg_6;
int __gen_e_acsl_ne_2;
- __gmpz_init_set_si(__gen_e_acsl__23,(long)1);
- __gmpz_init_set_si(__gen_e_acsl__24,(long)2);
+ __gmpz_init_set_ui(__gen_e_acsl__23,(unsigned long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__24,(unsigned long)2);
__gmpz_init(__gen_e_acsl_neg_6);
__gmpz_neg(__gen_e_acsl_neg_6,(__mpz_struct const *)(__gen_e_acsl__24));
__gen_e_acsl_ne_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__23),
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
index 28047909daa..74ca167908e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
@@ -7,7 +7,7 @@ int main(void)
{
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
@@ -21,8 +21,8 @@ int main(void)
mpz_t __gen_e_acsl__2;
mpz_t __gen_e_acsl__3;
int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl__2,(long)0);
- __gmpz_init_set_si(__gen_e_acsl__3,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)1);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__2),
(__mpz_struct const *)(__gen_e_acsl__3));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
index 80d96913a91..78842be2f71 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
@@ -39,17 +39,17 @@ int main(void)
int __gen_e_acsl_mod_guard;
mpz_t __gen_e_acsl_mod;
unsigned long __gen_e_acsl__4;
- __gmpz_init_set_si(__gen_e_acsl_,(long)2);
+ __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)2);
__gmpz_init(__gen_e_acsl_x);
__gmpz_import(__gen_e_acsl_x,1UL,1,8UL,0,0UL,(void const *)(& x));
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,(__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl_x));
- __gmpz_init_set_si(__gen_e_acsl__2,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_mul),
(__mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gmpz_init_set_ui(__gen_e_acsl__3,0UL);
__gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mod);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
index d086ece432a..11dd13abee4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
@@ -39,17 +39,17 @@ int main(void)
int __gen_e_acsl_mod_guard;
mpz_t __gen_e_acsl_mod;
int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_,(long)2);
+ __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)2);
__gmpz_init(__gen_e_acsl_x);
__gmpz_import(__gen_e_acsl_x,1UL,1,8UL,0,0UL,(void const *)(& x));
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,(__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl_x));
- __gmpz_init_set_si(__gen_e_acsl__2,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_mul),
(__mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gmpz_init_set_ui(__gen_e_acsl__3,0UL);
__gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mod);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
index 8ee1e05a971..f1e22043fb6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
@@ -10,7 +10,7 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set_ui(__gen_e_acsl_,0UL);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
@@ -25,7 +25,7 @@ int main(void)
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_ne;
__gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init_set_ui(__gen_e_acsl__2,0UL);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
index b2401c11ed4..a27112ee0f4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
@@ -10,11 +10,10 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_size ∈ [--..--]
-[value] using specification for function __gmpz_init_set_si
+[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init_set_str
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 2aa07b37357..427396a3100 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -16,9 +16,9 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
[value] user error: Recursive call on an unspecified function. Using potentially invalid
inferred assigns 'assigns \result \from x, n;'
[value] using specification for function my_pow
-tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
-tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
-[value] using specification for function __gmpz_init_set_si
+tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
+tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
+[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_import
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: precondition got status unknown.
@@ -29,7 +29,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: pre
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
[value] using specification for function __gmpz_get_ui
-tests/gmp/longlong.i:17:[value] warning: pointer comparison.
- assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
+tests/gmp/longlong.i:17:[kernel] warning: pointer comparison.
+ assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
[value] using specification for function __gmpz_clear
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index cb8aca989bc..e24d41cefb7 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -16,9 +16,9 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
[value] user error: Recursive call on an unspecified function. Using potentially invalid
inferred assigns 'assigns \result \from x, n;'
[value] using specification for function my_pow
-tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
-tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
-[value] using specification for function __gmpz_init_set_si
+tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
+tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
+[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_import
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: precondition got status unknown.
@@ -28,7 +28,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: pre
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
-tests/gmp/longlong.i:17:[value] warning: pointer comparison.
- assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0);
+tests/gmp/longlong.i:17:[kernel] warning: pointer comparison.
+ assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0);
[value] using specification for function __gmpz_clear
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
index 35b4ab588d7..97d849b1076 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
@@ -11,6 +11,7 @@
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_size ∈ [--..--]
[value] using specification for function __gmpz_init_set_si
+[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 78485b2682e..e108cf1e259 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -300,7 +300,7 @@ and context_insensitive_term_to_exp kf env t =
let zero = Logic_const.tinteger 0 in
let e, env =
comparison_to_exp
- kf ~loc ~name:"not" env New_typing.Gmp Eq t zero (Some t)
+ kf ~loc ~name:"not" env New_typing.gmp Eq t zero (Some t)
in
e, env, false, ""
else begin
@@ -346,7 +346,7 @@ and context_insensitive_term_to_exp kf env t =
(* do not generate [e2] from [t2] twice *)
let guard, env =
let name = name_of_binop bop ^ "_guard" in
- comparison_to_exp ~loc kf env New_typing.Gmp ~e1:e2 ~name Eq t2 zero t
+ comparison_to_exp ~loc kf env New_typing.gmp ~e1:e2 ~name Eq t2 zero t
in
let mk_stmts _v e =
assert (Gmpz.is_t ty);
@@ -798,13 +798,13 @@ exception No_simple_translation of term
(* This function is used by plug-in [Cfp]. *)
let term_to_exp typ t =
let ctx = match typ with
- | None -> New_typing.C_type IInt (* useless, but required *)
+ | None -> New_typing.c_int (* useless, but required *)
| Some typ ->
- if Gmpz.is_t typ then New_typing.Gmp
+ if Gmpz.is_t typ then New_typing.gmp
else
match typ with
- | TInt(i, _) -> New_typing.C_type i
- | _ -> New_typing.C_type IInt (* useless, but required *)
+ | TInt(ik, _) -> New_typing.ikind ik
+ | _ -> New_typing.c_int (* useless, but required *)
in
New_typing.type_term ~ctx t;
let env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
--
GitLab