From cdd242136e0a1f9aaae01cb52907d5d2f2d2f3e9 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 13 Oct 2020 11:04:36 +0200
Subject: [PATCH] [eacsl] Fix RTL function prefix in debug compilation
---
.../share/e-acsl/observation_model/e_acsl_observation_model.c | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
index 0e413258b36..9b1baa7ad97 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
@@ -39,7 +39,8 @@
* otherwise.
*/
int separated2(void * ptr1, size_t size1, void * ptr2, size_t size2) {
- DASSERT(valid_read(ptr1, size1, base_addr(ptr1), NULL) && valid_read(ptr2, size2, base_addr(ptr2), NULL));
+ DASSERT(eacsl_valid_read(ptr1, size1, eacsl_base_addr(ptr1), NULL)
+ && eacsl_valid_read(ptr2, size2, eacsl_base_addr(ptr2), NULL));
// Cast pointers to char* to be able to do pointer arithmetic without
// triggering undefined behavior
--
GitLab