From b4dc2e8b4d54894cfe72cf9da5a9fc8d40eb25f3 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Sat, 19 Jul 2014 18:14:58 +0200
Subject: [PATCH] Merge branch 'bug/bts1836' into 'stable/neon'
Bug/bts1836 (off by one in bittree)
---
src/plugins/e-acsl/.gitignore | 1 +
src/plugins/e-acsl/doc/Changelog | 2 +
.../e-acsl/memory_model/e_acsl_bittree.c | 3 +-
src/plugins/e-acsl/tests/check/Makefile | 29 +++++++
.../e-acsl/tests/check/check_e_acsl_bittree.c | 84 +++++++++++++++++++
5 files changed, 118 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/e-acsl/tests/check/Makefile
create mode 100644 src/plugins/e-acsl/tests/check/check_e_acsl_bittree.c
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 3ccc328577b..d7240f5a424 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -74,3 +74,4 @@
/tests/e-acsl-reject/result/*.annot
/tests/e-acsl-reject/result/*_DEP
/tests/e-acsl-reject/result/*.log
+/tests/check/obj/*
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 7210380aca5..7734389a2c9 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2014/07/19] Fix bug #1836 about one-off error when
+ computing the block which a pointer points to.
-* E-ACSL [2014/07/08] Fix bug about using some part of the
(Frama-C) libc which prevents linking of the generated C code.
-* E-ACSL [2014/05/21] Fix bug #1782 about incorrect URL in the
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index dd90b193a0e..d0329d4052f 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -371,7 +371,8 @@ struct _block * __get_cont (void * ptr) {
}
/* tmp->addr <= ptr, tmp may contain ptr
ptr is contained if tmp is large enough (begin addr + size) */
- else if((size_t)ptr <= tmp->leaf->size + tmp->addr)
+ else if((size_t)ptr < tmp->leaf->size + tmp->addr
+ || (tmp->leaf->size == 0 && (size_t)ptr == tmp->leaf->ptr))
return tmp->leaf;
/* tmp->addr <= ptr, but tmp->addr is not large enough */
else if (ind == -1)
diff --git a/src/plugins/e-acsl/tests/check/Makefile b/src/plugins/e-acsl/tests/check/Makefile
new file mode 100644
index 00000000000..3067f390e08
--- /dev/null
+++ b/src/plugins/e-acsl/tests/check/Makefile
@@ -0,0 +1,29 @@
+CC=gcc
+CFLAGS=-std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin
+SHARE=../../share/e-acsl
+LIBS=-lgmp -pthread -lcheck -lcheck_pic -lrt -lm
+ODIR=obj
+
+_DEPS=e_acsl.h memory_model/e_acsl_bittree.h memory_model/e_acsl_mmodel.h
+DEPS=$(patsubst %,$(SHARE)/%,$(_DEPS))
+
+_OBJ=e_acsl.o memory_model/e_acsl_bittree.o memory_model/e_acsl_mmodel.o check_e_acsl_bittree.o
+OBJ=$(patsubst %,$(ODIR)/%,$(_OBJ))
+
+
+run: $(ODIR)/tests.out
+ ./$(ODIR)/tests.out
+
+$(ODIR)/%.o: $(SHARE)/%.c $(DEPS)
+ mkdir -p $(basename $@)
+ $(CC) -c -o $@ $< $(CFLAGS) $(LIBS)
+
+$(ODIR)/%.o: %.c $(DEPS)
+ $(CC) -c -o $@ $< $(CFLAGS) $(LIBS)
+
+$(ODIR)/tests.out: $(OBJ)
+ gcc -o $@ $^ $(LIBS)
+
+.PHONE: clean
+clean:
+ find obj/ -iname \*.o -delete
diff --git a/src/plugins/e-acsl/tests/check/check_e_acsl_bittree.c b/src/plugins/e-acsl/tests/check/check_e_acsl_bittree.c
new file mode 100644
index 00000000000..ad9c32959be
--- /dev/null
+++ b/src/plugins/e-acsl/tests/check/check_e_acsl_bittree.c
@@ -0,0 +1,84 @@
+#include <check.h>
+#include <stdio.h>
+#include <math.h>
+
+#include "../../share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+#include "../../share/e-acsl/memory_model/e_acsl_bittree.h"
+
+START_TEST (bittree_size_zero)
+{
+
+ struct _block bk1 = {.ptr = 1, .size = 0};
+
+ __add_element(&bk1);
+ ck_assert_ptr_eq(__get_cont((void*)0), NULL);
+ ck_assert_ptr_eq(__get_cont((void*)1), &bk1);
+ ck_assert_ptr_eq(__get_cont((void*)2), NULL);
+}
+END_TEST
+
+START_TEST (bittree_adjacent_simple)
+{
+
+ struct _block bk1 = {.ptr = 1, .size = 1};
+ __add_element(&bk1);
+ ck_assert_ptr_eq(__get_cont((void*)0), NULL);
+ ck_assert_ptr_eq(__get_cont((void*)1), &bk1);
+ ck_assert_ptr_eq(__get_cont((void*)2), NULL);
+}
+END_TEST
+
+START_TEST (bittree_adjacent)
+{
+ struct _block bk1 = {.ptr = 4, .size = 4};
+ struct _block bk2 = {.ptr = 8, .size = 4};
+ struct _block bk3 = {.ptr = 16, .size = 4};
+
+ __add_element(&bk1);
+ __add_element(&bk2);
+ __add_element(&bk3);
+
+ struct _block *att_res[20] = {
+ NULL, NULL, NULL, NULL,
+ &bk1, &bk1, &bk1, &bk1,
+ &bk2, &bk2, &bk2, &bk2,
+ NULL, NULL, NULL, NULL,
+ &bk3, &bk3, &bk3, &bk3
+ };
+
+ for (uintptr_t i = 0; i < 20; i++) {
+ ck_assert_ptr_eq(__get_cont((void*)i), att_res[i]);
+ }
+
+ __remove_element(&bk1);
+ __remove_element(&bk2);
+ __remove_element(&bk3);
+}
+END_TEST
+
+Suite *
+gen_suite (void)
+{
+ Suite *s = suite_create ("Gen");
+
+ /* Core test case */
+ TCase *tc_core = tcase_create ("tests");
+ tcase_add_test (tc_core, bittree_size_zero);
+ tcase_add_test (tc_core, bittree_adjacent_simple);
+ tcase_add_test (tc_core, bittree_adjacent);
+ suite_add_tcase (s, tc_core);
+
+ return s;
+}
+
+int
+main (void)
+{
+ int number_failed;
+ Suite *s = gen_suite ();
+ SRunner *sr = srunner_create (s);
+ srunner_run_all (sr, CK_ENV);
+ number_failed = srunner_ntests_failed (sr);
+ srunner_free (sr);
+ return (number_failed == 0) ? EXIT_SUCCESS : EXIT_FAILURE;
+}
--
GitLab