From 33577608dd4cd76849d250cde84aa68f8426a616 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 31 Mar 2023 16:27:57 +0200
Subject: [PATCH] [test] Introducing new proposed metavars \lhost_read and
\lhost_written
---
tests/meta/lhost.c | 41 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 41 insertions(+)
create mode 100644 tests/meta/lhost.c
diff --git a/tests/meta/lhost.c b/tests/meta/lhost.c
new file mode 100644
index 0000000..c5cd5fd
--- /dev/null
+++ b/tests/meta/lhost.c
@@ -0,0 +1,41 @@
+/* run.config
+OPT: @META@ @PRINT@
+*/
+
+struct S {
+ unsigned owner;
+ int data;
+};
+
+extern unsigned current_id;
+
+int read(struct S* s) {
+ if (s->owner != current_id) return -1;
+ return s->data;
+}
+
+int write(struct S* s, int val) {
+ if (s->owner != current_id) return -1;
+ s->data = val;
+ return 0;
+}
+
+/*@ meta \prop,
+ \name(only_owner_reads),
+ \targets(\ALL),
+ \context(\reading),
+ \tguard(
+ \assert_type((struct S*)\lhost_read) &&
+ (!\separated(&(\lhost_read->data),\read) ==>
+ \lhost_read->owner == current_id);
+*/
+
+/*@ meta \prop,
+ \name(only_owner_writes),
+ \targets(\ALL),
+ \context(\writing),
+ \tguard(
+ \assert_type((struct S*)\lhost_written) &&
+ (!\separated(&(\lhost_written->data),\written) ==>
+ \lhost_written->owner == current_id);
+*/
--
GitLab