diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore index 3ccc328577bdc92ea5995d33e33a03852983c04f..d7240f5a42400374ac71544ccce2d9f6eca48e3e 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 7210380aca5660baf0847e8a02bf366ea6f963da..7734389a2c9b2104ece76cf330ecb6d15562b47a 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 dd90b193a0e3bf612ae301a6b99ddac97a631073..d0329d4052f07a014449da47616d753eb5f7df70 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 0000000000000000000000000000000000000000..3067f390e08e5734fa298880688c350a6703fefd --- /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 0000000000000000000000000000000000000000..ad9c32959be5d082828c3ae20c58ce9d150e25dd --- /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; +}