Global array of doubles is not properly packaged by start_function

[andrew-appel]

... especially in 32-bit mode, but maybe also in 64-bit mode (not tested). See this report on stackoverflow:

https://stackoverflow.com/questions/75227625/vst-verification-of-global-array-of-doubles

[andrew-appel]

Example to demonstrate this (from stackoverflow):

double dbls[] = {0.0, 1.1};
int main() {
  double sum;
  sum = dbls[0] + dbls[1];
  return 0;
}

VST proof:

Require Import VST.floyd.proofauto.
Require Import VST.progs.foo.
#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE  [] main_pre prog tt gv
  POST [ tint ] main_post prog gv.

Definition Gprog : funspecs :=   [ ].

Lemma body_main: semax_body Vprog Gprog f_main main_spec.
Proof.
start_function.