How to deal with potentially-aliased arguments in VST?

Consider the following code:

void incr(int *a, int *b) {
    (*a)++;
    (*b)++;
}

void f(int *a, int *b) {
  incr(a, b);
  incr(a, a);
}

The incr function admits two specifications:

• {a ↦ n * b ↦ m} incr(a, b) {a ↦ n + 1 * b ↦ m + 1}
• {a ↦ n} incr(a, a) {a ↦ n + 2}

How to specify which one to use when proving f?

From VST.floyd Require Import proofauto library.
Require Import incr.

#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

Definition incr_spec :=
  DECLARE _incr
  WITH a : val, n : Z, b : val, m : Z
  PRE [tptr tint, tptr tint]
    PROP (Int.min_signed <= n < Int.max_signed;
          Int.min_signed <= m < Int.max_signed)
    PARAMS (a; b)
    SEP (data_at Ews tint (Vint (Int.repr n)) a;
         data_at Ews tint (Vint (Int.repr m)) b)
  POST [tvoid]
    PROP ()
    RETURN ()
    SEP (data_at Ews tint (Vint (Int.repr (n + 1))) a;
         data_at Ews tint (Vint (Int.repr (m + 1))) b).

Definition incr_spec2 :=
  DECLARE _incr
  WITH a : val, n : Z
  PRE [tptr tint, tptr tint]
    PROP (Int.min_signed <= n <= Int.max_signed - 2)
    PARAMS (a; a)
    SEP (data_at Ews tint (Vint (Int.repr n)) a)
  POST [tvoid]
    PROP ()
    RETURN ()
    SEP (data_at Ews tint (Vint (Int.repr (n + 2))) a).

Definition f_spec :=
  DECLARE _f
  WITH a : val, n : Z, b : val, m : Z
  PRE [tptr tint, tptr tint]
    PROP (Int.min_signed <= n <= Int.max_signed - 3;
          Int.min_signed <= m < Int.max_signed)
    PARAMS (a; b)
    SEP (data_at Ews tint (Vint (Int.repr n)) a;
         data_at Ews tint (Vint (Int.repr m)) b)
  POST [tvoid]
    PROP ()
    RETURN ()
    SEP (data_at Ews tint (Vint (Int.repr (n + 3))) a;
         data_at Ews tint (Vint (Int.repr (m + 1))) b).

Definition Gprog := [ incr_spec; incr_spec2 ].

(* Lemma body_f : *)
(*   semax_body Vprog Gprog f_f f_spec. *)
(* Proof. *)
(*   start_function. *)
(*   forward_call. *)

This is not exactly what you asked for, but this ought to work. At the forward_call, you'll have to specify the boolean value of aliased .

Definition incr_spec :=
  DECLARE _incr
  WITH aliased: bool, a : val, n : Z, b : val, m : Z
  PRE [tptr tint, tptr tint]
    PROP (Int.min_signed <= n < (if aliased then (Int.max_signed-1) else Int.max_signed);
          Int.min_signed <= m < Int.max_signed)
    PARAMS (a; b)
    SEP (if aliased 
         then (!! (a=b) 
               && data_at Ews tint (Vint (Int.repr n)) a);
         else (data_at Ews tint (Vint (Int.repr n)) a * 
               data_at Ews tint (Vint (Int.repr m)) b)
  POST [tvoid]
    PROP ()
    RETURN ()
    SEP (if aliased 
         then data_at Ews tint (Vint (Int.repr (n + 2))) a;
         else (data_at Ews tint (Vint (Int.repr (n+1))) a * data_at Ews tint (Vint (Int.repr (m + 1))) b).