#include <civlc.cvh>
#include <memory.cvh>

enum CMD{
  SEND, RECV
};

$atomic_f void sendRecv(enum CMD cmd, void*buf, int**array)
  $depends [cmd==SEND] {$write(buf), $calls(sendRecv(cmd, buf, ...))}
  $depends [cmd==RECV] {$access(*buf)}
  $assigns [cmd==SEND] {$nothing}
  $assigns [cmd==RECV] {*buf}
  $reads {array[2 .. 5][...], *buf}
{
  if(cmd == SEND){
    //send(*buf, ...);
    int a = 0;

    a++;
  }else if(cmd==RECV){
    //*buf=recv(...);
    int a = 0;

    a++;
  }
}