diff --git a/tests/meta/lhost.c b/tests/meta/lhost.c new file mode 100644 index 0000000000000000000000000000000000000000..c5cd5fd6b5a1ec6117de589d293b699d3c40d0c0 --- /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); +*/