[Override Std] Fix missing \result in memcpy/move

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 =

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 =

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;

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;