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 {{{ ***/