From 86acae470f39a77eef1d91598e40a8ef8ab9ad32 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Sep 2019 11:07:07 +0200
Subject: [PATCH] [Override Std] Some tests for the generated contracts
---
src/plugins/override_std/Makefile.in | 2 +-
.../override_std/tests/functions/memcmp.c | 8 ++
.../override_std/tests/functions/memcpy.c | 8 ++
.../override_std/tests/functions/memmove.c | 8 ++
.../tests/functions/oracle/memcmp.res.oracle | 74 ++++++++++++++++++
.../tests/functions/oracle/memcpy.res.oracle | 76 +++++++++++++++++++
.../tests/functions/oracle/memmove.res.oracle | 68 +++++++++++++++++
src/plugins/override_std/tests/test_config | 1 +
8 files changed, 244 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/override_std/tests/functions/memcmp.c
create mode 100644 src/plugins/override_std/tests/functions/memcpy.c
create mode 100644 src/plugins/override_std/tests/functions/memmove.c
create mode 100644 src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle
create mode 100644 src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle
create mode 100644 src/plugins/override_std/tests/functions/oracle/memmove.res.oracle
create mode 100644 src/plugins/override_std/tests/test_config
diff --git a/src/plugins/override_std/Makefile.in b/src/plugins/override_std/Makefile.in
index 9d9ab06f2db..65767093708 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 00000000000..1da39df89a5
--- /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 00000000000..7dda713ac6d
--- /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 00000000000..33338d2d312
--- /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 00000000000..7ece1fdb389
--- /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 00000000000..974fd3a31a2
--- /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 00000000000..d922f913cad
--- /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 00000000000..ac3b92b43ff
--- /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
--
GitLab