Skip to content
Snippets Groups Projects
Commit 33577608 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[test] Introducing new proposed metavars \lhost_read and \lhost_written

parent fb6dc5ae
No related branches found
No related tags found
No related merge requests found
/* 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);
*/
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment