From 4b91b5f064499cdc7a4330c59b2ed9c49be2b862 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 23 Nov 2011 18:00:00 +0000
Subject: [PATCH] [e-acsl] \result
---
src/plugins/e-acsl/TODO | 3 +-
src/plugins/e-acsl/env.ml | 8 +-
.../tests/e-acsl-runtime/oracle/gen_result.c | 694 ++++++++++++++++++
.../e-acsl-runtime/oracle/result.err.oracle | 0
.../e-acsl-runtime/oracle/result.res.oracle | 217 ++++++
.../e-acsl/tests/e-acsl-runtime/result.i | 31 +
src/plugins/e-acsl/visit.ml | 46 +-
7 files changed, 977 insertions(+), 22 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/result.i
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 07935b4b05f..7a4303f1380 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -1,11 +1,11 @@
à traiter avant la 1ère release:
- quantifications sans exentension de syntaxe
-- \return
########
# CODE #
########
+- mixed assumes and ensures
- function contracts for functions only declared
==> le noyau génère un "assigns \nothing" pour ces fonctions...
ce assign n'est de toute façon pas gérer
@@ -25,6 +25,7 @@
# KNOWN BUGS #
##############
- \at incorrect si StmtLabel faisant référence au stmt courant (voir test at.i)
+- incorrect d'utiliser un \old dans le post-state si pre-state == post-state
#########
# TESTS #
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index f36034d506b..c60851c3471 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -148,13 +148,17 @@ let new_var ?(global=false) env t ty mk_stmts =
let local_env, _ = top env in
if global then
(* do not use memoisation here: it is incorrect for terms corresponding to
- impure expressions *)
+ impure expressions
+ [JS 2011/11/23] actually it is correct now since globals are only use for
+ \at *)
do_new_var ~global env t ty mk_stmts
else
try
match t with
| None -> raise No_term
- | Some t -> Term.Map.find t local_env.mpz_tbl.new_exps, env
+ | Some t ->
+ Options.feedback "memoized %a" Term.pretty t;
+ Term.Map.find t local_env.mpz_tbl.new_exps, env
with Not_found | No_term ->
do_new_var ~global env t ty mk_stmts
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
new file mode 100644
index 00000000000..46b82c22313
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
@@ -0,0 +1,694 @@
+/* Generated by Frama-C */
+typedef unsigned long size_t;
+typedef unsigned long mp_limb_t;
+typedef unsigned long mp_bitcnt_t;
+struct __anonstruct___mpz_struct_6 {
+ int _mp_alloc ;
+ int _mp_size ;
+ mp_limb_t *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_6 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+typedef mp_limb_t *mp_ptr;
+typedef mp_limb_t const *mp_srcptr;
+typedef long mp_size_t;
+struct __anonstruct___mpq_struct_7 {
+ __mpz_struct _mp_num ;
+ __mpz_struct _mp_den ;
+};
+typedef struct __anonstruct___mpq_struct_7 __mpq_struct;
+typedef __mpz_struct const *mpz_srcptr;
+typedef __mpz_struct *mpz_ptr;
+typedef __mpq_struct const *mpq_srcptr;
+typedef __mpq_struct *mpq_ptr;
+/* compiler builtin:
+ long __builtin_expect(long, long); */
+/*@ assigns \nothing; */
+extern int printf(char const * __restrict __format , ...);
+__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+/*@ requires \valid(z);
+ assigns \nothing; */
+extern long __gmpz_get_si(__mpz_struct const * /*[1]*/ z) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n) __attribute__((
+__pure__));
+/*@ ensures \valid(\old(x));
+ assigns *x; */
+extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+ assigns *z;
+ assigns *z \from n; */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
+__pure__));
+__inline static mp_bitcnt_t __gmpz_popcount(mpz_srcptr __gmp_u) __attribute__((
+__pure__));
+extern void __gmpz_set(mpz_ptr, mpz_srcptr);
+__inline static void __gmpz_set_q(mpz_ptr __gmp_w, mpq_srcptr __gmp_u);
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+__inline static void __gmpq_abs(mpq_ptr __gmp_w, mpq_srcptr __gmp_u);
+__inline static void __gmpq_neg(mpq_ptr __gmp_w, mpq_srcptr __gmp_u);
+extern void __gmpq_set(mpq_ptr, mpq_srcptr);
+__inline static mp_limb_t __gmpn_add(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize);
+__inline static mp_limb_t __gmpn_add_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n);
+extern mp_limb_t __gmpn_add_n(mp_ptr, mp_srcptr, mp_srcptr, mp_size_t);
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size) __attribute__((__pure__));
+__inline static mp_limb_t __gmpn_neg(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
+ mp_size_t __gmp_n);
+extern int __gmpn_perfect_square_p(mp_srcptr, mp_size_t) __attribute__((
+__pure__));
+extern mp_bitcnt_t __gmpn_popcount(mp_srcptr, mp_size_t) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpn_sub(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize);
+__inline static mp_limb_t __gmpn_sub_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n);
+extern mp_limb_t __gmpn_sub_n(mp_ptr, mp_srcptr, mp_srcptr, mp_size_t);
+__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpz_set(__gmp_w,__gmp_u); }
+ if (__gmp_w->_mp_size >= 0) { __gmp_w->_mp_size = __gmp_w->_mp_size; }
+ else { __gmp_w->_mp_size = - __gmp_w->_mp_size; }
+ return;
+}
+
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (long)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= (mp_limb_t)(~ ((unsigned int)0))) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (long)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= ~ ((unsigned long)0)) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (long)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= (mp_limb_t)((unsigned short)(~ 0))) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+/*@ requires \valid(z);
+ assigns \nothing; */
+__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z)
+{
+ mp_ptr __gmp_p;
+ mp_size_t __gmp_n;
+ mp_limb_t __gmp_l;
+ mp_limb_t tmp;
+ __gmp_p = z->_mp_d;
+ __gmp_n = (long)z->_mp_size;
+ __gmp_l = *(__gmp_p + 0);
+ if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
+ else { tmp = (unsigned long)0; }
+ return (tmp);
+}
+
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n)
+{
+ mp_limb_t __gmp_result;
+ long tmp_1;
+ int tmp_0;
+ __gmp_result = (unsigned long)0;
+ { /*undefined sequence*/
+ if (__gmp_n >= (mp_size_t)0) {
+ int tmp;
+ { /*undefined sequence*/
+ if (__gmp_z->_mp_size >= 0) { tmp = __gmp_z->_mp_size; }
+ else { tmp = - __gmp_z->_mp_size; }
+ ;
+ }
+ if (__gmp_n < (mp_size_t)tmp) { tmp_0 = 1; }
+ else { tmp_0 = 0; }
+ }
+ else { tmp_0 = 0; }
+ tmp_1 = __builtin_expect((long)(tmp_0 != 0),(long)1);
+ }
+ if (tmp_1) { __gmp_result = *(__gmp_z->_mp_d + __gmp_n); }
+ return (__gmp_result);
+}
+
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns *z1; */
+__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2)
+{
+ if (z1 != z2) { __gmpz_set(z1,z2); }
+ z1->_mp_size = - z1->_mp_size;
+ return;
+}
+
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
+__pure__));
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a)
+{
+ mp_size_t __gmp_asize;
+ int __gmp_result;
+ long tmp;
+ __gmp_asize = (long)__gmp_a->_mp_size;
+ __gmp_result = __gmp_asize >= (mp_size_t)0;
+ tmp = __builtin_expect((long)((__gmp_asize > (mp_size_t)0) != 0),(long)1);
+ if (tmp) {
+ __gmp_result = __gmpn_perfect_square_p((mp_limb_t const *)__gmp_a->_mp_d,
+ __gmp_asize);
+ }
+ return (__gmp_result);
+}
+
+__inline static mp_bitcnt_t __gmpz_popcount(mpz_srcptr __gmp_u) __attribute__((
+__pure__));
+__inline static mp_bitcnt_t __gmpz_popcount(mpz_srcptr __gmp_u)
+{
+ mp_size_t __gmp_usize;
+ mp_bitcnt_t __gmp_result;
+ long tmp;
+ __gmp_usize = (long)__gmp_u->_mp_size;
+ if (__gmp_usize < (mp_size_t)0) { __gmp_result = ~ ((unsigned long)0); }
+ else { __gmp_result = (unsigned long)0; }
+ tmp = __builtin_expect((long)((__gmp_usize > (mp_size_t)0) != 0),(long)1);
+ if (tmp) {
+ __gmp_result = __gmpn_popcount((mp_limb_t const *)__gmp_u->_mp_d,
+ __gmp_usize);
+ }
+ return (__gmp_result);
+}
+
+__inline static void __gmpz_set_q(mpz_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ __gmpz_tdiv_q(__gmp_w,& __gmp_u->_mp_num,& __gmp_u->_mp_den);
+ return;
+}
+
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z)
+{
+ size_t __retres;
+ int tmp;
+ if (__gmp_z->_mp_size >= 0) { tmp = __gmp_z->_mp_size; }
+ else { tmp = - __gmp_z->_mp_size; }
+ __retres = (unsigned long)tmp;
+ return (__retres);
+}
+
+__inline static void __gmpq_abs(mpq_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpq_set(__gmp_w,__gmp_u); }
+ if (__gmp_w->_mp_num._mp_size >= 0) {
+ __gmp_w->_mp_num._mp_size = __gmp_w->_mp_num._mp_size;
+ }
+ else { __gmp_w->_mp_num._mp_size = - __gmp_w->_mp_num._mp_size; }
+ return;
+}
+
+__inline static void __gmpq_neg(mpq_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpq_set(__gmp_w,__gmp_u); }
+ __gmp_w->_mp_num._mp_size = - __gmp_w->_mp_num._mp_size;
+ return;
+}
+
+__inline static mp_limb_t __gmpn_add(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ {
+ mp_size_t __gmp_i;
+ mp_limb_t __gmp_x;
+ __gmp_i = __gmp_ysize;
+ if (__gmp_i != (mp_size_t)0) {
+ mp_limb_t tmp_1;
+ tmp_1 = __gmpn_add_n(__gmp_wp,__gmp_xp,__gmp_yp,__gmp_i);
+ if (tmp_1) {
+ while (1) {
+ mp_size_t tmp;
+ mp_limb_t tmp_0;
+ if (__gmp_i >= __gmp_xsize) {
+ __gmp_c = (unsigned long)1;
+ goto __gmp_done;
+ }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ { /*undefined sequence*/
+ tmp = __gmp_i;
+ __gmp_i += (mp_size_t)1;
+ tmp_0 = (__gmp_x + (mp_limb_t)1) & (~ ((unsigned long)0) >> 0);
+ *(__gmp_wp + tmp) = tmp_0;
+ }
+ if (! (tmp_0 == (mp_limb_t)0)) { break; }
+ }
+ }
+ }
+ if (__gmp_wp != __gmp_xp) {
+ while (1) {
+ {
+ mp_size_t __gmp_j;
+ __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_xsize) {
+ *(__gmp_wp + __gmp_j) = *(__gmp_xp + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ __gmp_done: ;
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_add_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ {
+ mp_size_t __gmp_i;
+ mp_limb_t __gmp_x;
+ mp_limb_t __gmp_r;
+ __gmp_x = *(__gmp_src + 0);
+ __gmp_r = __gmp_x + __gmp_n;
+ *(__gmp_dst + 0) = __gmp_r;
+ if (__gmp_r < __gmp_n) {
+ __gmp_c = (unsigned long)1;
+ __gmp_i = (long)1;
+ while (__gmp_i < __gmp_size) {
+ __gmp_x = *(__gmp_src + __gmp_i);
+ __gmp_r = __gmp_x + (mp_limb_t)1;
+ *(__gmp_dst + __gmp_i) = __gmp_r;
+ __gmp_i += (mp_size_t)1;
+ if (! (__gmp_r < (mp_limb_t)1)) {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ {
+ mp_size_t __gmp_j;
+ __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_size) {
+ *(__gmp_dst + __gmp_j) = *(__gmp_src + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ break;
+ }
+ }
+ }
+ else {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ {
+ mp_size_t __gmp_j_0;
+ __gmp_j_0 = (long)1;
+ while (__gmp_j_0 < __gmp_size) {
+ *(__gmp_dst + __gmp_j_0) = *(__gmp_src + __gmp_j_0);
+ __gmp_j_0 += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ }
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size) __attribute__((__pure__));
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size)
+{
+ int __gmp_result;
+ while (1) {
+ {
+ mp_size_t __gmp_i;
+ mp_limb_t __gmp_x;
+ mp_limb_t __gmp_y;
+ __gmp_result = 0;
+ __gmp_i = __gmp_size;
+ while (1) {
+ __gmp_i -= (mp_size_t)1;
+ if (! (__gmp_i >= (mp_size_t)0)) { break; }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ __gmp_y = *(__gmp_yp + __gmp_i);
+ if (__gmp_x != __gmp_y) {
+ if (__gmp_x > __gmp_y) { __gmp_result = 1; }
+ else { __gmp_result = -1; }
+ break;
+ }
+ }
+ }
+
+ break;
+ }
+ return (__gmp_result);
+}
+
+__inline static mp_limb_t __gmpn_sub(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ {
+ mp_size_t __gmp_i;
+ mp_limb_t __gmp_x;
+ __gmp_i = __gmp_ysize;
+ if (__gmp_i != (mp_size_t)0) {
+ mp_limb_t tmp_0;
+ tmp_0 = __gmpn_sub_n(__gmp_wp,__gmp_xp,__gmp_yp,__gmp_i);
+ if (tmp_0) {
+ while (1) {
+ mp_size_t tmp;
+ if (__gmp_i >= __gmp_xsize) {
+ __gmp_c = (unsigned long)1;
+ goto __gmp_done;
+ }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ { /*undefined sequence*/
+ tmp = __gmp_i;
+ __gmp_i += (mp_size_t)1;
+ *(__gmp_wp + tmp) = (__gmp_x - (mp_limb_t)1) & (~ ((unsigned long)0) >> 0);
+ }
+ if (! (__gmp_x == (mp_limb_t)0)) { break; }
+ }
+ }
+ }
+ if (__gmp_wp != __gmp_xp) {
+ while (1) {
+ {
+ mp_size_t __gmp_j;
+ __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_xsize) {
+ *(__gmp_wp + __gmp_j) = *(__gmp_xp + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ __gmp_done: ;
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_sub_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ {
+ mp_size_t __gmp_i;
+ mp_limb_t __gmp_x;
+ mp_limb_t __gmp_r;
+ __gmp_x = *(__gmp_src + 0);
+ __gmp_r = __gmp_x - __gmp_n;
+ *(__gmp_dst + 0) = __gmp_r;
+ if (__gmp_x < __gmp_n) {
+ __gmp_c = (unsigned long)1;
+ __gmp_i = (long)1;
+ while (__gmp_i < __gmp_size) {
+ __gmp_x = *(__gmp_src + __gmp_i);
+ __gmp_r = __gmp_x - (mp_limb_t)1;
+ *(__gmp_dst + __gmp_i) = __gmp_r;
+ __gmp_i += (mp_size_t)1;
+ if (! (__gmp_x < (mp_limb_t)1)) {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ {
+ mp_size_t __gmp_j;
+ __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_size) {
+ *(__gmp_dst + __gmp_j) = *(__gmp_src + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ break;
+ }
+ }
+ }
+ else {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ {
+ mp_size_t __gmp_j_0;
+ __gmp_j_0 = (long)1;
+ while (__gmp_j_0 < __gmp_size) {
+ *(__gmp_dst + __gmp_j_0) = *(__gmp_src + __gmp_j_0);
+ __gmp_j_0 += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ }
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_neg(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
+ mp_size_t __gmp_n)
+{
+ mp_limb_t __gmp_ul;
+ mp_limb_t __gmp_cy;
+ __gmp_cy = (unsigned long)0;
+ while (1) {
+ {
+ mp_srcptr tmp;
+ mp_ptr tmp_0;
+ { /*undefined sequence*/ tmp = __gmp_up; __gmp_up ++; __gmp_ul = *tmp;
+ }
+ { /*undefined sequence*/
+ tmp_0 = __gmp_rp;
+ __gmp_rp ++;
+ *tmp_0 = - __gmp_ul - __gmp_cy;
+ }
+ __gmp_cy |= (unsigned long)(__gmp_ul != (mp_limb_t)0);
+ }
+
+ __gmp_n -= (mp_size_t)1;
+ if (! (__gmp_n != (mp_size_t)0)) { break; }
+ }
+ return (__gmp_cy);
+}
+
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+void e_acsl_fail(char *msg)
+{
+ printf("%s\n",msg);
+ exit(1);
+ return;
+}
+
+/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
+int f(int x)
+{
+ int e_acsl_1;
+ int e_acsl_3;
+ e_acsl_3 = x;
+ e_acsl_1 = x;
+ x = 0;
+ {
+ mpz_t e_acsl_2;
+ mpz_t e_acsl_4;
+ int e_acsl_5;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)e_acsl_1);
+ __gmpz_init((__mpz_struct *)(e_acsl_4));
+ __gmpz_sub((__mpz_struct *)(e_acsl_4),(__mpz_struct const *)(e_acsl_2),
+ (__mpz_struct const *)(e_acsl_2));
+ e_acsl_5 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_4));
+ if (! (x == e_acsl_5)) {
+ e_acsl_fail((char *)"(\\result == (int)(\\old(x)-\\old(x)))");
+ }
+ __gmpz_clear((__mpz_struct *)(e_acsl_2));
+ __gmpz_clear((__mpz_struct *)(e_acsl_4));
+ return (x);
+ }
+
+}
+
+int Y = 1;
+/*@ ensures \result ≡ Y; */
+int g(int x)
+{
+ if (! (x == Y)) { e_acsl_fail((char *)"(\\result == Y)"); }
+ return (x);
+}
+
+/*@ ensures \result ≡ 0; */
+int h(void)
+{
+ int __retres;
+ __retres = 0;
+ {
+ mpz_t e_acsl_1;
+ mpz_t e_acsl_2;
+ int e_acsl_3;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)__retres);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+ e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_2));
+ if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(\\result == 0)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ __gmpz_clear((__mpz_struct *)(e_acsl_2));
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ f(1);
+ g(Y);
+ h();
+ __retres = 0;
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
new file mode 100644
index 00000000000..6728e58d32b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -0,0 +1,217 @@
+[e-acsl] memoized \old(x)
+[e-acsl] memoized \old(x)
+[e-acsl] memoized \old(x)-\old(x)
+tests/e-acsl-runtime/result.i:7:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+[e-acsl] memoized \result
+[e-acsl] memoized 0
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ Y ∈ {1}
+[value] computing for function f <- main.
+ Called from PROJECT_FILE.i:188.
+[value] computing for function mpz_init_set_si <- f <- main.
+ Called from PROJECT_FILE.i:143.
+PROJECT_FILE.i:33:[value] Function mpz_init_set_si: postcondition got status valid.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <- f <- main.
+ Called from PROJECT_FILE.i:144.
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
+[value] Done for function mpz_init
+[value] computing for function mpz_sub <- f <- main.
+ Called from PROJECT_FILE.i:145.
+PROJECT_FILE.i:70:[value] Function mpz_sub: precondition got status valid.
+PROJECT_FILE.i:71:[value] Function mpz_sub: precondition got status valid.
+PROJECT_FILE.i:72:[value] Function mpz_sub: precondition got status valid.
+[value] Done for function mpz_sub
+[value] computing for function mpz_get_si <- f <- main.
+ Called from PROJECT_FILE.i:146.
+PROJECT_FILE.i:96:[value] Function mpz_get_si: precondition got status valid.
+[value] Done for function mpz_get_si
+[value] computing for function e_acsl_fail <- f <- main.
+ Called from PROJECT_FILE.i:148.
+[value] computing for function printf <- e_acsl_fail <- f <- main.
+ Called from PROJECT_FILE.i:129.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- f <- main.
+ Called from PROJECT_FILE.i:129.
+PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- f <- main.
+ Called from PROJECT_FILE.i:150.
+PROJECT_FILE.i:43:[value] Function mpz_clear: precondition got status valid.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- f <- main.
+ Called from PROJECT_FILE.i:151.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:131:[value] Function f: postcondition got status valid.
+[value] Recording results for f
+[value] Done for function f
+[value] computing for function g <- main.
+ Called from PROJECT_FILE.i:189.
+PROJECT_FILE.i:158:[value] Function g: postcondition got status valid.
+[value] Recording results for g
+[value] Done for function g
+[value] computing for function h <- main.
+ Called from PROJECT_FILE.i:190.
+[value] computing for function mpz_init_set_si <- h <- main.
+ Called from PROJECT_FILE.i:174.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- h <- main.
+ Called from PROJECT_FILE.i:175.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- h <- main.
+ Called from PROJECT_FILE.i:176.
+PROJECT_FILE.i:49:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:50:[value] Function mpz_cmp: precondition got status valid.
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <- h <- main.
+ Called from PROJECT_FILE.i:177.
+[value] computing for function printf <- e_acsl_fail <- h <- main.
+ Called from PROJECT_FILE.i:129.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- h <- main.
+ Called from PROJECT_FILE.i:129.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- h <- main.
+ Called from PROJECT_FILE.i:178.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- h <- main.
+ Called from PROJECT_FILE.i:179.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:165:[value] Function h: postcondition got status valid.
+[value] Recording results for h
+[value] Done for function h
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function g:
+[value] Values for function e_acsl_fail:
+ NON TERMINATING FUNCTION
+[value] Values for function f:
+ x ∈ {0}
+ e_acsl_1 ∈ {1}
+ e_acsl_3 ∈ {1}
+[value] Values for function h:
+ __retres ∈ {0}
+[value] Values for function main:
+ __retres ∈ {0}
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\old(x));
+ assigns *x; */
+extern void mpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+ assigns *z;
+ assigns *z \from n; */
+extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void mpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int mpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern void mpz_sub(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(z);
+ assigns \nothing; */
+extern long mpz_get_si(__mpz_struct const * /*[1]*/ z);
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+/*@ assigns \nothing; */
+extern int printf(char const * , ...);
+void e_acsl_fail(char *msg)
+{
+ printf("%s\n",msg);
+ exit(1);
+ return;
+}
+
+/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
+int f(int x)
+{
+ int e_acsl_1;
+ int e_acsl_3;
+ e_acsl_3 = x;
+ e_acsl_1 = x;
+ x = 0;
+ {
+ mpz_t e_acsl_2;
+ mpz_t e_acsl_4;
+ int e_acsl_5;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)e_acsl_1);
+ mpz_init((__mpz_struct *)(e_acsl_4));
+ mpz_sub((__mpz_struct *)(e_acsl_4),(__mpz_struct const *)(e_acsl_2),
+ (__mpz_struct const *)(e_acsl_2));
+ e_acsl_5 = (int)mpz_get_si((__mpz_struct const *)(e_acsl_4));
+ if (! (x == e_acsl_5)) {
+ e_acsl_fail((char *)"(\\result == (int)(\\old(x)-\\old(x)))");
+ }
+ mpz_clear((__mpz_struct *)(e_acsl_2));
+ mpz_clear((__mpz_struct *)(e_acsl_4));
+ return (x);
+ }
+
+}
+
+int Y = 1;
+/*@ ensures \result ≡ Y; */
+int g(int x)
+{
+ if (! (x == Y)) { e_acsl_fail((char *)"(\\result == Y)"); }
+ return (x);
+}
+
+/*@ ensures \result ≡ 0; */
+int h(void)
+{
+ int __retres;
+ __retres = 0;
+ {
+ mpz_t e_acsl_1;
+ mpz_t e_acsl_2;
+ int e_acsl_3;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)__retres);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+ e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_2));
+ if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(\\result == 0)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_1));
+ mpz_clear((__mpz_struct *)(e_acsl_2));
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ f(1);
+ g(Y);
+ h();
+ __retres = 0;
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
new file mode 100644
index 00000000000..b18c3c412ae
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
@@ -0,0 +1,31 @@
+/* run.config
+ COMMENT: \result
+ EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp
+*/
+
+// && ./tests/e-acsl-runtime/result/gen_result.out
+/*@ ensures \result == (int)(x - x); */
+int f(int x) {
+ x = 0;
+ return x; }
+
+int Y = 1;
+
+// does not work since it is converted into \result == \old(x) and,
+// in this particular case, the pre-state and the post-state are the same and
+// it does not work yet (related to issue in at.i).
+// /*@ ensures \result == x; */
+/*@ ensures \result == Y; */
+int g(int x) {
+ return x;
+}
+
+/*@ ensures \result == 0; */
+int h() { return 0; }
+
+int main(void) {
+ f(1);
+ g(Y);
+ h();
+ return 0;
+}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 84de17b01a6..1d852dd77cc 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -145,7 +145,16 @@ let constant_to_exp ?(loc=Location.unknown) = function
let rec thost_to_host env = function
| TVar { lv_origin = Some v } -> Var v, env
| TVar { lv_origin = None } -> Misc.not_yet "logic variable"
- | TResult _typ -> Misc.not_yet "\\result"
+ | TResult _typ ->
+ let vis = Env.get_visitor env in
+ let kf = Extlib.the vis#current_kf in
+ let stmt =
+ try Kernel_function.find_return kf
+ with Kernel_function.No_Statement -> assert false
+ in
+ (match stmt.skind with
+ | Return(Some { enode = Lval (lhost, NoOffset) }, _) -> lhost, env
+ | _ -> assert false)
| TMem t ->
let e, env = term_to_exp env (Ctype intType) t in
Options.warning ~source:(fst e.eloc) ~once:true
@@ -307,7 +316,7 @@ and context_insensitive_term_to_exp env t =
That is this variable which is the resulting expression.
ACSL typing rule ensures that the type of this variable is the same as
the one of [e]. *)
- let res, env =
+ let res, new_env =
Env.new_var ~global:true env
(Some t) (typeOf e)
(fun lv' e' ->
@@ -316,15 +325,16 @@ and context_insensitive_term_to_exp env t =
initialize it. *)
new_v := Some (lv', e'); [])
in
- let env_ref = ref env in
- (* visitor modifying in place the labeled statement in order to store [e] in
- the resulting variable at this location which is the only correct one. *)
+ let env_ref = ref new_env in
+ (* visitor modifying in place the labeled statement in order to store [e]
+ in the resulting variable at this location which is the only correct
+ one. *)
let o = object
inherit Visitor.frama_c_inplace
method vstmt_aux stmt =
let new_lv, new_e = Extlib.the !new_v in
- (* either a standard C affectation or an mpz one according to type of
- [e] *)
+ (* either a standard C affectation or an mpz one according to type of
+ [e] *)
let new_stmt =
if Mpz.is_t (typeOf new_e) then
Mpz.init_set new_e e
@@ -332,23 +342,21 @@ and context_insensitive_term_to_exp env t =
mkStmtOneInstr ~valid_sid:true
(Set((Var new_lv, NoOffset), e, Location.unknown))
in
- assert (!env_ref == env);
- (* generate the new block of code for the labeled statement and the
- corresponding environment *)
- let block, env =
- Env.pop_and_get env new_stmt ~global_clear:false Env.Middle
+ assert (!env_ref == new_env);
+ (* generate the new block of code for the labeled statement and the
+ corresponding environment *)
+ let block, new_env =
+ Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
in
let pre = match label with
| LogicLabel(_, s) when s = "Here" || s = "Post" -> true
| StmtLabel _ | LogicLabel _ -> false
in
- env_ref := Env.extend_stmt_in_place env stmt ~pre block;
-(* Options.feedback "the new stmt is (sid %d): %a" stmt.sid
- Stmt.pretty stmt;*)
+ env_ref := Env.extend_stmt_in_place new_env stmt ~pre block;
ChangeTo stmt
end
in
- let bhv = (Env.get_visitor env)#behavior in
+ let bhv = (Env.get_visitor new_env)#behavior in
let new_stmt = Visitor.visitFramacStmt o (get_stmt bhv stmt) in
set_stmt bhv stmt new_stmt;
res, !env_ref, false
@@ -379,11 +387,11 @@ and comparison_to_exp ?(loc=Location.unknown) ?e1 env bop t1 t2 t_opt =
let ctx = match e1 with
| None -> principal_type_from_term t1 t2
| Some(_, ctx) ->
-(* Options.feedback "principality oriented by %a" d_logic_type ctx;*)
+ (* Options.feedback "principality oriented by %a" d_logic_type ctx;*)
principal_type_from_term { t1 with term_type = ctx } t2
in
-(* Options.feedback "principal type of %a and %a is %a"
- d_term t1 d_term t2 d_logic_type ctx;*)
+ (* Options.feedback "principal type of %a and %a is %a"
+ d_term t1 d_term t2 d_logic_type ctx;*)
let e1, env = match e1 with
| None -> term_to_exp env ctx t1
| Some(e1, ctx1) when Cil_datatype.Logic_type.equal ctx ctx1 -> e1, env
--
GitLab