From 35d02826aa267ef2ed33138940c788b0ea5d4646 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 31 Mar 2020 18:31:50 +0200
Subject: [PATCH] [kernel] updated oracles wrt. sizeof(exp)
Old translation was potentially incorrect for sizeof(exp)
---
tests/value/oracle/sizeof.res.oracle | 18 ++++++++++--------
1 file changed, 10 insertions(+), 8 deletions(-)
diff --git a/tests/value/oracle/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle
index adc483ff665..aa8dc50d410 100644
--- a/tests/value/oracle/sizeof.res.oracle
+++ b/tests/value/oracle/sizeof.res.oracle
@@ -25,16 +25,16 @@
The imprecision originates from Arithmetic {tests/value/sizeof.i:32}
[eva:alarm] tests/value/sizeof.i:33: Warning:
accessing out of bounds index.
- assert (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
+ assert (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
[eva:alarm] tests/value/sizeof.i:33: Warning:
out of bounds write.
- assert \valid(&p->t[(unsigned int)(sizeof(s1.t) - (unsigned int)i)]);
+ assert \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]);
[eva:alarm] tests/value/sizeof.i:34: Warning:
accessing out of bounds index.
- assert (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
+ assert (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
[eva:alarm] tests/value/sizeof.i:34: Warning:
out of bounds write.
- assert \valid(&p->t[(unsigned int)(sizeof(s1.t) - (unsigned int)i)]);
+ assert \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]);
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function f <- main.
@@ -129,19 +129,21 @@ void main2(void)
/*@ assert Eva: pointer_downcast: (unsigned int)(&s1) ≤ 2147483647; */
struct s *p = (& s1 + (int)(& s1)) - (int)(& s1);
/*@ assert
- Eva: index_bound: (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
+ Eva: index_bound:
+ (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
*/
/*@ assert
Eva: mem_access:
- \valid(&p->t[(unsigned int)(sizeof(s1.t) - (unsigned int)i)]);
+ \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]);
*/
p->t[sizeof(s1.t) - (unsigned int)i] = 1;
/*@ assert
- Eva: index_bound: (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
+ Eva: index_bound:
+ (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
*/
/*@ assert
Eva: mem_access:
- \valid(&p->t[(unsigned int)(sizeof(s1.t) - (unsigned int)i)]);
+ \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]);
*/
p->t[sizeof(s1.t) - (unsigned int)i] = 2;
return;
--
GitLab