From 79ad9ebe10706d7f06fd5f4a3d13e1eca62394ad Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 24 Feb 2021 11:54:53 +0100
Subject: [PATCH] [eacsl] Fix e_acsl_observation_model.h contracts
If the Frama-C libc is used, then include `__fc_alloc_axiomatic.h`,
otherwise redeclare the axiomatics from this file.
In the redeclared axiomatics, use `SIZE_MAX` instead of `__FC_SIZE_MAX`
in E-ACSL specification since the Frama-C libc will not be available to
define this constant.
---
.../e-acsl/observation_model/e_acsl_observation_model.h | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
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 4a5a8204afd..12ce416be29 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 {{{ ***/
--
GitLab