From 548a008c26c7c9f3b1b4adccd10b1ae534211fc5 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 15 May 2017 15:56:21 +0200
Subject: [PATCH] Weak validity in segment model
---
.../e-acsl/segment_model/e_acsl_segment_tracking.h | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index 45fd1e1ab79..3bc186850f9 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -604,13 +604,13 @@ static int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr) {
length = short_lengths[code];
}
+#ifndef E_ACSL_WEAK_VALIDITY
if (addr != base_ptr) {
- uintptr_t base_addr = addr - offset;
- return BELONGS(base_ptr, base_addr, length)
+ return BELONGS(base_ptr, addr - offset, length)
&& offset + size <= length;
- } else {
- return offset + size <= length;
}
+#endif
+ return offset + size <= length;
}
return 0;
}
@@ -1053,8 +1053,12 @@ static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr) {
* offset is the difference between the address and base address (shadow[0])
* Then an address belongs to heap allocation if
* offset + size <= length */
+#ifndef E_ACSL_WEAK_VALIDITY
return base_shadow[0] == shadow[0] &&
(addr - shadow[0]) + size <= first_segment[1];
+#else
+ return (addr - shadow[0]) + size <= first_segment[1];
+#endif
}
return 0;
}
--
GitLab