From 0ff8ec7c2b6afa1399c74df06cca05fdbc335769 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 7 Mar 2016 19:05:53 +0100
Subject: [PATCH] [tests] Added test case for \block_length predicate
---
.../tests/e-acsl-runtime/block_length.c | 62 +++++++++++++++++++
1 file changed, 62 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/block_length.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/block_length.c b/src/plugins/e-acsl/tests/e-acsl-runtime/block_length.c
new file mode 100644
index 00000000000..9898e98c851
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/block_length.c
@@ -0,0 +1,62 @@
+/* run.config
+ COMMENT: Behaviours of the \block_length E-ACSL predicate
+*/
+
+#include <stdlib.h>
+
+int A[] = { 1, 2, 3, 4};
+int *PA;
+
+struct Zero { } ZERO;
+
+int main(void) {
+ /* Global memory */
+ PA = (int*)&A;
+ /*@ assert \block_length(A) == sizeof(A); */
+ /*@ assert \block_length(A+3) == sizeof(A); */
+ /*@ assert \block_length(PA) == sizeof(A); */
+ PA++;
+ /*@ assert \block_length(PA+1) == \block_length(A+1); */
+
+ /* Stack memory [long blocks] */
+ int a[] = { 1, 2, 3, 4};
+ int *pa = (int*)&a;
+ /*@ assert \block_length(a) == sizeof(a); */
+ /*@ assert \block_length(a+3) == sizeof(a); */
+ /*@ assert \block_length(pa) == sizeof(a); */
+ pa++;
+ /*@ assert \block_length(pa+1) == \block_length(a+1); */
+
+ /* Stack memory [Short blocks] */
+
+ long l = 4;
+ char *pl = (char*)&l;
+ /*@ assert \block_length(&l) == sizeof(long); */
+ /*@ assert \block_length(pl) == sizeof(long); */
+ /*@ assert \block_length(pl+7) == sizeof(long); */
+ int *pi = (int*)&l;
+ /*@ assert \block_length(pi) == \block_length(&l); */
+ pi++;
+ /*@ assert \block_length(pi) == \block_length(&l); */
+
+ /* Heap memory [single segment] */
+ size_t size = 12;
+ char *p = malloc(size);
+ /*@ assert \block_length(p) == size; */
+ /*@ assert \block_length(p+11) == size; */
+ p += 5;
+ /*@ assert \block_length(p+5) == \block_length(p-5); */
+
+ /* Heap memory [multiple segments] */
+ size = 30*sizeof(long);
+ long *q = malloc(size);
+
+ /*@ assert \block_length(q) == size; */
+ q += 4;
+ /*@ assert \block_length(q) == size; */
+
+ /* Zero-sized blocks */
+ struct Zero zero;
+ /*@ assert \block_length(&ZERO) == 0; */
+ /*@ assert \block_length(&zero) == 0; */
+}
--
GitLab