source: CIVL/mods/dev.civl.abc/examples/contract/por2.cvl

main
Last change on this file was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 486 bytes
Line 
1#include <civlc.cvh>
2#include <memory.cvh>
3
4enum CMD{
5 SEND, RECV
6};
7
8$atomic_f void sendRecv(enum CMD cmd, void*buf, int**array)
9 $depends [cmd==SEND] {$write(buf), $calls(sendRecv(cmd, buf, ...))}
10 $depends [cmd==RECV] {$access(*buf)}
11 $assigns [cmd==SEND] {$nothing}
12 $assigns [cmd==RECV] {*buf}
13 $reads {array[2 .. 5][...], *buf}
14{
15 if(cmd == SEND){
16 //send(*buf, ...);
17 int a = 0;
18
19 a++;
20 }else if(cmd==RECV){
21 //*buf=recv(...);
22 int a = 0;
23
24 a++;
25 }
26}
27
Note: See TracBrowser for help on using the repository browser.