From 53a3dd0ec220c59ca1d0aaed6b08e108740ad341 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 15 May 2017 13:58:17 +0200
Subject: [PATCH] Extra assertions in bittree
---
.../bittree_model/e_acsl_bittree_mmodel.c | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index d9b0c65b197..b175532a53d 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -28,6 +28,23 @@
#include "e_acsl_bittree.h"
+/* Assertions in debug mode */
+#define ALLOCATED(_ptr,_size) \
+ ((allocated(_ptr, _size, _ptr) == NULL) ? 0 : 1)
+
+#ifdef E_ACSL_DEBUG
+#define DVALIDATE_RO_ACCESS(_ptr, _size) \
+ vassert(ALLOCATED(_ptr, _size), \
+ "Not allocated [%a, %a + %lu]", (uintptr_t)_ptr, _size)
+#define DVALIDATE_RW_ACCESS(_ptr, _size) { \
+ DVALIDATE_RO_ACCESS(_ptr, _size); \
+ vassert(!readonly(_ptr), "Location %a is read-only", (uintptr_t)_ptr); \
+}
+#else
+#define DVALIDATE_RO_ACCESS(_ptr, _size)
+#define DVALIDATE_RW_ACCESS(_ptr, _size)
+#endif
+
/**************************/
/* SUPPORT {{{ */
/**************************/
--
GitLab