[Override Std] Some tests for the generated contracts

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 #

src/plugins/override_std/tests/functions/memcmp.c

+#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

src/plugins/override_std/tests/functions/memcpy.c

+#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

src/plugins/override_std/tests/functions/memmove.c

+#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

src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle

+[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;
+}
+
+

src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle

+[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;
+}
+
+

src/plugins/override_std/tests/functions/oracle/memmove.res.oracle

+[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;
+}
+
+

src/plugins/override_std/tests/test_config

+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