diff --git a/src/plugins/builtin/Makefile.in b/src/plugins/builtin/Makefile.in index c2c0f929c77c68ea118e7390ce3270ca12144c4f..70d49bb5ece3f3ea9d4473edf61478d8ea6a79e1 100644 --- a/src/plugins/builtin/Makefile.in +++ b/src/plugins/builtin/Makefile.in @@ -36,14 +36,14 @@ endif PLUGIN_DIR ?= . PLUGIN_ENABLE := @ENABLE_BUILTIN@ PLUGIN_NAME := Builtin -PLUGIN_CMI := +PLUGIN_CMI := PLUGIN_CMO := basic_blocks options builtin_builder transform \ memcpy memcmp memmove memset \ register PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE) PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure #PLUGIN_NO_DEFAULT_TEST := no -PLUGIN_TESTS_DIRS := functions +PLUGIN_TESTS_DIRS := functions options ################ # Generic part # diff --git a/src/plugins/builtin/tests/test_config b/src/plugins/builtin/tests/functions/test_config similarity index 100% rename from src/plugins/builtin/tests/test_config rename to src/plugins/builtin/tests/functions/test_config diff --git a/src/plugins/builtin/tests/options/ignore-builtin.c b/src/plugins/builtin/tests/options/ignore-builtin.c new file mode 100644 index 0000000000000000000000000000000000000000..e9312d8ec9865418337ac99d6c5d9dc09f1460cc --- /dev/null +++ b/src/plugins/builtin/tests/options/ignore-builtin.c @@ -0,0 +1,12 @@ +/* run.config + STDOPT:+"-builtin-no-memcpy" +*/ + +#include <string.h> + +void foo(){ + int src[10] ; + int dest[10] ; + memset(src, 0, sizeof(src)) ; + memcpy(dest, src, sizeof(src)) ; +} \ No newline at end of file diff --git a/src/plugins/builtin/tests/options/ignore-functions.c b/src/plugins/builtin/tests/options/ignore-functions.c new file mode 100644 index 0000000000000000000000000000000000000000..5cec9a3a2ee31294dd14f1546a8fa76bca3cea95 --- /dev/null +++ b/src/plugins/builtin/tests/options/ignore-functions.c @@ -0,0 +1,23 @@ +/* run.config + STDOPT: +"-builtin-fct=@all,-foo" +*/ + +#include <string.h> + +void foo(){ + int src[10] = {0} ; + int dest[10] ; + memcpy(dest, src, sizeof(src)) ; +} + +void bar(){ + int src[10] = {0} ; + int dest[10] ; + memcpy(dest, src, sizeof(src)) ; +} + +void baz(){ + int src[10] = {0} ; + int dest[10] ; + memcpy(dest, src, sizeof(src)) ; +} \ No newline at end of file diff --git a/src/plugins/builtin/tests/options/only-functions.c b/src/plugins/builtin/tests/options/only-functions.c new file mode 100644 index 0000000000000000000000000000000000000000..9ad8836a67a6f38cca18a24f1387d1d936c3ec03 --- /dev/null +++ b/src/plugins/builtin/tests/options/only-functions.c @@ -0,0 +1,23 @@ +/* run.config + STDOPT: +"-builtin-fct=foo" +*/ + +#include <string.h> + +void foo(){ + int src[10] = {0} ; + int dest[10] ; + memcpy(dest, src, sizeof(src)) ; +} + +void bar(){ + int src[10] = {0} ; + int dest[10] ; + memcpy(dest, src, sizeof(src)) ; +} + +void baz(){ + int src[10] = {0} ; + int dest[10] ; + memcpy(dest, src, sizeof(src)) ; +} \ No newline at end of file diff --git a/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle b/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..a37f9b74200c7255c87db8d50d5d9c22beba6794 --- /dev/null +++ b/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle @@ -0,0 +1,34 @@ +[kernel] Parsing tests/options/ignore-builtin.c (with preprocessing) +/* Generated by Frama-C */ +#include "stddef.h" +#include "string.h" +#include "strings.h" +/*@ requires aligned_end: num % 4 ≡ 0; + requires + valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1)); + ensures + set_content: + \let __fc_len = num / 4; + ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 0; + ensures result: \result ≡ ptr; + assigns *(ptr + (0 .. num - 1)), \result; + assigns *(ptr + (0 .. num - 1)) \from \nothing; + assigns \result \from ptr; + */ +int *memset_int_0(int *ptr, size_t num) +{ + int *__retres; + __retres = (int *)memset((void *)ptr,0,num); + return __retres; +} + +void foo(void) +{ + int src[10]; + int dest[10]; + memset_int_0(src,sizeof(src)); + memcpy((void *)(dest),(void const *)(src),sizeof(src)); + return; +} + + diff --git a/src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle b/src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..ee940654e55f18b258c25732c041fc052d140fbf --- /dev/null +++ b/src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle @@ -0,0 +1,56 @@ +[kernel] Parsing tests/options/ignore-functions.c (with preprocessing) +/* Generated by Frama-C */ +#include "stddef.h" +#include "string.h" +#include "strings.h" +void foo(void) +{ + int dest[10]; + int src[10] = {0}; + memcpy((void *)(dest),(void const *)(src),sizeof(src)); + return; +} + +/*@ requires aligned_end: len % 4 ≡ 0; + requires + valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1)); + requires + valid_read_src: + \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1)); + requires + separation: + \let __fc_len = len / 4; + \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1)); + ensures + copied: + \let __fc_len = len / 4; + ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0); + ensures result: \result ≡ dest; + assigns *(dest + (0 .. len - 1)), \result; + assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1)); + assigns \result \from dest; + */ +int *memcpy_int(int *dest, int const *src, size_t len) +{ + int *__retres; + __retres = (int *)memcpy((void *)dest,(void const *)src,len); + return __retres; +} + +void bar(void) +{ + int dest[10]; + int src[10] = {0}; + memcpy_int(dest,src,sizeof(src)); + return; +} + +void baz(void) +{ + int dest[10]; + int src[10] = {0}; + memcpy_int(dest,src,sizeof(src)); + return; +} + + diff --git a/src/plugins/builtin/tests/options/oracle/only-functions.res.oracle b/src/plugins/builtin/tests/options/oracle/only-functions.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..11b95496d169ba377d983069c571bcc57c898dea --- /dev/null +++ b/src/plugins/builtin/tests/options/oracle/only-functions.res.oracle @@ -0,0 +1,56 @@ +[kernel] Parsing tests/options/only-functions.c (with preprocessing) +/* Generated by Frama-C */ +#include "stddef.h" +#include "string.h" +#include "strings.h" +/*@ requires aligned_end: len % 4 ≡ 0; + requires + valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1)); + requires + valid_read_src: + \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1)); + requires + separation: + \let __fc_len = len / 4; + \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1)); + ensures + copied: + \let __fc_len = len / 4; + ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0); + ensures result: \result ≡ dest; + assigns *(dest + (0 .. len - 1)), \result; + assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1)); + assigns \result \from dest; + */ +int *memcpy_int(int *dest, int const *src, size_t len) +{ + int *__retres; + __retres = (int *)memcpy((void *)dest,(void const *)src,len); + return __retres; +} + +void foo(void) +{ + int dest[10]; + int src[10] = {0}; + memcpy_int(dest,src,sizeof(src)); + return; +} + +void bar(void) +{ + int dest[10]; + int src[10] = {0}; + memcpy((void *)(dest),(void const *)(src),sizeof(src)); + return; +} + +void baz(void) +{ + int dest[10]; + int src[10] = {0}; + memcpy((void *)(dest),(void const *)(src),sizeof(src)); + return; +} + + diff --git a/src/plugins/builtin/tests/options/test_config b/src/plugins/builtin/tests/options/test_config new file mode 100644 index 0000000000000000000000000000000000000000..23385de533568c5088ea4b945e39aa4c5c35e504 --- /dev/null +++ b/src/plugins/builtin/tests/options/test_config @@ -0,0 +1 @@ +OPT: @PTEST_FILE@ -builtin -print \ No newline at end of file