Move annotations to make tests in folder 42 compile

References #492

Author: michael-schwarz

tests/regression/23-partitioned_arrays_last/01-simple_array.c

@@ -156,7 +156,7 @@ void example7(void) {
     assert(a[top] == 0); // UNKNOWN
 }
 
-// Check that the global variable is not used for paritioning
+// Check that the global variable is not used for partitioning
 void example8() {
     int a[10];
 

tests/regression/42-annotated-precision/01-def_exc.c

@@ -1,15 +1,18 @@
 // PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint
 #include<assert.h>
 
-int f(int in) __attribute__ ((goblint_precision("def_exc", "interval"))) {
+int f(int in) __attribute__ ((goblint_precision("def_exc", "interval")));
+int main() __attribute__ ((goblint_precision("def_exc")));
+
+int f(int in) {
   in++;
   return in;
 }
 
-int main() __attribute__ ((goblint_precision("def_exc"))) {
+int main() {
   int a = 0;
   assert(a); // FAIL!
   a = f(a);
   assert(a);
   return 0;
-}
+}

tests/regression/42-annotated-precision/02-interval.c

@@ -1,15 +1,18 @@
 // PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint
 #include<assert.h>
 
-int f(int in) __attribute__ ((goblint_precision("no-def_exc","interval"))) {
+int f(int in) __attribute__ ((goblint_precision("no-def_exc","interval")));
+int main() __attribute__ ((goblint_precision("def_exc", "interval"))) ;
+
+int f(int in) {
   in++;
   return in;
 }
 
-int main() __attribute__ ((goblint_precision("def_exc", "interval"))) {
+int main() {
   int a = 0;
   assert(a); // FAIL!
   a = f(a);
   assert(a);
   return 0;
-}
+}

tests/regression/42-annotated-precision/03-congruence.c

@@ -1,17 +1,20 @@
 // PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint
 #include<assert.h>
 
-int f(int in) __attribute__ ((goblint_precision("no-def_exc","interval"))) {
+int f(int in) __attribute__ ((goblint_precision("no-def_exc","interval")));
+int main() __attribute__ ((goblint_precision("no-def_exc","congruence")));
+
+int f(int in) {
   in++;
   return in;
 }
 
-int main() __attribute__ ((goblint_precision("no-def_exc","congruence"))) {
+int main() {
   int a = 0;
   int b = f(a);
   assert(b);
   a = b % 2;
   b = f(a);
   assert(b == 2);
   return 0;
-}
+}

tests/regression/42-annotated-precision/04-struct.c

@@ -6,12 +6,15 @@ struct a {
   int i;
 };
 
-void f(struct a *in) __attribute__ ((goblint_precision("no-def_exc","interval", "congruence"))) {
+void f(struct a *in) __attribute__ ((goblint_precision("no-def_exc","interval", "congruence")));
+int main() __attribute__ ((goblint_precision("congruence")));
+
+void f(struct a *in) {
   in->i += 4;
   return;
 }
 
-int main() __attribute__ ((goblint_precision("congruence"))) {
+int main() {
   struct a a1, b1 = {"Jane", 3};
 
   a1.name = "John";
@@ -24,4 +27,4 @@ int main() __attribute__ ((goblint_precision("congruence"))) {
   b1.i = a1.i % 5;
   assert(b1.i); // FAIL!
   return 0;
-}
+}

tests/regression/42-annotated-precision/05-array.c

@@ -3,7 +3,12 @@
 #include<stdbool.h>
 #include<assert.h>
 
-void f(int in[], int len) __attribute__ ((goblint_precision("no-def_exc","interval", "congruence"))) {
+void f(int in[], int len) __attribute__ ((goblint_precision("no-def_exc","interval", "congruence")));
+void g(bool in[], int len) __attribute__ ((goblint_precision("interval", "enums", "congruence")));
+int main() __attribute__ ((goblint_precision("interval")));
+
+
+void f(int in[], int len) {
   assert(in[0]); // FAIL!
   int c[len];
   for (int i = 0; i < len; i++) {
@@ -13,14 +18,14 @@ void f(int in[], int len) __attribute__ ((goblint_precision("no-def_exc","interv
   return;
 }
 
-void g(bool in[], int len) __attribute__ ((goblint_precision("interval", "enums", "congruence"))) {
+void g(bool in[], int len) {
   for (int i = 0; i < len; i++) {
     in[i] ^= true;
   }
   return;
 }
 
-int main() __attribute__ ((goblint_precision("interval"))) {
+int main() {
   int a[] = {0,0,0};
   bool b[] = {true, false};
   char s[][] = {"Edward","Tom","Julia"};
@@ -34,4 +39,4 @@ int main() __attribute__ ((goblint_precision("interval"))) {
   a[1] = 1;
   assert(a[1]); // UNKNOWN!
   return 0;
-}
+}

tests/regression/42-annotated-precision/06-global.c

@@ -1,21 +1,24 @@
 // PARAM: --enable annotation.int.enabled --enable exp.earlyglobs --set ana.int.refinement fixpoint
 #include<assert.h>
 
+int inc(int in) __attribute__ ((goblint_precision("no-def_exc", "interval")));
+int main() __attribute__ ((goblint_precision("def_exc")));
+
 int g1 = 0;
 int g2 = 0;
 
-int inc(int in) __attribute__ ((goblint_precision("no-def_exc", "interval"))) {
+int inc(int in) {
     int b = in + 1;
     assert(b);
     g2 = 1;
     return b;
 }
 
-int main() __attribute__ ((goblint_precision("def_exc"))) {
+int main() {
   int a = 0;
   assert(g1); // FAIL!
   a = inc(g1);
   assert(a == g1); // FAIL!
   assert(a == g2); // UNKNOWN!
   return 0;
-}
+}

tests/regression/42-annotated-precision/07-missing_annotation.c

@@ -1,12 +1,16 @@
 // PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint
 
-int f(int in) __attribute__((goblint_precision("def_exc"))) {
+int f(int in) __attribute__((goblint_precision("def_exc")));
+int main() __attribute__((goblint_precision("no-def_exc")));
+
+
+int f(int in) {
   return in + 1;
 }
 
-int main() __attribute__((goblint_precision("no-def_exc"))) {
+int main() {
   int a = 1;
   assert(a); // UNKNOWN!
   a = f(a);
   return 0;
-}
+}

tests/regression/42-annotated-precision/08-22_01-simple_array.c

@@ -1,7 +1,20 @@
 // PARAM: --set solver td3 --enable ana.int.interval --enable exp.partition-arrays.enabled  --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set exp.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint
 int global;
 
-int main(void) __attribute__((goblint_precision("no-interval")))
+int main(void) __attribute__((goblint_precision("no-interval")));
+void example1(void) __attribute__((goblint_precision("no-def_exc")));
+void example2(void) __attribute__((goblint_precision("no-def_exc")));
+void example3(void) __attribute__((goblint_precision("no-def_exc")));
+void example4(void) __attribute__((goblint_precision("no-def_exc")));
+void example5(void) __attribute__((goblint_precision("no-def_exc")));
+void example6(void) __attribute__((goblint_precision("no-def_exc")));
+void example7(void) __attribute__((goblint_precision("no-def_exc")));
+void example8() __attribute__((goblint_precision("no-def_exc")));
+void example9() __attribute__((goblint_precision("no-def_exc")));
+void example10() __attribute__((goblint_precision("no-def_exc")));
+
+
+int main(void)
 {
     example1();
     example2();
@@ -17,7 +30,7 @@ int main(void) __attribute__((goblint_precision("no-interval")))
 }
 
 // Simple example
-void example1(void) __attribute__((goblint_precision("no-def_exc")))
+void example1(void)
 {
     int a[42];
     int i = 0;
@@ -37,7 +50,7 @@ void example1(void) __attribute__((goblint_precision("no-def_exc")))
 }
 
 // More complicated expression to index rather than just a variable
-void example2(void) __attribute__((goblint_precision("no-def_exc"))) {
+void example2(void) {
     int a[42];
     int i = 1;
 
@@ -54,7 +67,7 @@ void example2(void) __attribute__((goblint_precision("no-def_exc"))) {
 }
 
 // Two values initialized in one loop
-void example3(void) __attribute__((goblint_precision("no-def_exc"))) {
+void example3(void) {
     int a[42];
     int i = 0;
 
@@ -72,7 +85,7 @@ void example3(void) __attribute__((goblint_precision("no-def_exc"))) {
 }
 
 // Example where initialization proceeds backwards
-void example4(void) __attribute__((goblint_precision("no-def_exc"))) {
+void example4(void) {
     int a[42];
     int i = 41;
 
@@ -88,7 +101,7 @@ void example4(void) __attribute__((goblint_precision("no-def_exc"))) {
 }
 
 // Example having two arrays partitioned according to one expression
-void example5(void) __attribute__((goblint_precision("no-def_exc"))) {
+void example5(void) {
     int a[42];
     int b[42];
     int i = 0;
@@ -109,7 +122,7 @@ void example5(void) __attribute__((goblint_precision("no-def_exc"))) {
 }
 
 // Example showing array becoming partitioned according to different expressions
-void example6(void) __attribute__((goblint_precision("no-def_exc"))) {
+void example6(void) {
     int a[42];
     int i = 0;
     int j = 0;
@@ -139,7 +152,7 @@ void example6(void) __attribute__((goblint_precision("no-def_exc"))) {
 }
 
 // This was the case where we thought we needed path-splitting
-void example7(void) __attribute__((goblint_precision("no-def_exc"))) {
+void example7(void) {
     int a[42];
     int i = 0;
     int top;
@@ -159,7 +172,7 @@ void example7(void) __attribute__((goblint_precision("no-def_exc"))) {
 }
 
 // Check that the global variable is not used for partitioning
-void example8() __attribute__((goblint_precision("no-def_exc"))) {
+void example8() {
     int a[10];
 
     a[global] = 4;
@@ -177,7 +190,7 @@ void example8() __attribute__((goblint_precision("no-def_exc"))) {
 }
 
 // Check that arrays of types different from int are handeled correctly
-void example9() __attribute__((goblint_precision("no-def_exc"))) {
+void example9() {
     char a[10];
     int n;
     assert(a[3] == 800); // FAIL
@@ -196,7 +209,7 @@ void example9() __attribute__((goblint_precision("no-def_exc"))) {
     assert(a[3] == -129); //FAIL
 }
 
-void example10() __attribute__((goblint_precision("no-def_exc"))) {
+void example10() {
     int a[20];
     a[5] = 3;