diff --git a/src/plugins/override_std/Makefile.in b/src/plugins/override_std/Makefile.in index 9d9ab06f2dbc636525c392bae06c82a36f309b91..657670937086607c7d9844eb09bdcfa5de1c06d4 100644 --- a/src/plugins/override_std/Makefile.in +++ b/src/plugins/override_std/Makefile.in @@ -41,7 +41,7 @@ PLUGIN_CMO := options transform override_table basic_blocks memcpy memcmp memmov PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE) PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure #PLUGIN_NO_DEFAULT_TEST := no -PLUGIN_TESTS_DIRS := +PLUGIN_TESTS_DIRS := functions ################ # Generic part # diff --git a/src/plugins/override_std/tests/functions/memcmp.c b/src/plugins/override_std/tests/functions/memcmp.c new file mode 100644 index 0000000000000000000000000000000000000000..1da39df89a53462b2d9767208cebbd72b44acca0 --- /dev/null +++ b/src/plugins/override_std/tests/functions/memcmp.c @@ -0,0 +1,8 @@ +#include <string.h> + +int main(void){ + int s1[10] = { 0 } ; + int s2[10] = { 0 }; + + int res = memcmp(s1, s2, sizeof(s1)); +} \ No newline at end of file diff --git a/src/plugins/override_std/tests/functions/memcpy.c b/src/plugins/override_std/tests/functions/memcpy.c new file mode 100644 index 0000000000000000000000000000000000000000..7dda713ac6d1c8212fb18bce80edd245e16bace3 --- /dev/null +++ b/src/plugins/override_std/tests/functions/memcpy.c @@ -0,0 +1,8 @@ +#include <string.h> + +int main(void){ + int src[10] = { 0 } ; + int dest[10] ; + + int *p = memcpy(dest, src, sizeof(src)); +} \ No newline at end of file diff --git a/src/plugins/override_std/tests/functions/memmove.c b/src/plugins/override_std/tests/functions/memmove.c new file mode 100644 index 0000000000000000000000000000000000000000..33338d2d312753e8b519e16aa7657765da2d7f64 --- /dev/null +++ b/src/plugins/override_std/tests/functions/memmove.c @@ -0,0 +1,8 @@ +#include <string.h> + +int main(void){ + int src[10] = { 0 } ; + int dest[10] ; + + int *p = memmove(dest, src, sizeof(src)); +} \ No newline at end of file diff --git a/src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle b/src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..7ece1fdb38954432441e08ccc48f8a48cabbc28c --- /dev/null +++ b/src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle @@ -0,0 +1,74 @@ +[kernel] Parsing tests/functions/memcmp.c (with preprocessing) +/* Generated by Frama-C */ +#include "stddef.h" +#include "string.h" +#include "strings.h" +/*@ requires aligned_end: len % 4 ≡ 0; + requires + valid_read_s1: + \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1)); + requires + valid_read_s2: + \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1)); + ensures + equals: + \let __fc_len = len / 4; + \result ≡ 0 ⇔ + (∀ ℤ j; 0 ≤ j < __fc_len ⇒ *(s1 + j) ≡ *(s2 + j)); + assigns \result; + assigns \result + \from (indirect: *(s1 + (0 .. len - 1))), + (indirect: *(s2 + (0 .. len - 1))); + */ +int memcmp_int(int const *s1, int const *s2, size_t len); + +int main(void) +{ + int __retres; + int s1[10] = {0}; + int s2[10] = {0}; + int res = memcmp_int(s1,s2,sizeof(s1)); + __retres = 0; + return __retres; +} + + +[kernel] Parsing tests/functions/result/memcmp.c (with preprocessing) +[kernel] Parsing tests/functions/memcmp.c (with preprocessing) +[kernel] tests/functions/memcmp.c:3: Warning: + def'n of func main at tests/functions/memcmp.c:3 (sum 2855) conflicts with the one at tests/functions/result/memcmp.c:24 (sum 4629); keeping the one at tests/functions/result/memcmp.c:24. +/* Generated by Frama-C */ +#include "stddef.h" +#include "string.h" +#include "strings.h" +/*@ requires aligned_end: len % 4 ≡ 0; + requires + valid_read_s1: + \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1)); + requires + valid_read_s2: + \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1)); + ensures + equals: + \let __fc_len = \old(len) / 4; + \result ≡ 0 ⇔ + (∀ ℤ j; + 0 ≤ j < __fc_len ⇒ *(\old(s1) + j) ≡ *(\old(s2) + j)); + assigns \result; + assigns \result + \from (indirect: *(s1 + (0 .. len - 1))), + (indirect: *(s2 + (0 .. len - 1))); + */ +int memcmp_int(int const *s1, int const *s2, size_t len); + +int main(void) +{ + int __retres; + int s1[10] = {0}; + int s2[10] = {0}; + int res = memcmp_int((int const *)(s1),(int const *)(s2),sizeof(s1)); + __retres = 0; + return __retres; +} + + diff --git a/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle b/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..974fd3a31a232e95e8f4731e4293fe2f5b4e7d1e --- /dev/null +++ b/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle @@ -0,0 +1,76 @@ +[kernel] Parsing tests/functions/memcpy.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; + ∀ ℤ j; 0 ≤ j < __fc_len ⇒ *(dest + j) ≡ *(src + j); + 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 main(void) +{ + int __retres; + int dest[10]; + int src[10] = {0}; + int *p = memcpy_int(dest,src,sizeof(src)); + __retres = 0; + return __retres; +} + + +[kernel] Parsing tests/functions/result/memcpy.c (with preprocessing) +[kernel] Parsing tests/functions/memcpy.c (with preprocessing) +[kernel] tests/functions/memcpy.c:3: Warning: + def'n of func main at tests/functions/memcpy.c:3 (sum 1968) conflicts with the one at tests/functions/result/memcpy.c:25 (sum 3742); keeping the one at tests/functions/result/memcpy.c:25. +/* 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 = \old(len) / 4; + ∀ ℤ j; + 0 ≤ j < __fc_len ⇒ *(\old(dest) + j) ≡ *(\old(src) + j); + 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 main(void) +{ + int __retres; + int dest[10]; + int src[10] = {0}; + int *p = memcpy_int(dest,(int const *)(src),sizeof(src)); + __retres = 0; + return __retres; +} + + diff --git a/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle b/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..d922f913cad2e7c1e0aa7f363a03dd96a1b81fb3 --- /dev/null +++ b/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle @@ -0,0 +1,68 @@ +[kernel] Parsing tests/functions/memmove.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)); + ensures + moved: + \let __fc_len = len / 4; + ∀ ℤ j; 0 ≤ j < __fc_len ⇒ *(dest + j) ≡ \at(*(src + j),Pre); + assigns *(dest + (0 .. len - 1)), \result; + assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1)); + assigns \result \from dest; + */ +int *memmove_int(int *dest, int const *src, size_t len); + +int main(void) +{ + int __retres; + int dest[10]; + int src[10] = {0}; + int *p = memmove_int(dest,src,sizeof(src)); + __retres = 0; + return __retres; +} + + +[kernel] Parsing tests/functions/result/memmove.c (with preprocessing) +[kernel] Parsing tests/functions/memmove.c (with preprocessing) +[kernel] tests/functions/memmove.c:3: Warning: + def'n of func main at tests/functions/memmove.c:3 (sum 1968) conflicts with the one at tests/functions/result/memmove.c:21 (sum 3742); keeping the one at tests/functions/result/memmove.c:21. +/* 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)); + ensures + moved: + \let __fc_len = \old(len) / 4; + ∀ ℤ j; + 0 ≤ j < __fc_len ⇒ *(\old(dest) + j) ≡ \at(*(src + j),Pre); + assigns *(dest + (0 .. len - 1)), \result; + assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1)); + assigns \result \from dest; + */ +int *memmove_int(int *dest, int const *src, size_t len); + +int main(void) +{ + int __retres; + int dest[10]; + int src[10] = {0}; + int *p = memmove_int(dest,(int const *)(src),sizeof(src)); + __retres = 0; + return __retres; +} + + diff --git a/src/plugins/override_std/tests/test_config b/src/plugins/override_std/tests/test_config new file mode 100644 index 0000000000000000000000000000000000000000..ac3b92b43ff97c69d2b381fc3f4591cba41b738e --- /dev/null +++ b/src/plugins/override_std/tests/test_config @@ -0,0 +1 @@ +OPT: @PTEST_FILE@ -override-std -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print \ No newline at end of file