Skip to content
Snippets Groups Projects
Commit 35d02826 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[kernel] updated oracles wrt. sizeof(exp)

Old translation was potentially incorrect for sizeof(exp)
parent a0d20d3f
No related branches found
No related tags found
No related merge requests found
...@@ -25,16 +25,16 @@ ...@@ -25,16 +25,16 @@
The imprecision originates from Arithmetic {tests/value/sizeof.i:32} The imprecision originates from Arithmetic {tests/value/sizeof.i:32}
[eva:alarm] tests/value/sizeof.i:33: Warning: [eva:alarm] tests/value/sizeof.i:33: Warning:
accessing out of bounds index. 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: [eva:alarm] tests/value/sizeof.i:33: Warning:
out of bounds write. 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: [eva:alarm] tests/value/sizeof.i:34: Warning:
accessing out of bounds index. 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: [eva:alarm] tests/value/sizeof.i:34: Warning:
out of bounds write. 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] Recording results for main2
[eva] Done for function main2 [eva] Done for function main2
[eva] computing for function f <- main. [eva] computing for function f <- main.
...@@ -129,19 +129,21 @@ void main2(void) ...@@ -129,19 +129,21 @@ void main2(void)
/*@ assert Eva: pointer_downcast: (unsigned int)(&s1) ≤ 2147483647; */ /*@ assert Eva: pointer_downcast: (unsigned int)(&s1) ≤ 2147483647; */
struct s *p = (& s1 + (int)(& s1)) - (int)(& s1); struct s *p = (& s1 + (int)(& s1)) - (int)(& s1);
/*@ assert /*@ 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 /*@ assert
Eva: mem_access: 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; p->t[sizeof(s1.t) - (unsigned int)i] = 1;
/*@ assert /*@ 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 /*@ assert
Eva: mem_access: 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; p->t[sizeof(s1.t) - (unsigned int)i] = 2;
return; return;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment