Merge branch 'bugfix/basile/eacsl-no-fc-stdlib' into 'master'

[eacsl] Fix use of E-ACSL with `-no-frama-c-stdlib`

See merge request frama-c/frama-c!3083

src/plugins/e-acsl/doc/Changelog

@@ -37,6 +37,8 @@ Plugin E-ACSL <next-release>
                 (frama-c/e-acsl#104).
 -  e-acsl-gcc   [2021-02-24] Do not load Frama-C plugins when retrieving share
                 and plugins paths (frama-c/e-acsl#104).
+-* runtime      [2021-02-18] Fix integration of contracts from the runtime
+                library into Frama-C (#@999).
 -* E-ACSL       [2021-01-12] Fix crash when comparing two structs, which is
                 currently unsupported (frama-c/e-acsl#139).
 -* Makefile     [2021-01-05] Fix dependencies in bytecode-only compilation.

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h

@@ -35,7 +35,7 @@
 #ifdef __FC_STDLIB
 #include <__fc_alloc_axiomatic.h>
 #else
-/*@ ghost extern int __fc_heap_status __attribute__((FRAMA_C_MODEL)); */
+/*@ ghost extern int __fc_heap_status; */
 #endif
 
 #define contract_t                            export_alias(contract_t)

src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h

@@ -36,6 +36,9 @@
 #include "../internals/e_acsl_alias.h"
 #include "e_acsl_heap.h"
 
+#ifdef __FC_STDLIB
+#include <__fc_alloc_axiomatic.h>
+#else
 /*@ ghost extern int __fc_heap_status; */
 
 /*@ axiomatic dynamic_allocation {
@@ -45,9 +48,10 @@
   @   // predicate depends on the memory state
   @   axiom never_allocable{L}:
   @     \forall integer i;
-  @        i < 0 || i > __FC_SIZE_MAX ==> !is_allocable(i);
+  @        i < 0 || i > SIZE_MAX ==> !is_allocable(i);
   @ }
 */
+#endif
 
 /************************************************************************/
 /*** API Prefixes {{{ ***/

src/plugins/e-acsl/tests/test_config_dev.in

@@ -9,7 +9,7 @@ MACRO: ROOT_EACSL_GCC_ENABLE yes
 COMMENT: Default options for `e-acsl-gcc.sh`
 MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X
 COMMENT: Default options for the frama-c invocation
-MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0 -kernel-warn-key *=inactive
+MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
 COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation
 MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT
 COMMENT: Define the following macro in a test to pass extra options to `e-acsl-gcc.sh`