diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 78cc37da4c49c8c878f610ec3f0fc6be7fa84fd8..05e7510ee516f4b4dbf613b0ecd8594eebd852bf 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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.
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h
index b3349fdf027d604293f5b9c3ced6a0a01507a455..96fe1fbbdb706aa92bee4db9cabd5c009e3d7148 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h
+++ b/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)
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
index 4a5a8204afda7fc9457a9b68a8c7712c5290ee09..12ce416be2984b2edce0a5080c8df258ca0ac9b2 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
+++ b/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 {{{ ***/
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index 5319ddedd5a6be13da2dc29af8cc3950e4f83913..c10b67e1493d2b3bb5f112244bf657a09a5e1122 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/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`