Finding ways to specify Functional Specification Verifiable-c

Question

I'm just getting started with verifiable-c work and am struggling with generating functional specifications for the C code I've written. My basic example I'm working with is (C code) simply

int xor(int v1, int v2) {
  return v1 ^ v2;
}

and I'm having difficulty putting together the Definition xor_spec section.

Thanks.

Answer 1

Definition xor_spec :=
 DECLARE _xor
 WITH v1 : int, v2: int
 PRE [ _v1 OF tint, _v2 OF tint]
    PROP () 
    LOCAL (temp _v1 (Vint v1); temp _v2 (Vint v2))
    SEP ()
 POST [ tint ]
    PROP() 
    LOCAL (temp ret_temp (Vint (Int.xor v1 v2))) 
    SEP().

That version uses "int" values, that is, 32-bit integers from CompCert's Int module. Usually I like to specify my functions on the mathematical integers; that style of specification would like like:

Definition xor_spec2 :=
 DECLARE _xor
 WITH v1 : Z, v2: Z
 PRE [ _v1 OF tint, _v2 OF tint]
    PROP (0 <= v1 <= Int.max_unsigned; 0 <= v2 <= Int.max_unsigned) 
    LOCAL (temp _v1 (Vint (Int.repr v1)); temp _v2 (Vint (Int.repr v2)))
    SEP ()
 POST [ tint ]
    PROP() 
    LOCAL (temp ret_temp (Vint (Int.repr (Z.lxor v1 v2)))) 
    SEP().

Caveat: I haven't run either of these through Coq, so they might have minor typos. And I haven't studied Z.lxor enough to make sure it's what you'd want.