diff --git a/tests/value/oracle/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle index adc483ff665929f6a5ccbcac65eee15f7da03395..aa8dc50d410df0a8961e66ac04949f144fedee20 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;