Merge branch 'feature/andre/test-for-refactored-casts' into 'master'

[tests] add test for cast refactoring

See merge request frama-c/frama-c!3017

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;

tests/syntax/unroll_visit.i

 /* 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++;