From fb8234bf5c4427e1c82673cbb99ffc622ac95746 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 22 Oct 2019 11:06:31 +0200
Subject: [PATCH] [Builtin] Tests more types
---
src/plugins/builtin/tests/functions/memcmp.c | 30 ++-
src/plugins/builtin/tests/functions/memcpy.c | 35 ++-
src/plugins/builtin/tests/functions/memmove.c | 35 ++-
.../tests/functions/oracle/memcmp.res.oracle | 189 ++++++++++++++--
.../tests/functions/oracle/memcpy.res.oracle | 206 ++++++++++++++++--
.../tests/functions/oracle/memmove.res.oracle | 190 ++++++++++++++--
6 files changed, 609 insertions(+), 76 deletions(-)
diff --git a/src/plugins/builtin/tests/functions/memcmp.c b/src/plugins/builtin/tests/functions/memcmp.c
index 67d1b22a579..8a0b48622a6 100644
--- a/src/plugins/builtin/tests/functions/memcmp.c
+++ b/src/plugins/builtin/tests/functions/memcmp.c
@@ -1,12 +1,28 @@
#include <string.h>
-int main(void){
- int s1[10] = { 0 } ;
- int s2[10] = { 0 };
+struct X {
+ int x ;
+ int y ;
+} ;
- int res = memcmp(s1, s2, sizeof(s1));
+typedef int named ;
+
+int integer(int src[10], int dest[10]){
+ return memcmp(dest, src, 10 * sizeof(int));
+}
+
+int with_named(named src[10], named dest[10]){
+ return memcmp(dest, src, 10 * sizeof(named));
+}
+
+int structure(struct X src[10], struct X dest[10]){
+ return memcmp(dest, src, 10 * sizeof(struct X));
+}
+
+int pointers(int* src[10], int* dest[10]){
+ return memcmp(dest, src, 10 * sizeof(int*));
}
-int nested(int (*dest) [10], int (*src) [10], size_t n){
- return memcmp(dest, src, n) ;
-}
\ No newline at end of file
+int nested(int (*src)[10], int (*dest)[10], int n){
+ return memcmp(dest, src, n * sizeof(int[10]));
+}
diff --git a/src/plugins/builtin/tests/functions/memcpy.c b/src/plugins/builtin/tests/functions/memcpy.c
index 7264434129d..ed3022f3718 100644
--- a/src/plugins/builtin/tests/functions/memcpy.c
+++ b/src/plugins/builtin/tests/functions/memcpy.c
@@ -1,12 +1,33 @@
#include <string.h>
-int main(void){
- int src[10] = { 0 } ;
- int dest[10] ;
+struct X {
+ int x ;
+ int y ;
+} ;
- int *p = memcpy(dest, src, sizeof(src));
+typedef int named ;
+
+void integer(int src[10], int dest[10]){
+ int * res = memcpy(dest, src, 10 * sizeof(int));
+ memcpy(src, res, 10 * sizeof(int));
+}
+
+void with_named(named src[10], named dest[10]){
+ named * res = memcpy(dest, src, 10 * sizeof(named));
+ memcpy(src, res, 10 * sizeof(named));
+}
+
+void structure(struct X src[10], struct X dest[10]){
+ struct X * res = memcpy(dest, src, 10 * sizeof(struct X));
+ memcpy(src, res, 10 * sizeof(struct X));
+}
+
+void pointers(int* src[10], int* dest[10]){
+ int ** res = memcpy(dest, src, 10 * sizeof(int*));
+ memcpy(src, res, 10 * sizeof(int*));
}
-void nested(int (*dest) [10], int (*src) [10], size_t n){
- memcpy(dest, src, n) ;
-}
\ No newline at end of file
+void nested(int (*src)[10], int (*dest)[10], int n){
+ int (*res) [10] = memcpy(dest, src, n * sizeof(int[10]));
+ memcpy(src, res, n * sizeof(int[10]));
+}
diff --git a/src/plugins/builtin/tests/functions/memmove.c b/src/plugins/builtin/tests/functions/memmove.c
index 7a17026266d..3944ba03563 100644
--- a/src/plugins/builtin/tests/functions/memmove.c
+++ b/src/plugins/builtin/tests/functions/memmove.c
@@ -1,12 +1,33 @@
#include <string.h>
-int main(void){
- int src[10] = { 0 } ;
- int dest[10] ;
+struct X {
+ int x ;
+ int y ;
+} ;
- int *p = memmove(dest, src, sizeof(src));
+typedef int named ;
+
+void integer(int src[10], int dest[10]){
+ int * res = memmove(dest, src, 10 * sizeof(int));
+ memmove(src, res, 10 * sizeof(int));
+}
+
+void with_named(named src[10], named dest[10]){
+ named * res = memmove(dest, src, 10 * sizeof(named));
+ memmove(src, res, 10 * sizeof(named));
+}
+
+void structure(struct X src[10], struct X dest[10]){
+ struct X * res = memmove(dest, src, 10 * sizeof(struct X));
+ memmove(src, res, 10 * sizeof(struct X));
+}
+
+void pointers(int* src[10], int* dest[10]){
+ int ** res = memmove(dest, src, 10 * sizeof(int*));
+ memmove(src, res, 10 * sizeof(int*));
}
-void nested(int (*dest) [10], int (*src) [10], size_t n) {
- memmove(dest, src, n) ;
-}
\ No newline at end of file
+void nested(int (*src)[10], int (*dest)[10], int n){
+ int (*res) [10] = memmove(dest, src, n * sizeof(int[10]));
+ memmove(src, res, n * sizeof(int[10]));
+}
diff --git a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle b/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
index 77e86fe5a03..b0d88d0280a 100644
--- a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
@@ -3,6 +3,11 @@
#include "stddef.h"
#include "string.h"
#include "strings.h"
+struct X {
+ int x ;
+ int y ;
+};
+typedef int named;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
@@ -27,16 +32,82 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
return __retres;
}
-int main(void)
+int integer(int * /*[10]*/ src, int * /*[10]*/ dest)
+{
+ int tmp;
+ tmp = memcmp_int(dest,src,(unsigned int)10 * sizeof(int));
+ return tmp;
+}
+
+int with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
+{
+ int tmp;
+ tmp = memcmp_int(dest,src,(unsigned int)10 * sizeof(named));
+ return tmp;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+ requires
+ valid_read_s1:
+ \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
+ requires
+ valid_read_s2:
+ \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
+ ensures
+ equals:
+ \let __fc_len = len / 8;
+ \result ≡ 0 ⇔
+ (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
+ assigns \result;
+ assigns \result
+ \from (indirect: *(s1 + (0 .. len - 1))),
+ (indirect: *(s2 + (0 .. len - 1)));
+ */
+int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
+{
+ int __retres;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
+ return __retres;
+}
+
+int structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+{
+ int tmp;
+ tmp = memcmp_X(dest,src,(unsigned int)10 * sizeof(struct X));
+ return tmp;
+}
+
+/*@ 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 ⇔
+ (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
+ assigns \result;
+ assigns \result
+ \from (indirect: *(s1 + (0 .. len - 1))),
+ (indirect: *(s2 + (0 .. len - 1)));
+ */
+int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{
int __retres;
- int s1[10] = {0};
- int s2[10] = {0};
- int res = memcmp_int(s1,s2,sizeof(s1));
- __retres = 0;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
return __retres;
}
+int pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+{
+ int tmp;
+ tmp = memcmp_ptr_int(dest,src,(unsigned int)10 * sizeof(int *));
+ return tmp;
+}
+
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_read_s1:
@@ -64,24 +135,35 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
return __retres;
}
-int nested(int (*dest)[10], int (*src)[10], size_t n)
+int nested(int (*src)[10], int (*dest)[10], int n)
{
int tmp;
- tmp = memcmp_arr10_int(dest,src,n);
+ tmp = memcmp_arr10_int(dest,src,(unsigned int)n * sizeof(int [10]));
return tmp;
}
[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:29 (sum 4629); keeping the one at tests/functions/result/memcmp.c:29.
[kernel] tests/functions/memcmp.c:10: Warning:
- def'n of func nested at tests/functions/memcmp.c:10 (sum 1087) conflicts with the one at tests/functions/result/memcmp.c:66 (sum 1974); keeping the one at tests/functions/result/memcmp.c:66.
+ def'n of func integer at tests/functions/memcmp.c:10 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:34 (sum 1972); keeping the one at tests/functions/result/memcmp.c:34.
+[kernel] tests/functions/memcmp.c:14: Warning:
+ def'n of func with_named at tests/functions/memcmp.c:14 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:41 (sum 1972); keeping the one at tests/functions/result/memcmp.c:41.
+[kernel] tests/functions/memcmp.c:18: Warning:
+ def'n of func structure at tests/functions/memcmp.c:18 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:72 (sum 1972); keeping the one at tests/functions/result/memcmp.c:72.
+[kernel] tests/functions/memcmp.c:22: Warning:
+ def'n of func pointers at tests/functions/memcmp.c:22 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:103 (sum 1972); keeping the one at tests/functions/result/memcmp.c:103.
+[kernel] tests/functions/memcmp.c:26: Warning:
+ def'n of func nested at tests/functions/memcmp.c:26 (sum 1087) conflicts with the one at tests/functions/result/memcmp.c:137 (sum 1974); keeping the one at tests/functions/result/memcmp.c:137.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
+struct X {
+ int x ;
+ int y ;
+};
+typedef int named;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
@@ -107,16 +189,88 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
return __retres;
}
-int main(void)
+int integer(int *src, int *dest)
+{
+ int tmp;
+ tmp = memcmp_int((int const *)dest,(int const *)src,
+ (unsigned int)10 * sizeof(int));
+ return tmp;
+}
+
+int with_named(named *src, named *dest)
+{
+ int tmp;
+ tmp = memcmp_int((int const *)dest,(int const *)src,
+ (unsigned int)10 * sizeof(named));
+ return tmp;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+ requires
+ valid_read_s1:
+ \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
+ requires
+ valid_read_s2:
+ \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
+ ensures
+ equals:
+ \let __fc_len = \old(len) / 8;
+ \result ≡ 0 ⇔
+ (∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
+ assigns \result;
+ assigns \result
+ \from (indirect: *(s1 + (0 .. len - 1))),
+ (indirect: *(s2 + (0 .. len - 1)));
+ */
+int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
+{
+ int __retres;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
+ return __retres;
+}
+
+int structure(struct X *src, struct X *dest)
+{
+ int tmp;
+ tmp = memcmp_X((struct X const *)dest,(struct X const *)src,
+ (unsigned int)10 * sizeof(struct X));
+ return tmp;
+}
+
+/*@ 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 ⇔
+ (∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
+ assigns \result;
+ assigns \result
+ \from (indirect: *(s1 + (0 .. len - 1))),
+ (indirect: *(s2 + (0 .. len - 1)));
+ */
+int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{
int __retres;
- int s1[10] = {0};
- int s2[10] = {0};
- int res = memcmp_int((int const *)(s1),(int const *)(s2),sizeof(s1));
- __retres = 0;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
return __retres;
}
+int pointers(int **src, int **dest)
+{
+ int tmp;
+ tmp = memcmp_ptr_int((int * const *)dest,(int * const *)src,
+ (unsigned int)10 * sizeof(int *));
+ return tmp;
+}
+
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_read_s1:
@@ -145,10 +299,11 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
return __retres;
}
-int nested(int (*dest)[10], int (*src)[10], size_t n)
+int nested(int (*src)[10], int (*dest)[10], int n)
{
int tmp;
- tmp = memcmp_arr10_int((int const (*)[10])dest,(int const (*)[10])src,n);
+ tmp = memcmp_arr10_int((int const (*)[10])dest,(int const (*)[10])src,
+ (unsigned int)n * sizeof(int [10]));
return tmp;
}
diff --git a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle b/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
index 7c8012b7448..b29798e2515 100644
--- a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
@@ -3,6 +3,11 @@
#include "stddef.h"
#include "string.h"
#include "strings.h"
+struct X {
+ int x ;
+ int y ;
+};
+typedef int named;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -29,16 +34,86 @@ int *memcpy_int(int *dest, int const *src, size_t len)
return __retres;
}
-int main(void)
+void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
{
- int __retres;
- int dest[10];
- int src[10] = {0};
- int *p = memcpy_int(dest,src,sizeof(src));
- __retres = 0;
+ int *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(int));
+ memcpy_int(src,res,(unsigned int)10 * sizeof(int));
+ return;
+}
+
+void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
+{
+ named *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(named));
+ memcpy_int(src,res,(unsigned int)10 * sizeof(named));
+ return;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
+ requires
+ valid_read_src:
+ \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
+ requires
+ separation:
+ \let __fc_len = len / 8;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ ensures
+ copied:
+ \let __fc_len = len / 8;
+ ∀ ℤ 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;
+ */
+struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
+{
+ struct X *__retres;
+ __retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
+ return __retres;
+}
+
+void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+{
+ struct X *res = memcpy_X(dest,src,(unsigned int)10 * sizeof(struct X));
+ memcpy_X(src,res,(unsigned int)10 * sizeof(struct X));
+ 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_ptr_int(int **dest, int * const *src, size_t len)
+{
+ int **__retres;
+ __retres = (int **)memcpy((void *)dest,(void const *)src,len);
return __retres;
}
+void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+{
+ int **res = memcpy_ptr_int(dest,src,(unsigned int)10 * sizeof(int *));
+ memcpy_ptr_int(src,res,(unsigned int)10 * sizeof(int *));
+ return;
+}
+
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
@@ -70,23 +145,36 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
return __retres;
}
-void nested(int (*dest)[10], int (*src)[10], size_t n)
+void nested(int (*src)[10], int (*dest)[10], int n)
{
- memcpy_arr10_int(dest,src,n);
+ int (*res)[10] =
+ memcpy_arr10_int(dest,src,(unsigned int)n * sizeof(int [10]));
+ memcpy_arr10_int(src,res,(unsigned int)n * sizeof(int [10]));
return;
}
[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:31 (sum 3742); keeping the one at tests/functions/result/memcpy.c:31.
[kernel] tests/functions/memcpy.c:10: Warning:
- dropping duplicate def'n of func nested at tests/functions/memcpy.c:10 in favor of that at tests/functions/result/memcpy.c:72
+ dropping duplicate def'n of func integer at tests/functions/memcpy.c:10 in favor of that at tests/functions/result/memcpy.c:36
+[kernel] tests/functions/memcpy.c:15: Warning:
+ dropping duplicate def'n of func with_named at tests/functions/memcpy.c:15 in favor of that at tests/functions/result/memcpy.c:43
+[kernel] tests/functions/memcpy.c:20: Warning:
+ dropping duplicate def'n of func structure at tests/functions/memcpy.c:20 in favor of that at tests/functions/result/memcpy.c:76
+[kernel] tests/functions/memcpy.c:25: Warning:
+ dropping duplicate def'n of func pointers at tests/functions/memcpy.c:25 in favor of that at tests/functions/result/memcpy.c:109
+[kernel] tests/functions/memcpy.c:30: Warning:
+ dropping duplicate def'n of func nested at tests/functions/memcpy.c:30 in favor of that at tests/functions/result/memcpy.c:147
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
+struct X {
+ int x ;
+ int y ;
+};
+typedef int named;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -114,16 +202,92 @@ int *memcpy_int(int *dest, int const *src, size_t len)
return __retres;
}
-int main(void)
+void integer(int *src, int *dest)
+{
+ int *res =
+ memcpy_int(dest,(int const *)src,(unsigned int)10 * sizeof(int));
+ memcpy_int(src,(int const *)res,(unsigned int)10 * sizeof(int));
+ return;
+}
+
+void with_named(named *src, named *dest)
+{
+ named *res =
+ memcpy_int(dest,(int const *)src,(unsigned int)10 * sizeof(named));
+ memcpy_int(src,(int const *)res,(unsigned int)10 * sizeof(named));
+ return;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
+ requires
+ valid_read_src:
+ \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
+ requires
+ separation:
+ \let __fc_len = len / 8;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ ensures
+ copied:
+ \let __fc_len = \old(len) / 8;
+ ∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
+ ensures result: \result ≡ \old(dest);
+ assigns *(dest + (0 .. len - 1)), \result;
+ assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
+ assigns \result \from dest;
+ */
+struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
+{
+ struct X *__retres;
+ __retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
+ return __retres;
+}
+
+void structure(struct X *src, struct X *dest)
+{
+ struct X *res =
+ memcpy_X(dest,(struct X const *)src,(unsigned int)10 * sizeof(struct X));
+ memcpy_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+ 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 = \old(len) / 4;
+ ∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
+ ensures result: \result ≡ \old(dest);
+ assigns *(dest + (0 .. len - 1)), \result;
+ assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
+ assigns \result \from dest;
+ */
+int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
{
- int __retres;
- int dest[10];
- int src[10] = {0};
- int *p = memcpy_int(dest,(int const *)(src),sizeof(src));
- __retres = 0;
+ int **__retres;
+ __retres = (int **)memcpy((void *)dest,(void const *)src,len);
return __retres;
}
+void pointers(int **src, int **dest)
+{
+ int **res =
+ memcpy_ptr_int(dest,(int * const *)src,(unsigned int)10 * sizeof(int *));
+ memcpy_ptr_int(src,(int * const *)res,(unsigned int)10 * sizeof(int *));
+ return;
+}
+
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
@@ -156,9 +320,13 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
return __retres;
}
-void nested(int (*dest)[10], int (*src)[10], size_t n)
+void nested(int (*src)[10], int (*dest)[10], int n)
{
- memcpy_arr10_int(dest,(int const (*)[10])src,n);
+ int (*res)[10] =
+ memcpy_arr10_int(dest,(int const (*)[10])src,
+ (unsigned int)n * sizeof(int [10]));
+ memcpy_arr10_int(src,(int const (*)[10])res,
+ (unsigned int)n * sizeof(int [10]));
return;
}
diff --git a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle b/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
index e6c64844a25..43e53fcefa4 100644
--- a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
@@ -3,6 +3,11 @@
#include "stddef.h"
#include "string.h"
#include "strings.h"
+struct X {
+ int x ;
+ int y ;
+};
+typedef int named;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -25,16 +30,78 @@ int *memmove_int(int *dest, int const *src, size_t len)
return __retres;
}
-int main(void)
+void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
{
- int __retres;
- int dest[10];
- int src[10] = {0};
- int *p = memmove_int(dest,src,sizeof(src));
- __retres = 0;
+ int *res = memmove_int(dest,src,(unsigned int)10 * sizeof(int));
+ memmove_int(src,res,(unsigned int)10 * sizeof(int));
+ return;
+}
+
+void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
+{
+ named *res = memmove_int(dest,src,(unsigned int)10 * sizeof(named));
+ memmove_int(src,res,(unsigned int)10 * sizeof(named));
+ return;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
+ requires
+ valid_read_src:
+ \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
+ ensures
+ moved:
+ \let __fc_len = len / 8;
+ ∀ ℤ 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;
+ */
+struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
+{
+ struct X *__retres;
+ __retres = (struct X *)memmove((void *)dest,(void const *)src,len);
return __retres;
}
+void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+{
+ struct X *res = memmove_X(dest,src,(unsigned int)10 * sizeof(struct X));
+ memmove_X(src,res,(unsigned int)10 * sizeof(struct X));
+ 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));
+ ensures
+ moved:
+ \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 **memmove_ptr_int(int **dest, int * const *src, size_t len)
+{
+ int **__retres;
+ __retres = (int **)memmove((void *)dest,(void const *)src,len);
+ return __retres;
+}
+
+void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+{
+ int **res = memmove_ptr_int(dest,src,(unsigned int)10 * sizeof(int *));
+ memmove_ptr_int(src,res,(unsigned int)10 * sizeof(int *));
+ return;
+}
+
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
@@ -62,23 +129,36 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
return __retres;
}
-void nested(int (*dest)[10], int (*src)[10], size_t n)
+void nested(int (*src)[10], int (*dest)[10], int n)
{
- memmove_arr10_int(dest,src,n);
+ int (*res)[10] =
+ memmove_arr10_int(dest,src,(unsigned int)n * sizeof(int [10]));
+ memmove_arr10_int(src,res,(unsigned int)n * sizeof(int [10]));
return;
}
[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:27 (sum 3742); keeping the one at tests/functions/result/memmove.c:27.
[kernel] tests/functions/memmove.c:10: Warning:
- dropping duplicate def'n of func nested at tests/functions/memmove.c:10 in favor of that at tests/functions/result/memmove.c:64
+ dropping duplicate def'n of func integer at tests/functions/memmove.c:10 in favor of that at tests/functions/result/memmove.c:32
+[kernel] tests/functions/memmove.c:15: Warning:
+ dropping duplicate def'n of func with_named at tests/functions/memmove.c:15 in favor of that at tests/functions/result/memmove.c:39
+[kernel] tests/functions/memmove.c:20: Warning:
+ dropping duplicate def'n of func structure at tests/functions/memmove.c:20 in favor of that at tests/functions/result/memmove.c:68
+[kernel] tests/functions/memmove.c:25: Warning:
+ dropping duplicate def'n of func pointers at tests/functions/memmove.c:25 in favor of that at tests/functions/result/memmove.c:97
+[kernel] tests/functions/memmove.c:30: Warning:
+ dropping duplicate def'n of func nested at tests/functions/memmove.c:30 in favor of that at tests/functions/result/memmove.c:131
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
+struct X {
+ int x ;
+ int y ;
+};
+typedef int named;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -102,16 +182,84 @@ int *memmove_int(int *dest, int const *src, size_t len)
return __retres;
}
-int main(void)
+void integer(int *src, int *dest)
+{
+ int *res =
+ memmove_int(dest,(int const *)src,(unsigned int)10 * sizeof(int));
+ memmove_int(src,(int const *)res,(unsigned int)10 * sizeof(int));
+ return;
+}
+
+void with_named(named *src, named *dest)
+{
+ named *res =
+ memmove_int(dest,(int const *)src,(unsigned int)10 * sizeof(named));
+ memmove_int(src,(int const *)res,(unsigned int)10 * sizeof(named));
+ return;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+ requires
+ valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
+ requires
+ valid_read_src:
+ \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
+ ensures
+ moved:
+ \let __fc_len = \old(len) / 8;
+ ∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
+ ensures result: \result ≡ \old(dest);
+ assigns *(dest + (0 .. len - 1)), \result;
+ assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
+ assigns \result \from dest;
+ */
+struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
+{
+ struct X *__retres;
+ __retres = (struct X *)memmove((void *)dest,(void const *)src,len);
+ return __retres;
+}
+
+void structure(struct X *src, struct X *dest)
{
- int __retres;
- int dest[10];
- int src[10] = {0};
- int *p = memmove_int(dest,(int const *)(src),sizeof(src));
- __retres = 0;
+ struct X *res =
+ memmove_X(dest,(struct X const *)src,(unsigned int)10 * sizeof(struct X));
+ memmove_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+ 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));
+ ensures
+ moved:
+ \let __fc_len = \old(len) / 4;
+ ∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
+ ensures result: \result ≡ \old(dest);
+ assigns *(dest + (0 .. len - 1)), \result;
+ assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
+ assigns \result \from dest;
+ */
+int **memmove_ptr_int(int **dest, int * const *src, size_t len)
+{
+ int **__retres;
+ __retres = (int **)memmove((void *)dest,(void const *)src,len);
return __retres;
}
+void pointers(int **src, int **dest)
+{
+ int **res =
+ memmove_ptr_int(dest,(int * const *)src,(unsigned int)10 * sizeof(int *));
+ memmove_ptr_int(src,(int * const *)res,(unsigned int)10 * sizeof(int *));
+ return;
+}
+
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
@@ -140,9 +288,13 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
return __retres;
}
-void nested(int (*dest)[10], int (*src)[10], size_t n)
+void nested(int (*src)[10], int (*dest)[10], int n)
{
- memmove_arr10_int(dest,(int const (*)[10])src,n);
+ int (*res)[10] =
+ memmove_arr10_int(dest,(int const (*)[10])src,
+ (unsigned int)n * sizeof(int [10]));
+ memmove_arr10_int(src,(int const (*)[10])res,
+ (unsigned int)n * sizeof(int [10]));
return;
}
--
GitLab