Specifications with Addressable Local Variables

Question

I'm trying to understand how VST handles (addressable) local variables, so I wrote this function:

int main() {
    int x = 5, y = 7;
    int *a = &x;
    int *b = &y;

    *a = 8;
    *b = 9;

    return x;
}

then I tried to verify it with the following specification:

Definition main_spec :=
 DECLARE _main
  WITH p : int (* still toying with things, couldn't figure out how to drop this *)
  PRE [ ]
   PROP ()
   LOCAL ()
   SEP ()
  POST [ tint ]
   EX i : Z,
   PROP ( i = 8 )
   LOCAL (temp ret_temp  (Vint (Int.repr i)))
   SEP ().

Everything goes well simply using (forward) until the return statement where I am left to prove the following

data_at Tsh tint (vint 9) v_y * data_at Tsh tint (vint 8) v_x |-- FF

which seems like it should be unprovable (note that I have just applied forward up until this point). I was expecting some specification stating that the heap is empty after the local variables had been de-allocated, i.e. emp |-- emp.

Is there somewhere that I could look to get more information about this?

Thanks!

Additional Information: I dug into the source of the FF post-condition, and it comes from typecheck_expr, in particular, the case for Evar:

  | Evar id ty =>
      match access_mode ty with
      | By_reference =>
          match get_var_type Delta id with
          | Some ty' =>
              tc_bool (eqb_type ty ty')
                (mismatch_context_type ty ty')
          | None =>
              tc_FF
                (var_not_in_tycontext Delta id)
          end
      | _ => tc_FF (deref_byvalue ty) (* ?? *)
      end

Unless I'm reading something wrong, this seems to suggest that you can not access local variables by value. Is this just an oversight? Or is there something in the semantics that prevents this?

Answer 1

The reason for this failure is that you forgot the -normalize flag to clightgen. If you translate your .c file using clightgen -normalize instead of clightgen, it should work fine.