There are missing declarations of local variables listed in the
"locations" or "exists" clause.
They can cause warnings from gcc that look like:
.../litmus0xx.c: In function 'code0':
.../litmus0xx.c:458:15: warning: cast from pointer to integer of different size
[-Wpointer-to-int-cast]
458 | *out_0_r1 = (int)r1;
| ^
Declare such local variables in the init blocks.
Signed-off-by: Akira Yokosawa <[email protected]>
---
.../herd/C-MP+o-o-rcusync-o+o-o-rcusync-o+rl-o-o-rul.litmus | 3 +++
.../C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus | 3 +++
CodeSamples/formal/herd/C-double-check-cas-2.litmus | 2 ++
CodeSamples/formal/herd/C-double-check-rcu-2.litmus | 2 ++
CodeSamples/formal/herd/C-double-check-rcu-3.litmus | 3 +++
CodeSamples/formal/herd/C-double-check-rcu-4.litmus | 4 ++++
6 files changed, 17 insertions(+)
diff --git
a/CodeSamples/formal/herd/C-MP+o-o-rcusync-o+o-o-rcusync-o+rl-o-o-rul.litmus
b/CodeSamples/formal/herd/C-MP+o-o-rcusync-o+o-o-rcusync-o+rl-o-o-rul.litmus
index d074d6c1..58887051 100644
--- a/CodeSamples/formal/herd/C-MP+o-o-rcusync-o+o-o-rcusync-o+rl-o-o-rul.litmus
+++ b/CodeSamples/formal/herd/C-MP+o-o-rcusync-o+o-o-rcusync-o+rl-o-o-rul.litmus
@@ -6,6 +6,9 @@ C C-MP+o-o-rcusync-o+o-o-rcusync-o+rl-o-o-rul
int b;
int c;
int *p=a;
+ int *0:r1; (* \fcvexclude *)
+ int *1:r1; (* \fcvexclude *)
+ int *2:r1; (* \fcvexclude *)
}
P0(int *a, int *b, int *c, int **p)
diff --git
a/CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus
b/CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus
index 86ea5553..37c7cb0f 100644
---
a/CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus
+++
b/CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus
@@ -6,6 +6,9 @@ C C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul
int b;
int c;
int *p=a; (* \lnlbl[init:p] *)
+ int *0:r1; (* \fcvexclude *)
+ int *1:r1; (* \fcvexclude *)
+ int *2:r1; (* \fcvexclude *)
}
P0(int *a, int *b, int *c, int **p)
diff --git a/CodeSamples/formal/herd/C-double-check-cas-2.litmus
b/CodeSamples/formal/herd/C-double-check-cas-2.litmus
index 4c2dc523..2296fe3d 100644
--- a/CodeSamples/formal/herd/C-double-check-cas-2.litmus
+++ b/CodeSamples/formal/herd/C-double-check-cas-2.litmus
@@ -5,6 +5,8 @@ C C-double-check-cas-2
int a;
int b;
int *p=0;
+ int *0:r1; (* \fcvexclude *)
+ int *1:r1; (* \fcvexclude *)
}
P0(int *a, int *b, int **p)
diff --git a/CodeSamples/formal/herd/C-double-check-rcu-2.litmus
b/CodeSamples/formal/herd/C-double-check-rcu-2.litmus
index ff7a1dd3..a108d318 100644
--- a/CodeSamples/formal/herd/C-double-check-rcu-2.litmus
+++ b/CodeSamples/formal/herd/C-double-check-rcu-2.litmus
@@ -5,6 +5,8 @@ C C-double-check-rcu-2
int a;
int b;
int *p=0;
+ int *0:r1; (* \fcvexclude *)
+ int *1:r1; (* \fcvexclude *)
}
P0(int *a, int *b, int **p)
diff --git a/CodeSamples/formal/herd/C-double-check-rcu-3.litmus
b/CodeSamples/formal/herd/C-double-check-rcu-3.litmus
index c5d5f9e4..6bff1f82 100644
--- a/CodeSamples/formal/herd/C-double-check-rcu-3.litmus
+++ b/CodeSamples/formal/herd/C-double-check-rcu-3.litmus
@@ -6,6 +6,9 @@ C C-double-check-rcu-3
int b;
int c;
int *p=0;
+ int *0:r1; (* \fcvexclude *)
+ int *1:r1; (* \fcvexclude *)
+ int *2:r1; (* \fcvexclude *)
}
P0(int *a, int *b, int *c, int **p)
diff --git a/CodeSamples/formal/herd/C-double-check-rcu-4.litmus
b/CodeSamples/formal/herd/C-double-check-rcu-4.litmus
index 02f34366..e81d5850 100644
--- a/CodeSamples/formal/herd/C-double-check-rcu-4.litmus
+++ b/CodeSamples/formal/herd/C-double-check-rcu-4.litmus
@@ -7,6 +7,10 @@ C C-double-check-rcu-4
int c;
int d;
int *p=0;
+ int *0:r1; (* \fcvexclude *)
+ int *1:r1; (* \fcvexclude *)
+ int *2:r1; (* \fcvexclude *)
+ int *3:r1; (* \fcvexclude *)
}
P0(int *a, int *b, int *c, int *d, int **p)
--
2.43.0
