Frama-c eva usually get message "invalid memory access" in program generated by Csmith

[tju-chenyaosuo]

Hi, I use csmith to generate test program, but I usually get "invalid memory access" or "accesses to uninitialized left-values" under frama-c-21.1 -eva. Is there something wrong with my usage of csmith or frama-c?

$ csmith > a.c
$ gcc -E -I /home/suocy/bin/csmith-2.3.0/include/csmith-2.3.0/ a.c -o pre.c
$ frama-c -c11 -cpp-command "gcc -C -Dvolatile= -E -I." -eva -machdep x86_64 pre.c
...
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  45 functions analyzed (out of 107): 42% coverage.
  In these functions, 2069 statements reached (out of 2427): 85% coverage.
  ----------------------------------------------------------------------------
  Some errors and warnings have been raised during the analysis:
    by the Eva analyzer:      0 errors    2 warnings
    by the Frama-C kernel:    0 errors    5 warnings
  ----------------------------------------------------------------------------
  6 alarms generated by the analysis:
       1 invalid memory access
       5 accesses to uninitialized left-values
  ----------------------------------------------------------------------------
  No logical properties have been reached by the analysis.
  ----------------------------------------------------------------------------

[tju-chenyaosuo]

use ''' perl -pi.bak -e 's/int main (int argc, char* argv[])/int argc; char **argv; int main (void)/' a.c &&\ frama-c -c11 -cpp-command "gcc -C -Dvolatile= -E -I." -eva -eva-precision 2 -machdep x86_64 pre.c '''

[PeiqiChen]

Have the same issue. 👏