From fb50cf91277b93c122b52f68aeaffd246cb6f1e0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Sep 2019 14:00:08 +0200
Subject: [PATCH] [Override Std] Fix missing \result in memcpy/move
---
src/plugins/override_std/memcpy.ml | 10 +++++++---
src/plugins/override_std/memmove.ml | 10 +++++++---
.../tests/functions/oracle/memcpy.res.oracle | 4 +++-
.../tests/functions/oracle/memmove.res.oracle | 4 +++-
4 files changed, 20 insertions(+), 8 deletions(-)
diff --git a/src/plugins/override_std/memcpy.ml b/src/plugins/override_std/memcpy.ml
index b0cbffaf38c..f3a789cb2e7 100644
--- a/src/plugins/override_std/memcpy.ml
+++ b/src/plugins/override_std/memcpy.ml
@@ -46,6 +46,9 @@ let pcopied_memcpy ?loc p1 p2 len =
let pcopied_len_bytes ?loc p1 p2 bytes_len =
plet_len_div_size ?loc p1.term_type bytes_len (pcopied_memcpy ?loc p1 p2)
+let presult_dest ?loc t dest =
+ prel ?loc (Req, (tresult ?loc t), dest)
+
let generate_requires loc dest src len =
List.map new_predicate [
{ (pcorrect_len_bytes ~loc dest.term_type len) with pred_name = ["aligned_end"] } ;
@@ -63,9 +66,10 @@ let generate_assigns loc t dest src len =
let res = result, From [dest] in
Writes [ copy ; res ]
-let generate_ensures loc dest src len =
+let generate_ensures loc t dest src len =
List.map (fun p -> Normal, new_predicate p) [
- { (pcopied_len_bytes ~loc dest src len) with pred_name = [ "copied"] }
+ { (pcopied_len_bytes ~loc dest src len) with pred_name = [ "copied"] } ;
+ { (presult_dest ~loc t dest) with pred_name = [ "result"] }
]
let generate_spec vi loc =
@@ -79,7 +83,7 @@ let generate_spec vi loc =
let len = cvar_to_tvar clen in
let requires = generate_requires loc dest src len in
let assigns = generate_assigns loc t dest src len in
- let ensures = generate_ensures loc dest src len in
+ let ensures = generate_ensures loc t dest src len in
make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
let generate_prototype t =
diff --git a/src/plugins/override_std/memmove.ml b/src/plugins/override_std/memmove.ml
index f0ddef2df5c..a29ca3383e5 100644
--- a/src/plugins/override_std/memmove.ml
+++ b/src/plugins/override_std/memmove.ml
@@ -43,6 +43,9 @@ let pmoved_memmove ?loc dest src len =
let pmoved_len_bytes ?loc dest src bytes_len =
plet_len_div_size ?loc dest.term_type bytes_len (pmoved_memmove ?loc dest src)
+let presult_dest ?loc t dest =
+ prel ?loc (Req, (tresult ?loc t), dest)
+
let generate_requires loc dest src len =
List.map new_predicate [
{ (pcorrect_len_bytes ~loc dest.term_type len) with pred_name = ["aligned_end"] } ;
@@ -59,9 +62,10 @@ let generate_assigns loc t dest src len =
let res = result, From [dest] in
Writes [ copy ; res ]
-let generate_ensures loc dest src len =
+let generate_ensures loc t dest src len =
List.map (fun p -> Normal, new_predicate p) [
- { (pmoved_len_bytes ~loc dest src len) with pred_name = [ "moved"] }
+ { (pmoved_len_bytes ~loc dest src len) with pred_name = [ "moved"] } ;
+ { (presult_dest ~loc t dest) with pred_name = [ "result"] }
]
let generate_spec vi loc =
@@ -75,7 +79,7 @@ let generate_spec vi loc =
let len = cvar_to_tvar clen in
let requires = generate_requires loc dest src len in
let assigns = generate_assigns loc t dest src len in
- let ensures = generate_ensures loc dest src len in
+ let ensures = generate_ensures loc t dest src len in
make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
let generate_prototype t =
diff --git a/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle b/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle
index 974fd3a31a2..6bb3d9d1bb5 100644
--- a/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle
+++ b/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle
@@ -17,6 +17,7 @@
copied:
\let __fc_len = len / 4;
∀ ℤ j; 0 ≤ j < __fc_len ⇒ *(dest + j) ≡ *(src + j);
+ ensures result: \result ≡ dest;
assigns *(dest + (0 .. len - 1)), \result;
assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
assigns \result \from dest;
@@ -37,7 +38,7 @@ int main(void)
[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.
+ def'n of func main at tests/functions/memcpy.c:3 (sum 1968) conflicts with the one at tests/functions/result/memcpy.c:26 (sum 3742); keeping the one at tests/functions/result/memcpy.c:26.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -57,6 +58,7 @@ int main(void)
\let __fc_len = \old(len) / 4;
∀ ℤ j;
0 ≤ j < __fc_len ⇒ *(\old(dest) + j) ≡ *(\old(src) + j);
+ 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;
diff --git a/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle b/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle
index d922f913cad..2db11ab0c0c 100644
--- a/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle
+++ b/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle
@@ -13,6 +13,7 @@
moved:
\let __fc_len = len / 4;
∀ ℤ j; 0 ≤ j < __fc_len ⇒ *(dest + j) ≡ \at(*(src + j),Pre);
+ ensures result: \result ≡ dest;
assigns *(dest + (0 .. len - 1)), \result;
assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
assigns \result \from dest;
@@ -33,7 +34,7 @@ int main(void)
[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.
+ def'n of func main at tests/functions/memmove.c:3 (sum 1968) conflicts with the one at tests/functions/result/memmove.c:22 (sum 3742); keeping the one at tests/functions/result/memmove.c:22.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -49,6 +50,7 @@ int main(void)
\let __fc_len = \old(len) / 4;
∀ ℤ j;
0 ≤ j < __fc_len ⇒ *(\old(dest) + j) ≡ \at(*(src + j),Pre);
+ 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;
--
GitLab