Merge pull request #5931 from tautschnig/labelled-decls

C front-end: labelled declarations are only supported by Visual Studio

Author: tautschnig

regression/ansi-c/label1/main.c

@@ -0,0 +1,14 @@
+extern void foo(int *, unsigned int);
+
+int main()
+{
+#ifdef _MSC_VER
+label:
+  int x;
+#elif defined(__GNUC__)
+  int *p;
+  unsigned int u;
+label:
+  __attribute__((unused)) foo(p, u);
+#endif
+}

regression/ansi-c/label1/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+GCC does not permit labelling declarations as they are not considered
+statements, and would result in ambiguity in case of label attributes. We used
+to run into this problem, treating the function call in this test as a KnR
+function declaration.
+
+Visual Studio, on the other hand, happily accepts labelled declarations.

regression/cbmc/destructors/main.c

@@ -6,7 +6,7 @@ int main(int argc, char **argv) {
 
   const float *pc = (const float []){1e0, 1e1, 1e2};
 
-start:
+start:;
   test newAlloc0 = {0};
   if(argv[0])
   {
@@ -20,7 +20,7 @@ int main(int argc, char **argv) {
     if (argv[2])
     {
       test newAlloc3 = {3};
-nested_if:
+    nested_if:;
       test newAlloc5 = {5};
       if (argv[3])
       {

regression/cbmc/symex_should_exclude_null_pointers/main.c

@@ -38,15 +38,15 @@ int main(int argc, char **argv) {
   int *ptr4 = maybe_null;
   goto check;
 
-deref:
+deref:;
   int deref4 = *ptr4;
   goto end_test4;
 
 check:
   __CPROVER_assume(ptr4 != 0);
   goto deref;
 
-end_test4:
+end_test4:;
 
   // Should be judged unsafe by LSPA and safe by value-set filtering
   // (guarded by confluence):

regression/cbmc/symex_should_filter_value_sets/main.c

@@ -61,28 +61,28 @@ int main(int argc, char **argv)
   int *p7 = ptr_to_a_or_b;
   goto check7;
 
-divide7:
+divide7:;
   int c7 = *p7;
   goto end_test7;
 
 check7:
   __CPROVER_assume(p7 != &a);
   goto divide7;
 
-end_test7:
+end_test7:;
 
   int *p8 = ptr_to_a_or_b;
   goto check8;
 
-divide8:
+divide8:;
   int c8 = *p8;
   goto end_test8;
 
 check8:
   __CPROVER_assume(*p8 != 2);
   goto divide8;
 
-end_test8:
+end_test8:;
 
   // Should work (value-set filtered by confluence of if and else):
   int *p9 = ptr_to_a_or_b;

regression/cbmc/unwind_counters2/main.c

@@ -1,8 +1,9 @@
 int main()
 {
   l2: goto l1;
-  l1: int x=5;
-  goto l2;
+  l1:;
+    int x = 5;
+    goto l2;
 
-  return 0;
+    return 0;
 }

regression/cbmc/unwind_counters3/main.c

@@ -2,8 +2,9 @@ int main()
 {
   int i=0;
   l2: if(i==1) int y=0;
-  l1: int x=5;
-  goto l2;
+  l1:;
+    int x = 5;
+    goto l2;
 
-  return 0;
+    return 0;
 }

regression/cbmc/unwind_counters4/main.c

@@ -8,7 +8,7 @@ int main()
     y = 10;
     goto label;
     x = 1; // dead code, makes sure the above goto is not removed
-  label:
+  label:;
     _Bool nondet;
     if(nondet)
       __CPROVER_assert(y != 10, "violated via first loop");

regression/goto-instrument/labels1/main.c

@@ -24,8 +24,9 @@ int main()
     x = 42;
 label_four:
   assert(foo() == 1);
+  fptr_t fp;
 label_five:
-  fptr_t fp = foo;
+  fp = foo;
   assert(fp() == 1);
 label_six:
   return *p;

regression/goto-instrument/safe-dereferences/main.c

@@ -30,15 +30,15 @@ int main(int argc, char **argv) {
   int *ptr4 = &x;
   goto check;
 
-deref:
+deref:;
   int deref4 = *ptr4;
   goto end_test4;
 
 check:
   __CPROVER_assume(ptr4 != 0);
   goto deref;
 
-end_test4:
+end_test4:;
 
   // Shouldn't work yet despite being safe (guarded by confluence):
   int *ptr5 = &x;