From 144f42bbad75a3b315d6eb62dd983f254a8b9365 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 12 May 2011 14:42:20 +0000
Subject: [PATCH] [e-acsl] minor code+tests improvements
---
.../tests/e-acsl-runtime/integer_constant.i | 2 +-
.../oracle/gen_integer_constant.c | 4 ++--
.../oracle/integer_constant.res.oracle | 4 ++--
src/plugins/e-acsl/visit.ml | 23 +++++++++++--------
4 files changed, 18 insertions(+), 15 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
index ed63e1f988a..ecbe431cb85 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
@@ -7,7 +7,7 @@ int main(void) {
int x;
/*@ assert 0 == 0; */ x = 0;
/*@ assert 0 != 1; */
- /*@ assert 0xfffffffffffffff == 0xfffffffffffffff; */
+ /*@ assert 1152921504606846975 == 0xfffffffffffffff; */
/* /\*@ assert 0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff; *\/ */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index dc3fe0bba1c..2f8d4ef60a3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -593,14 +593,14 @@ int main(void)
__gmpz_clear((__mpz_struct *)(e_acsl_5));
}
- /*@ assert 0xfffffffffffffff ≡ 0xfffffffffffffff; */ ;
+ /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */ ;
{ mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
__gmpz_init_set_str((__mpz_struct *)(e_acsl_7),"1152921504606846975",10);
__gmpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
(__mpz_struct const *)(e_acsl_8));
if (! (e_acsl_9 == 0)) {
- e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
+ e_acsl_fail((char *)"(1152921504606846975 == 0xfffffffffffffff)");
} __gmpz_clear((__mpz_struct *)(e_acsl_7));
__gmpz_clear((__mpz_struct *)(e_acsl_8));
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index ea258f13f9d..a5656a25923 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -175,14 +175,14 @@ int main(void)
mpz_clear((__mpz_struct *)(e_acsl_5));
}
- /*@ assert 0xfffffffffffffff ≡ 0xfffffffffffffff; */ ;
+ /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */ ;
{ mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
mpz_init_set_str((__mpz_struct *)(e_acsl_7),"1152921504606846975",10);
mpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
e_acsl_9 = mpz_cmp((__mpz_struct const *)(e_acsl_7),
(__mpz_struct const *)(e_acsl_8));
if (! (e_acsl_9 == 0)) {
- e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
+ e_acsl_fail((char *)"(1152921504606846975 == 0xfffffffffffffff)");
} mpz_clear((__mpz_struct *)(e_acsl_7));
mpz_clear((__mpz_struct *)(e_acsl_8));
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 4677d7dc5b5..71b84af223a 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -230,14 +230,17 @@ end
(* ************************************************************************** *)
let constant_to_exp ?(loc=Location.unknown) = function
- | CInt64(n, k, s) ->
- (match k with
- | IBool | IChar | IUChar | IUInt | IUShort | IULong
- | ISChar | IShort | IInt | ILong ->
- kinteger64_repr ?loc k n s
- | ILongLong | IULongLong ->
- mkString ?loc (Int64.to_string n))
- | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c -> new_exp ?loc (Const c)
+ | CInt64(n,
+ (IBool | IChar | IUChar | IUInt | IUShort | IULong
+ | ISChar | IShort | IInt | ILong as k),
+ s) ->
+ kinteger64_repr ?loc k n s
+ | CInt64(n, (ILongLong | IULongLong), _s) ->
+ (* cannot use the string [s] if any since we do not know the base in which
+ it is written. Such a base is required by GMP. *)
+ mkString ?loc (Int64.to_string n)
+ | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c ->
+ new_exp ?loc (Const c)
let tlval_to_lval = function
| TVar { lv_origin = Some v }, TNoOffset -> Var v, NoOffset
@@ -536,7 +539,8 @@ class e_acsl_visitor prj generate = object (self)
stmt
Env.empty
in
- if Env.is_empty env then DoChildren
+ if Env.is_empty env then
+ DoChildren
else begin
assert generate;
let mk_block stmt =
@@ -548,7 +552,6 @@ class e_acsl_visitor prj generate = object (self)
initializer Env.register_actions_queue self#get_filling_actions
-
end
let do_visit ?(prj=Project.current ()) generate =
--
GitLab