2
votes

I've successfully compiled Frama-C Neon (Ubuntu) along with Why2, Why3 and Coq.

With previous versions (Nitrogen) it was possible to choose a particular heap model, by defining some symbols like:

#define FRAMA_C_MALLOC_HEAP

and so on.

The Frama-C Neon user manual suggests to include the file share/malloc.c, but I can't find it.

  • Frama-C Nitrogen contains both share/malloc.c andshare/libc/stdlib.c (including the latter worked fine);
  • Frama-C Fluorine 3 contains share/stdlib.c only;
  • Frama-C Fluorine 2 contains neither ;
  • Frama-C Neon contains neither;

Moreover the Fluorine 3 changelog lists "Add missing C library files."

Are FRAMA_C_MALLOC_* symbols deprecated or is the Neon source distribution somewhat incomplete?

1

1 Answers

1
votes

Yes, some files in relation to modeling dynamic memory allocation were removed from the Neon Frama-C release.