Weak-memory examples: selectively use thread-local variables

We cannot soundly handle pointer offsets that are shared across threads,
and will reject this in future to avoid unsound verification results.
Here, however, the pointer offsets are not actually shared, so we can
safely mark them `__CPROVER_thread_local`.

Author: tautschnig

regression/goto-instrument-wmm-core/ppc_aclwsrr000_PSO_ALL/aclwsrr000.c

@@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p2_r1 = 0;
 int __unbuffered_p2_r3 = 0;
-int __unbuffered_p2_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
 int __unbuffered_p2_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr000_PSO_OPC/aclwsrr000.c

@@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p2_r1 = 0;
 int __unbuffered_p2_r3 = 0;
-int __unbuffered_p2_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
 int __unbuffered_p2_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr000_RMO_ALL/aclwsrr000.c

@@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p2_r1 = 0;
 int __unbuffered_p2_r3 = 0;
-int __unbuffered_p2_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
 int __unbuffered_p2_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr000_RMO_OPC/aclwsrr000.c

@@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p2_r1 = 0;
 int __unbuffered_p2_r3 = 0;
-int __unbuffered_p2_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
 int __unbuffered_p2_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr000_TSO_ALL/aclwsrr000.c

@@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p2_r1 = 0;
 int __unbuffered_p2_r3 = 0;
-int __unbuffered_p2_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
 int __unbuffered_p2_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr000_TSO_OPC/aclwsrr000.c

@@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p2_r1 = 0;
 int __unbuffered_p2_r3 = 0;
-int __unbuffered_p2_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
 int __unbuffered_p2_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr002_POWER_ALL/aclwsrr002.c

@@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
 int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p1_r3 = 0;
-int __unbuffered_p1_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
 int __unbuffered_p1_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr002_POWER_OPC/aclwsrr002.c

@@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
 int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p1_r3 = 0;
-int __unbuffered_p1_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
 int __unbuffered_p1_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr002_PSO_ALL/aclwsrr002.c

@@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
 int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p1_r3 = 0;
-int __unbuffered_p1_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
 int __unbuffered_p1_r5 = 0;
 int x = 0;
 int y = 0;

regression/goto-instrument-wmm-core/ppc_aclwsrr002_PSO_OPC/aclwsrr002.c

@@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
 int __unbuffered_p0_r3 = 0;
 int __unbuffered_p1_r1 = 0;
 int __unbuffered_p1_r3 = 0;
-int __unbuffered_p1_r4 = 0;
+__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
 int __unbuffered_p1_r5 = 0;
 int x = 0;
 int y = 0;