From edb12060621c6137c8ff11b204a3176414a26ad5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 25 Mar 2011 12:00:50 +0000
Subject: [PATCH] updating according to changes in Frama-C kernel
---
.../e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c | 4 ++--
.../tests/e-acsl-runtime/oracle/integer_constant.res.oracle | 4 ++--
src/plugins/e-acsl/visit.ml | 2 --
7 files changed, 10 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 5353425ece9..462f26204da 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -845,10 +845,10 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct mpz_t[1];
-/*@ ensures \valid(\at(x,Old));
+/*@ ensures \valid(\old(x));
assigns *x; */
extern void mpz_init(__mpz_struct * /*[1]*/ x ) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
assigns *z; */
extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
/*@ requires \valid(x);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index b54bf42b8c7..668d1cda588 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -272,7 +272,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct mpz_t[1];
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
assigns *z; */
extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
/*@ requires \valid(x);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 5873fe9fa5f..add013d2688 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -62,10 +62,10 @@ __pure__)) ;
__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z ,
mp_size_t __gmp_n ) __attribute__((
__pure__)) ;
-/*@ ensures \valid(\at(x,Old));
+/*@ ensures \valid(\old(x));
assigns *x; */
extern void __gmpz_init(__mpz_struct * /*[1]*/ x ) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
assigns *z; */
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
/*@ requires \valid(z1);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 67cc8ed29d4..4d40b16e6a0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -45,7 +45,7 @@ __pure__)) ;
__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z ,
mp_size_t __gmp_n ) __attribute__((
__pure__)) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
assigns *z; */
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1 ,
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 88b4e2f8fd4..20a0d8a4480 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
@@ -45,10 +45,10 @@ __pure__)) ;
__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z ,
mp_size_t __gmp_n ) __attribute__((
__pure__)) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
assigns *z; */
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
assigns *z; */
extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z ,
char const *str , int base ) ;
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 504adf43ccc..d9645140f4c 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
@@ -123,10 +123,10 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct mpz_t[1];
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
assigns *z; */
extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
assigns *z; */
extern int mpz_init_set_str(__mpz_struct * /*[1]*/ z , char const *str ,
int base ) ;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 03c5f2bfb2f..04c863bb48c 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -298,7 +298,6 @@ let rec term_to_exp t = match t.term_node with
| Tlambda _ -> not_yet "functional"
| TDataCons _ -> not_yet "constructor"
| Tif _ -> not_yet "conditional"
- | Told _ -> not_yet "\\old"
| Tat _ -> not_yet "\\at"
| Tbase_addr _ -> not_yet "\\base_addr"
| Tblock_length _ -> not_yet "\\block_length"
@@ -350,7 +349,6 @@ let rec named_predicate_to_revexp p = match p.content with
| Plet _ -> not_yet "let _ = _ in _"
| Pforall _ -> not_yet "\\forall"
| Pexists _ -> not_yet "\\exists"
- | Pold _ -> not_yet "\\old"
| Pat _ -> not_yet "\\at"
| Pvalid _ -> type_error "\\valid"
| Pvalid_index _ -> type_error "\\valid_index"
--
GitLab