Opaque Int64.repr blocking tactics

[roconnor-blockstream]

Consider the following function:

void test(long a) {
  if (a > -1L) return;
}

with the following correctness proof

Require Import VST.floyd.proofauto.
Require Import test.

Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Definition test_spec : ident * funspec :=
DECLARE _test
  WITH a : int64
  PRE [ tlong ]
    PROP()
    PARAMS(Vlong a)
  SEP()
POST [ tvoid ]
  PROP()
  RETURN()
  SEP(). 

Definition Gprog := ltac:(with_library prog
  [test_spec
  ]).

Lemma body_test: semax_body Vprog Gprog f_test test_spec.
Proof.
start_function.
(* forward_if just burns through memory. 
   However if you run: *)
(* Transparent Int64.repr.*)
(* forward_if runs as expected. *)
forward_if.
Abort.

For some reason Int64.repr is marked as Opaque (while Int.repr remains transparent). This prevents reduction that would otherwise solve conditions in examples such as the above.

This was tested in VST v2.11.1.

[andrew-appel]

Fixed in #684