Conditional variable name binding

[mu-mu-mu]

Hello,

I am verifying the following simple function.

void add(int *a, int *b, int *c) 
{
    *a = *b + *c;
}

When this function is called, the pointers a and b might point to the same memory, e.g., add(p, p, q) where p and q are pointers to int.

I wrote the following pre and post condition.

//@requires *a |-> ?aa &*&  (a == b ? emp : *b |-> ?bb) &*& *c |-> ?cc;
//@ensures  *a |-> ((a == b ? aa : bb) + cc) &*& (a == b ? emp : *b |-> bb) &*& *c |-> cc;

However, it failed due to an error: No such variable, constructor, regular function, predicate, enum element, global variable, or module: bb.

How could I refer to the variable bb? Or should I avoid this strategy to verify the function?

Thank you.

[btj]

Here, it is helpful to nest the ensures clause inside the requires clause:

void add(int *a, int *b, int *c) 
/*@
requires
    *a |-> ?aa &*&
    [?fc]*c |-> ?cc &*&
    b == a ?
        ensures *a |-> aa + cc &*& [fc]*c |-> cc
    :
        [?fb]*b |-> ?bb &*&
        ensures *a |-> bb + cc &*& [fb]*b |-> bb &*& [fc]*c |-> cc;
@*/
//@ ensures true;
{
    *a = *b + *c;
}

(The VeriFast parser still requires a separate ensures clause as well but it is ignored.)

An alternative approach is by using a predicate:

/*@

predicate ab(int *a, real fb, int *b, int aa, int bb) =
    *a |-> aa &*&
    b == a ?
        bb == aa
    :
        [fb]*b |-> bb;

@*/

void add(int *a, int *b, int *c) 
//@ requires ab(a, ?fb, b, ?aa, ?bb) &*& [?fc]*c |-> ?cc;
//@ ensures *a |-> bb + cc &*& (b == a ? true : [fb]*b |-> bb) &*& [fc]*c |-> cc;
{
    //@ open ab(_, _, _, _, _);
    *a = *b + *c;
}

[mu-mu-mu]

Thank you for your help.

I ran the function with a caller.

int main()
//@ requires true;
//@ ensures true;
{
  int a = 0, b = 0, c =10;
  add(&a, &b, &c);
//add(&a, &a, &c);
  assert (a == 10);
  return 0;
}

I could verify the former case. However, in the latter case, I encountered this error: a.c(11,14-16): No matching heap chunks: ab(a_addr, _, b_addr, _, _).

Could you help debug this?

complete source code

/*@
predicate ab(int *a, real fb, int *b, int aa, int bb) =
    *a |-> aa &*&
    b == a ?
        bb == aa
    :
        [fb]*b |-> bb;
@*/

void add(int *a, int *b, int *c)
//@ requires ab(a, ?fb, b, ?aa, ?bb) &*& [?fc]*c |-> ?cc;
//@ ensures *a |-> bb + cc &*& (b == a ? true : [fb]*b |-> bb) &*& [fc]*c |-> cc;
{
    //@ open ab(_, _, _, _, _);
    *a = *b + *c;
}

int main()
//@ requires true;
//@ ensures true;
{
  int a = 0, b = 0, c =10;
  add(&a, &a, &c);
  assert (a == 10);
  return 0;
}

[mu-mu-mu]

I could verify the latter, but I am not sure how to select the number of the fractional permission in that case. Is it ok to select any number in (0,1]? Also, is it only for concurrent verification?

Thank you.

/*@
predicate ab(int *a, real fb, int *b, int aa, int bb) =
    *a |-> aa &*&
    b == a ?
        bb == aa
    :
        [fb]*b |-> bb;
@*/

void add(int *a, int *b, int *c)
//@ requires ab(a, ?fb, b, ?aa, ?bb) &*& [?fc]*c |-> ?cc;
//@ ensures *a |-> bb + cc &*& (b == a ? true : [fb]*b |-> bb) &*& [fc]*c |-> cc;
{
    //@ open ab(_, _, _, _, _);
    *a = *b + *c;
}

int main()
//@ requires true;
//@ ensures true;
{
  int a = 0, b = 0, c =10;
  //@close ab(&a, 1, &a, ?bb, ?cc);
  add(&a, &a, &c);
  assert (a == 10);
  return 0;
}

[btj]

If a == b, any real number at all will do for fb since it is not used. Fractional permissions are useful whenever there is sharing, not just between threads but also between parts of a single-threaded program. For example, you may have some immutable data that you want to use in various places without bothering to track ownership.

[mu-mu-mu]

you may have some immutable data that you want to use in various places without bothering to track ownership. Ah, I understand. Thank you very much for your help.