Merge pull request #6496 from tautschnig/duplicate-label

C front-end: reject code containing duplicate labels

Author: tautschnig

regression/ansi-c/duplicate_label1/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int x;
+label:
+  x = 1;
+  goto label;
+label:
+  x = 2;
+}

regression/ansi-c/duplicate_label1/test.desc

@@ -0,0 +1,9 @@
+CORE test-c++-front-end
+main.c
+
+^EXIT=(1|64)$
+^SIGNAL=0$
+error: duplicate label 'label'
+^CONVERSION ERROR$
+--
+^warning: ignoring

regression/cbmc-concurrency/atomic_section_sc3/main.c

@@ -85,8 +85,10 @@ unsigned dec() {
 
 int main(){
 __CPROVER_ASYNC_1: inc();
-__CPROVER_ASYNC_1: dec();
-__CPROVER_ASYNC_1: dec();
+__CPROVER_ASYNC_2:
+  dec();
+__CPROVER_ASYNC_3:
+  dec();
 
   return 0;
 }

regression/cbmc-concurrency/conditional_spawn2/main.c

@@ -16,8 +16,10 @@ int main()
 __CPROVER_ASYNC_1: thread();
   }
 
-__CPROVER_ASYNC_1: thread();
-__CPROVER_ASYNC_1: thread();
+__CPROVER_ASYNC_2:
+  thread();
+__CPROVER_ASYNC_3:
+  thread();
 
   __CPROVER_assert(n<4, "3 threads spawned");
 

regression/cbmc-concurrency/generic_hw_sw_benchmark1/main.c

@@ -8,9 +8,9 @@
 
 #ifdef _ENABLE_CBMC_
 
-#define ASYNC(c) __CPROVER_ASYNC_1: (c)
-#define ATOMIC_BEGIN  __CPROVER_atomic_begin()
-#define ATOMIC_END  __CPROVER_atomic_end()
+#  define ASYNC(n, c) __CPROVER_ASYNC_##n : (c)
+#  define ATOMIC_BEGIN __CPROVER_atomic_begin()
+#  define ATOMIC_END __CPROVER_atomic_end()
 
 char symbolic_char(char);
 
@@ -233,7 +233,7 @@ void* write_data_register(struct Hardware *hw, RegisterId reg_id, Register value
     pthread_create(&interrupt_thread, NULL, hw->interrupt_handler, (void *) hw->fw);
   }
 #else
-    ASYNC(hw->interrupt_handler((void *) hw->fw));
+    ASYNC(1, hw->interrupt_handler((void *)hw->fw));
 #endif
 
 SKIP:
@@ -346,7 +346,7 @@ int main(void)
   pthread_t firmware_thread;
   pthread_create(&firmware_thread, NULL, poll, (void *) fw);
 #else
-  ASYNC(poll((void *) fw));
+  ASYNC(1, poll((void *)fw));
 #endif
 
 #ifdef _EXPOSE_BUG_
@@ -358,7 +358,7 @@ int main(void)
   pthread_t stimulus_thread;
   pthread_create(&stimulus_thread, NULL, stimulus, (void *) hw);
 #else
-  ASYNC(stimulus((void *) hw));
+  ASYNC(2, stimulus((void *)hw));
 #endif
 
 #ifdef _EXPOSE_BUG_

regression/cbmc-concurrency/invalid_object1/main.c

@@ -283,7 +283,7 @@ static signed int ethoc_reset(struct ethoc *dev)
 __CPROVER_ASYNC_1:
   open_eth_reg_write(dev->open_eth, (unsigned int)0, mode);
 
-__CPROVER_ASYNC_1:
+__CPROVER_ASYNC_2:
   open_eth_reg_write(dev->open_eth, (unsigned int)0, mode);
   return 0;
 }

regression/cbmc-concurrency/recursion1/main.c

@@ -13,7 +13,7 @@ int main()
 
 start2:
   (void)0;
-__CPROVER_ASYNC_1:
+__CPROVER_ASYNC_2:
   goto start2;
 
   rec_spawn();

regression/cbmc-concurrency/svcomp13_qrcu_safe/main.c

@@ -118,7 +118,9 @@ void* qrcu_updater() {
 
 int main() {
 __CPROVER_ASYNC_1: qrcu_reader1();
-__CPROVER_ASYNC_1: qrcu_reader2();
-__CPROVER_ASYNC_1: qrcu_updater();
+__CPROVER_ASYNC_2:
+  qrcu_reader2();
+__CPROVER_ASYNC_3:
+  qrcu_updater();
   return 0;
 }

regression/cbmc-concurrency/svcomp13_qrcu_unsafe/main.c

@@ -118,7 +118,9 @@ void* qrcu_updater() {
 
 int main() {
 __CPROVER_ASYNC_1: qrcu_reader1();
-__CPROVER_ASYNC_1: qrcu_reader2();
-__CPROVER_ASYNC_1: qrcu_updater();
+__CPROVER_ASYNC_2:
+  qrcu_reader2();
+__CPROVER_ASYNC_3:
+  qrcu_updater();
   return 0;
 }

regression/cbmc-concurrency/svcomp13_read_write_lock_safe/main.c

@@ -39,8 +39,11 @@ void *reader() { //reader
 
 int main() {
 __CPROVER_ASYNC_1: writer();
-__CPROVER_ASYNC_1: reader();
-__CPROVER_ASYNC_1: writer();
-__CPROVER_ASYNC_1: reader();
+__CPROVER_ASYNC_2:
+  reader();
+__CPROVER_ASYNC_3:
+  writer();
+__CPROVER_ASYNC_4:
+  reader();
   return 0;
 }