diff --git a/tests/syntax/oracle/unroll_visit.res.oracle b/tests/syntax/oracle/unroll_visit.res.oracle index 1a379a6743705c352cce356440beb9ca38b2a218..271518ba4c2d9a67a2fd616ca5818cbe5d4818b3 100644 --- a/tests/syntax/oracle/unroll_visit.res.oracle +++ b/tests/syntax/oracle/unroll_visit.res.oracle @@ -4,8 +4,8 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization -[eva] tests/syntax/unroll_visit.i:8: assertion got status valid. -[eva] tests/syntax/unroll_visit.i:6: starting to merge loop iterations +[eva] tests/syntax/unroll_visit.i:9: assertion got status valid. +[eva] tests/syntax/unroll_visit.i:7: starting to merge loop iterations [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== @@ -23,28 +23,29 @@ [inout] Inputs for function main: \nothing /* Generated by Frama-C */ +typedef char i8; void main(void) { - int i = 0; - if (! (i < 100)) goto unrolling_2_loop; - i --; + i8 i = (char)0; + if (! ((int)i < 100)) goto unrolling_2_loop; + i = (char)((int)i - 1); /*@ assert i < 100; */ ; - i ++; - i ++; + i = (char)((int)i + 1); + i = (char)((int)i + 1); unrolling_4_loop: ; - if (! (i < 100)) goto unrolling_2_loop; - i --; + if (! ((int)i < 100)) goto unrolling_2_loop; + i = (char)((int)i - 1); /*@ assert i < 100; */ ; - i ++; - i ++; + i = (char)((int)i + 1); + i = (char)((int)i + 1); unrolling_3_loop: ; /*@ loop pragma UNROLL 2; loop pragma UNROLL "done", 2; */ - while (i < 100) { - i --; + while ((int)i < 100) { + i = (char)((int)i - 1); /*@ assert i < 100; */ ; - i ++; - i ++; + i = (char)((int)i + 1); + i = (char)((int)i + 1); } unrolling_2_loop: ; return; diff --git a/tests/syntax/unroll_visit.i b/tests/syntax/unroll_visit.i index 38d55c380b64b1be5bc5017806f5f0f462ef59e8..495b3bd0c50ce064137350a98b95406b6d5ed3ff 100644 --- a/tests/syntax/unroll_visit.i +++ b/tests/syntax/unroll_visit.i @@ -1,9 +1,10 @@ /* run.config STDOPT: +"-eva @EVA_CONFIG@ -deps -out -input -deps" */ +typedef char i8; // ideally, pretty-printing should keep 'i8' for some casts void main() { /*@ loop pragma UNROLL 2; */ - for(int i=0; i<100; i++) { + for(i8 i=0; i<100; i++) { i--; //@ assert i<100; i++;