No check for signed overflow in some cases.

[roconnor-blockstream]

Consider the following function:

void test(long a, long b) {
  long c = (unsigned int) a * b;
  long d = a * (unsigned int) b;
}

In both cases the unsigned int argument is promoted to signed long and the multiplication is performed as a signed long multiplication. In both cases an signed integer overflow could occur and we would need to verify that it does not.

However when run through VST only the d assignment yields an overflow side-condition check, while the c assignment appears to progress without checking for overflow.

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, b : int64
  PRE [ tlong, tlong ]
    PROP()
    PARAMS(Vlong a; Vlong b)
  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.
(* missing overflow entailment check. *)
forward.
(* overflow entailment check is produced here. *)
Abort.