From 838879f8c2620a64383618ab0fa5a10286cda987 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 24 Oct 2019 17:36:15 +0200
Subject: [PATCH] [Builtin] Fix on assigns ranges for string functions
---
src/plugins/builtin/basic_blocks.ml | 10 +
src/plugins/builtin/basic_blocks.mli | 23 +-
src/plugins/builtin/string/memcmp.ml | 4 +-
src/plugins/builtin/string/memcpy.ml | 4 +-
src/plugins/builtin/string/memmove.ml | 4 +-
src/plugins/builtin/string/memset.ml | 6 +-
.../options/oracle/ignore-builtin.res.oracle | 14 +-
.../oracle/ignore-functions.res.oracle | 4 +-
.../options/oracle/only-functions.res.oracle | 4 +-
.../tests/string/oracle/memcmp.res.oracle | 32 +-
.../tests/string/oracle/memcpy.res.oracle | 36 +-
.../tests/string/oracle/memmove.res.oracle | 36 +-
.../tests/string/oracle/memset_0.res.oracle | 212 +++++------
.../tests/string/oracle/memset_FF.res.oracle | 352 +++++++++---------
.../string/oracle/memset_value.res.oracle | 72 ++--
15 files changed, 414 insertions(+), 399 deletions(-)
diff --git a/src/plugins/builtin/basic_blocks.ml b/src/plugins/builtin/basic_blocks.ml
index 2cddd187f02..604043ae9b8 100644
--- a/src/plugins/builtin/basic_blocks.ml
+++ b/src/plugins/builtin/basic_blocks.ml
@@ -164,6 +164,16 @@ let unroll_logic_type = function
| Ctype t -> Ctype (Cil.unrollType t)
| t -> t
+let tunref_range_bytes_len ?loc ptr bytes_len =
+ let sizeof = sizeofpointed ptr.term_type in
+ if sizeof = 1 then
+ tunref_range ?loc ptr bytes_len
+ else
+ let sizeof = tinteger ?loc sizeof in
+ let len = tdivide ?loc bytes_len sizeof in
+ tunref_range ?loc ptr len
+
+
(** Features related to predicates *)
let plet_len_div_size ?loc ?name_ext t bytes_len pred =
diff --git a/src/plugins/builtin/basic_blocks.mli b/src/plugins/builtin/basic_blocks.mli
index b7547d10c24..0fb7d2052d6 100644
--- a/src/plugins/builtin/basic_blocks.mli
+++ b/src/plugins/builtin/basic_blocks.mli
@@ -71,6 +71,11 @@ val cvar_to_tvar: varinfo -> term
(** [tunref_range ~loc ptr len] builds [*(ptr + (0 .. len-1))] *)
val tunref_range: ?loc:location -> term -> term -> term
+(** [tunref_range ~loc ptr bytes_len] same as [tunref_range] except that length
+ is provided in bytes.
+*)
+val tunref_range_bytes_len: ?loc:location -> term -> term -> term
+
(** [tplus ~loc t1 t2] builds [t1+t2] *)
val tplus: ?loc:location -> term -> term -> term
@@ -162,11 +167,11 @@ val punfold_flexible_struct_pred:
val pvalid_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
(** [pvalid_read_len_bytes ~loc label ptr bytes_len] generates a predicate
- - [\valid_read{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr))))].
+ - [\valid_read{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr))))].
- Parameters:
- - [ptr] must be a term of pointer type.
- *)
+ Parameters:
+ - [ptr] must be a term of pointer type.
+*)
val pvalid_read_len_bytes:
?loc:location -> logic_label -> term -> term -> predicate
@@ -187,11 +192,11 @@ val pseparated_memories:
(** {2 Specification} *)
(** Builds a behavior from its components. If a component is missing,
- it defaults to:
- - [name]: [Cil.default_behavior_name]
- - [requires], [ensures], [extension]: [[]]
- - [assigns]: = [WritesAny]
- - [alloc]: [FreeAllocAny]
+ it defaults to:
+ - [name]: [Cil.default_behavior_name]
+ - [requires], [ensures], [extension]: [[]]
+ - [assigns]: = [WritesAny]
+ - [alloc]: [FreeAllocAny]
*)
val make_behavior:
?name:string ->
diff --git a/src/plugins/builtin/string/memcmp.ml b/src/plugins/builtin/string/memcmp.ml
index 6399e653ecc..a8edb6e540b 100644
--- a/src/plugins/builtin/string/memcmp.ml
+++ b/src/plugins/builtin/string/memcmp.ml
@@ -43,8 +43,8 @@ let presult_memcmp ?loc p1 p2 len =
let generate_assigns loc s1 s2 len =
let indirect_range loc s len =
- let t = { (tunref_range ~loc s len) with term_name = ["indirect"] } in
- new_identified_term t
+ new_identified_term
+ { (tunref_range_bytes_len ~loc s len) with term_name = ["indirect"] }
in
let s1_range = indirect_range loc s1 len in
let s2_range = indirect_range loc s2 len in
diff --git a/src/plugins/builtin/string/memcpy.ml b/src/plugins/builtin/string/memcpy.ml
index 4346977aa87..31eee35d2b4 100644
--- a/src/plugins/builtin/string/memcpy.ml
+++ b/src/plugins/builtin/string/memcpy.ml
@@ -50,8 +50,8 @@ let generate_requires loc dest src len =
]
let generate_assigns loc t dest src len =
- let dest_range = new_identified_term (tunref_range ~loc dest len) in
- let src_range = new_identified_term(tunref_range ~loc src len) in
+ let dest_range = new_identified_term (tunref_range_bytes_len ~loc dest len) in
+ let src_range = new_identified_term(tunref_range_bytes_len ~loc src len) in
let copy = dest_range, From [src_range] in
let result = new_identified_term (tresult t) in
let dest = new_identified_term dest in
diff --git a/src/plugins/builtin/string/memmove.ml b/src/plugins/builtin/string/memmove.ml
index aa200185ca3..dd3104d45c5 100644
--- a/src/plugins/builtin/string/memmove.ml
+++ b/src/plugins/builtin/string/memmove.ml
@@ -44,8 +44,8 @@ let generate_requires loc dest src len =
]
let generate_assigns loc t dest src len =
- let dest_range = new_identified_term (tunref_range ~loc dest len) in
- let src_range = new_identified_term(tunref_range ~loc src len) in
+ let dest_range = new_identified_term (tunref_range_bytes_len ~loc dest len) in
+ let src_range = new_identified_term(tunref_range_bytes_len ~loc src len) in
let copy = dest_range, From [src_range] in
let result = new_identified_term (tresult t) in
let dest = new_identified_term dest in
diff --git a/src/plugins/builtin/string/memset.ml b/src/plugins/builtin/string/memset.ml
index 34c8e2b601c..6da6545f3b0 100644
--- a/src/plugins/builtin/string/memset.ml
+++ b/src/plugins/builtin/string/memset.ml
@@ -133,7 +133,7 @@ let generate_requires loc ptr value len =
let generate_assigns loc t ptr value len =
let open Extlib in
- let ptr_range = new_identified_term (tunref_range ~loc ptr len) in
+ let ptr_range = new_identified_term (tunref_range_bytes_len ~loc ptr len) in
let value = list_of_opt (opt_map new_identified_term value) in
let set = ptr_range, From value in
let result = new_identified_term (tresult t) in
@@ -210,14 +210,14 @@ let char_prototype t =
let params = [
("ptr", ptr_of t, []) ;
("value", base_char_type t, []) ;
- ("num", size_t(), [])
+ ("len", size_t(), [])
] in
TFun (ptr_of t, Some params, false, [])
let non_char_prototype t =
let params = [
("ptr", (ptr_of t), []) ;
- ("num", size_t(), [])
+ ("len", size_t(), [])
] in
TFun ((ptr_of t), Some params, false, [])
diff --git a/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle b/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle
index a37f9b74200..69cf5e09ef7 100644
--- a/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle
+++ b/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle
@@ -3,22 +3,22 @@
#include "stddef.h"
#include "string.h"
#include "strings.h"
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 0;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int *memset_int_0(int *ptr, size_t num)
+int *memset_int_0(int *ptr, size_t len)
{
int *__retres;
- __retres = (int *)memset((void *)ptr,0,num);
+ __retres = (int *)memset((void *)ptr,0,len);
return __retres;
}
diff --git a/src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle b/src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle
index ee940654e55..8aacf1fa757 100644
--- a/src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle
+++ b/src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle
@@ -26,8 +26,8 @@ void foo(void)
\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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int *memcpy_int(int *dest, int const *src, size_t len)
diff --git a/src/plugins/builtin/tests/options/oracle/only-functions.res.oracle b/src/plugins/builtin/tests/options/oracle/only-functions.res.oracle
index 11b95496d16..cc08c601aac 100644
--- a/src/plugins/builtin/tests/options/oracle/only-functions.res.oracle
+++ b/src/plugins/builtin/tests/options/oracle/only-functions.res.oracle
@@ -18,8 +18,8 @@
\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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int *memcpy_int(int *dest, int const *src, size_t len)
diff --git a/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle b/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
index 7b39a351f64..83f1e8a4fba 100644
--- a/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
@@ -23,8 +23,8 @@ typedef int named;
(∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
assigns \result;
assigns \result
- \from (indirect: *(s1 + (0 .. len - 1))),
- (indirect: *(s2 + (0 .. len - 1)));
+ \from (indirect: *(s1 + (0 .. len / 4 - 1))),
+ (indirect: *(s2 + (0 .. len / 4 - 1)));
*/
int memcmp_int(int const *s1, int const *s2, size_t len)
{
@@ -61,8 +61,8 @@ int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2)
(∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
assigns \result;
assigns \result
- \from (indirect: *(s1 + (0 .. len - 1))),
- (indirect: *(s2 + (0 .. len - 1)));
+ \from (indirect: *(s1 + (0 .. len / 8 - 1))),
+ (indirect: *(s2 + (0 .. len / 8 - 1)));
*/
int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
{
@@ -92,8 +92,8 @@ int structure(struct X * /*[10]*/ s1, struct X * /*[10]*/ s2)
(∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
assigns \result;
assigns \result
- \from (indirect: *(s1 + (0 .. len - 1))),
- (indirect: *(s2 + (0 .. len - 1)));
+ \from (indirect: *(s1 + (0 .. len / 4 - 1))),
+ (indirect: *(s2 + (0 .. len / 4 - 1)));
*/
int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{
@@ -126,8 +126,8 @@ int pointers(int ** /*[10]*/ s1, int ** /*[10]*/ s2)
0 ≤ j1 < 10 ⇒ (*(s1 + j0))[j1] ≡ (*(s2 + j0))[j1]));
assigns \result;
assigns \result
- \from (indirect: (*(s1 + (0 .. len - 1)))[0 .. 10 - 1]),
- (indirect: (*(s2 + (0 .. len - 1)))[0 .. 10 - 1]);
+ \from (indirect: (*(s1 + (0 .. len / 40 - 1)))[0 .. 10 - 1]),
+ (indirect: (*(s2 + (0 .. len / 40 - 1)))[0 .. 10 - 1]);
*/
int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
{
@@ -189,8 +189,8 @@ typedef int named;
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)));
+ \from (indirect: *(s1 + (0 .. len / 4 - 1))),
+ (indirect: *(s2 + (0 .. len / 4 - 1)));
*/
int memcmp_int(int const *s1, int const *s2, size_t len)
{
@@ -230,8 +230,8 @@ int with_named(named *s1, named *s2)
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)));
+ \from (indirect: *(s1 + (0 .. len / 8 - 1))),
+ (indirect: *(s2 + (0 .. len / 8 - 1)));
*/
int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
{
@@ -263,8 +263,8 @@ int structure(struct X *s1, struct X *s2)
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)));
+ \from (indirect: *(s1 + (0 .. len / 4 - 1))),
+ (indirect: *(s2 + (0 .. len / 4 - 1)));
*/
int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{
@@ -299,8 +299,8 @@ int pointers(int **s1, int **s2)
(*(\old(s1) + j0))[j1] ≡ (*(\old(s2) + j0))[j1]));
assigns \result;
assigns \result
- \from (indirect: (*(s1 + (0 .. len - 1)))[0 .. 10 - 1]),
- (indirect: (*(s2 + (0 .. len - 1)))[0 .. 10 - 1]);
+ \from (indirect: (*(s1 + (0 .. len / 40 - 1)))[0 .. 10 - 1]),
+ (indirect: (*(s2 + (0 .. len / 40 - 1)))[0 .. 10 - 1]);
*/
int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
{
diff --git a/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle b/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
index ced9071c356..5a9013b038d 100644
--- a/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
@@ -25,8 +25,8 @@ typedef int named;
\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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int *memcpy_int(int *dest, int const *src, size_t len)
@@ -65,8 +65,8 @@ void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
\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 *(dest + (0 .. len / 8 - 1)), \result;
+ assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest;
*/
struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
@@ -98,8 +98,8 @@ void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
\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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
@@ -135,9 +135,9 @@ void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
(∀ ℤ j1;
0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
ensures result: \result ≡ dest;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
- \from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
+ assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1]
+ \from (*(src + (0 .. len / 40 - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
@@ -202,8 +202,8 @@ typedef int named;
∀ ℤ 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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int *memcpy_int(int *dest, int const *src, size_t len)
@@ -245,8 +245,8 @@ void with_named(named *src, named *dest)
∀ ℤ 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 *(dest + (0 .. len / 8 - 1)), \result;
+ assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest;
*/
struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
@@ -281,8 +281,8 @@ void structure(struct X *src, struct X *dest)
∀ ℤ 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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
@@ -320,9 +320,9 @@ void pointers(int **src, int **dest)
0 ≤ j1 < 10 ⇒
(*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
ensures result: \result ≡ \old(dest);
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
- \from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
+ assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1]
+ \from (*(src + (0 .. len / 40 - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
diff --git a/src/plugins/builtin/tests/string/oracle/memmove.res.oracle b/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
index 7b7122fb41a..193a3f96dbc 100644
--- a/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
@@ -21,8 +21,8 @@ typedef int named;
\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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int *memmove_int(int *dest, int const *src, size_t len)
@@ -57,8 +57,8 @@ void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
\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 *(dest + (0 .. len / 8 - 1)), \result;
+ assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest;
*/
struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
@@ -86,8 +86,8 @@ void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
\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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int **memmove_ptr_int(int **dest, int * const *src, size_t len)
@@ -119,9 +119,9 @@ void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
(∀ ℤ j1;
0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
ensures result: \result ≡ dest;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
- \from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
+ assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1]
+ \from (*(src + (0 .. len / 40 - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
@@ -182,8 +182,8 @@ typedef int named;
∀ ℤ 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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int *memmove_int(int *dest, int const *src, size_t len)
@@ -221,8 +221,8 @@ void with_named(named *src, named *dest)
∀ ℤ 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 *(dest + (0 .. len / 8 - 1)), \result;
+ assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest;
*/
struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
@@ -253,8 +253,8 @@ void structure(struct X *src, struct X *dest)
∀ ℤ 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 *(dest + (0 .. len / 4 - 1)), \result;
+ assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int **memmove_ptr_int(int **dest, int * const *src, size_t len)
@@ -288,9 +288,9 @@ void pointers(int **src, int **dest)
0 ≤ j1 < 10 ⇒
(*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
ensures result: \result ≡ \old(dest);
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
- \from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
+ assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1]
+ \from (*(src + (0 .. len / 40 - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
diff --git a/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
index ba939b95fc5..84e0ba0e23d 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
@@ -11,18 +11,18 @@ struct X {
};
typedef int named;
/*@ requires in_bounds_value: -128 ≤ value < 128;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
- set_content: ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(ptr + j0) ≡ value;
+ set_content: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(ptr + j0) ≡ value;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
-char *memset_char(char *ptr, char value, size_t num)
+char *memset_char(char *ptr, char value, size_t len)
{
char *__retres;
- __retres = (char *)memset((void *)ptr,(int)value,num);
+ __retres = (char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -34,19 +34,19 @@ void chars(char * /*[10]*/ dest)
}
/*@ requires in_bounds_value: 0 ≤ value < 256;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
- set_content: ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(ptr + j0) ≡ value;
+ set_content: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(ptr + j0) ≡ value;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
- size_t num)
+ size_t len)
{
unsigned char *__retres;
- __retres = (unsigned char *)memset((void *)ptr,(int)value,num);
+ __retres = (unsigned char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -59,22 +59,22 @@ void uchars(unsigned char * /*[10]*/ dest)
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires
- valid_dest: \let __fc_len = num / 10; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 10; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 10;
+ \let __fc_len = len / 10;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ value);
ensures result: \result ≡ ptr;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from value;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1] \from value;
assigns \result \from ptr;
*/
-char (*memset_arr10_char(char (*ptr)[10], char value, size_t num))[10]
+char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
{
char (*__retres)[10];
- __retres = (char (*)[10])memset((void *)ptr,(int)value,num);
+ __retres = (char (*)[10])memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -85,22 +85,22 @@ void nested_chars(char (* /*[10]*/ dest)[10])
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 0;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int *memset_int_0(int *ptr, size_t num)
+int *memset_int_0(int *ptr, size_t len)
{
int *__retres;
- __retres = (int *)memset((void *)ptr,0,num);
+ __retres = (int *)memset((void *)ptr,0,len);
return __retres;
}
@@ -111,22 +111,22 @@ void integer(int * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 0.;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-float *memset_float_0(float *ptr, size_t num)
+float *memset_float_0(float *ptr, size_t len)
{
float *__retres;
- __retres = (float *)memset((void *)ptr,0,num);
+ __retres = (float *)memset((void *)ptr,0,len);
return __retres;
}
@@ -144,23 +144,23 @@ void with_named(named * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 8 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 8; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 8;
+ \let __fc_len = len / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ (ptr + j0)->x ≡ 0 ∧ (ptr + j0)->y ≡ 0;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-struct X *memset_st_X_0(struct X *ptr, size_t num)
+struct X *memset_st_X_0(struct X *ptr, size_t len)
{
struct X *__retres;
- __retres = (struct X *)memset((void *)ptr,0,num);
+ __retres = (struct X *)memset((void *)ptr,0,len);
return __retres;
}
@@ -171,22 +171,22 @@ void structure(struct X * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ \null;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int **memset_ptr_int_0(int **ptr, size_t num)
+int **memset_ptr_int_0(int **ptr, size_t len)
{
int **__retres;
- __retres = (int **)memset((void *)ptr,0,num);
+ __retres = (int **)memset((void *)ptr,0,len);
return __retres;
}
@@ -197,24 +197,24 @@ void pointers(int ** /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 40 ≡ 0;
+/*@ requires aligned_end: len % 40 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 40; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 40; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 40;
+ \let __fc_len = len / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ 0);
ensures result: \result ≡ ptr;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from \nothing;
+ assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1] \from \nothing;
assigns \result \from ptr;
*/
-int (*memset_arr10_int_0(int (*ptr)[10], size_t num))[10]
+int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10]
{
int (*__retres)[10];
- __retres = (int (*)[10])memset((void *)ptr,0,num);
+ __retres = (int (*)[10])memset((void *)ptr,0,len);
return __retres;
}
@@ -266,20 +266,20 @@ struct X {
};
typedef int named;
/*@ requires in_bounds_value: -128 ≤ value < 128;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
set_content:
∀ ℤ j0;
- 0 ≤ j0 < \old(num) ⇒ *(\old(ptr) + j0) ≡ \old(value);
+ 0 ≤ j0 < \old(len) ⇒ *(\old(ptr) + j0) ≡ \old(value);
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
-char *memset_char(char *ptr, char value, size_t num)
+char *memset_char(char *ptr, char value, size_t len)
{
char *__retres;
- __retres = (char *)memset((void *)ptr,(int)value,num);
+ __retres = (char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -291,21 +291,21 @@ void chars(char *dest)
}
/*@ requires in_bounds_value: 0 ≤ value < 256;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
set_content:
∀ ℤ j0;
- 0 ≤ j0 < \old(num) ⇒ *(\old(ptr) + j0) ≡ \old(value);
+ 0 ≤ j0 < \old(len) ⇒ *(\old(ptr) + j0) ≡ \old(value);
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
- size_t num)
+ size_t len)
{
unsigned char *__retres;
- __retres = (unsigned char *)memset((void *)ptr,(int)value,num);
+ __retres = (unsigned char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -318,23 +318,23 @@ void uchars(unsigned char *dest)
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires
- valid_dest: \let __fc_len = num / 10; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 10; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 10;
+ \let __fc_len = \old(len) / 10;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ \old(value));
ensures result: \result ≡ \old(ptr);
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from value;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1] \from value;
assigns \result \from ptr;
*/
-char (*memset_arr10_char(char (*ptr)[10], char value, size_t num))[10]
+char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
{
char (*__retres)[10];
- __retres = (char (*)[10])memset((void *)ptr,(int)value,num);
+ __retres = (char (*)[10])memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -345,22 +345,22 @@ void nested_chars(char (*dest)[10])
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 0;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int *memset_int_0(int *ptr, size_t num)
+int *memset_int_0(int *ptr, size_t len)
{
int *__retres;
- __retres = (int *)memset((void *)ptr,0,num);
+ __retres = (int *)memset((void *)ptr,0,len);
return __retres;
}
@@ -371,22 +371,22 @@ void integer(int *dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 0.;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-float *memset_float_0(float *ptr, size_t num)
+float *memset_float_0(float *ptr, size_t len)
{
float *__retres;
- __retres = (float *)memset((void *)ptr,0,num);
+ __retres = (float *)memset((void *)ptr,0,len);
return __retres;
}
@@ -404,24 +404,24 @@ void with_named(named *dest)
return;
}
-/*@ requires aligned_end: num % 8 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 8; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 8;
+ \let __fc_len = \old(len) / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(\old(ptr) + j0)->x ≡ 0 ∧ (\old(ptr) + j0)->y ≡ 0;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-struct X *memset_st_X_0(struct X *ptr, size_t num)
+struct X *memset_st_X_0(struct X *ptr, size_t len)
{
struct X *__retres;
- __retres = (struct X *)memset((void *)ptr,0,num);
+ __retres = (struct X *)memset((void *)ptr,0,len);
return __retres;
}
@@ -432,22 +432,22 @@ void structure(struct X *dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ \null;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int **memset_ptr_int_0(int **ptr, size_t num)
+int **memset_ptr_int_0(int **ptr, size_t len)
{
int **__retres;
- __retres = (int **)memset((void *)ptr,0,num);
+ __retres = (int **)memset((void *)ptr,0,len);
return __retres;
}
@@ -458,24 +458,24 @@ void pointers(int **dest)
return;
}
-/*@ requires aligned_end: num % 40 ≡ 0;
+/*@ requires aligned_end: len % 40 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 40; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 40; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 40;
+ \let __fc_len = \old(len) / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ 0);
ensures result: \result ≡ \old(ptr);
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from \nothing;
+ assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1] \from \nothing;
assigns \result \from ptr;
*/
-int (*memset_arr10_int_0(int (*ptr)[10], size_t num))[10]
+int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10]
{
int (*__retres)[10];
- __retres = (int (*)[10])memset((void *)ptr,0,num);
+ __retres = (int (*)[10])memset((void *)ptr,0,len);
return __retres;
}
diff --git a/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
index 1115c29a5ac..e45698fc0a3 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
@@ -11,18 +11,18 @@ struct X {
};
typedef int named;
/*@ requires in_bounds_value: -128 ≤ value < 128;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
- set_content: ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(ptr + j0) ≡ value;
+ set_content: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(ptr + j0) ≡ value;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
-char *memset_char(char *ptr, char value, size_t num)
+char *memset_char(char *ptr, char value, size_t len)
{
char *__retres;
- __retres = (char *)memset((void *)ptr,(int)value,num);
+ __retres = (char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -34,19 +34,19 @@ void chars(char * /*[10]*/ dest)
}
/*@ requires in_bounds_value: 0 ≤ value < 256;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
- set_content: ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(ptr + j0) ≡ value;
+ set_content: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(ptr + j0) ≡ value;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
- size_t num)
+ size_t len)
{
unsigned char *__retres;
- __retres = (unsigned char *)memset((void *)ptr,(int)value,num);
+ __retres = (unsigned char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -60,22 +60,22 @@ void uchars(unsigned char * /*[10]*/ dest)
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires
- valid_dest: \let __fc_len = num / 10; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 10; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 10;
+ \let __fc_len = len / 10;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ value);
ensures result: \result ≡ ptr;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from value;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1] \from value;
assigns \result \from ptr;
*/
-char (*memset_arr10_char(char (*ptr)[10], char value, size_t num))[10]
+char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
{
char (*__retres)[10];
- __retres = (char (*)[10])memset((void *)ptr,(int)value,num);
+ __retres = (char (*)[10])memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -86,22 +86,22 @@ void nested_chars(char (* /*[10]*/ dest)[10])
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -2147483648;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int *memset_int_FF(int *ptr, size_t num)
+int *memset_int_FF(int *ptr, size_t len)
{
int *__retres;
- __retres = (int *)memset((void *)ptr,255,num);
+ __retres = (int *)memset((void *)ptr,255,len);
return __retres;
}
@@ -112,22 +112,22 @@ void integer(int * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 4294967295;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-unsigned int *memset_uint_FF(unsigned int *ptr, size_t num)
+unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
{
unsigned int *__retres;
- __retres = (unsigned int *)memset((void *)ptr,255,num);
+ __retres = (unsigned int *)memset((void *)ptr,255,len);
return __retres;
}
@@ -139,22 +139,22 @@ void unsigned_integer(unsigned int * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -2147483648;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-long *memset_long_FF(long *ptr, size_t num)
+long *memset_long_FF(long *ptr, size_t len)
{
long *__retres;
- __retres = (long *)memset((void *)ptr,255,num);
+ __retres = (long *)memset((void *)ptr,255,len);
return __retres;
}
@@ -165,22 +165,22 @@ void long_integer(long * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 4294967295;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-unsigned long *memset_ulong_FF(unsigned long *ptr, size_t num)
+unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
{
unsigned long *__retres;
- __retres = (unsigned long *)memset((void *)ptr,255,num);
+ __retres = (unsigned long *)memset((void *)ptr,255,len);
return __retres;
}
@@ -192,23 +192,23 @@ void unsigned_long_integer(unsigned long * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 8 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 8; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 8;
+ \let __fc_len = len / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ -9223372036854775808;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-long long *memset_llong_FF(long long *ptr, size_t num)
+long long *memset_llong_FF(long long *ptr, size_t len)
{
long long *__retres;
- __retres = (long long *)memset((void *)ptr,255,num);
+ __retres = (long long *)memset((void *)ptr,255,len);
return __retres;
}
@@ -220,23 +220,23 @@ void long_long_integer(long long * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 8 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 8; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 8;
+ \let __fc_len = len / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 18446744073709551615;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t num)
+unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len)
{
unsigned long long *__retres;
- __retres = (unsigned long long *)memset((void *)ptr,255,num);
+ __retres = (unsigned long long *)memset((void *)ptr,255,len);
return __retres;
}
@@ -248,22 +248,22 @@ void unsigned_long_long_integer(unsigned long long * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ \is_NaN(*(ptr + j0));
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-float *memset_float_FF(float *ptr, size_t num)
+float *memset_float_FF(float *ptr, size_t len)
{
float *__retres;
- __retres = (float *)memset((void *)ptr,255,num);
+ __retres = (float *)memset((void *)ptr,255,len);
return __retres;
}
@@ -281,24 +281,24 @@ void with_named(named * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 8 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 8; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 8;
+ \let __fc_len = len / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(ptr + j0)->x ≡ -2147483648 ∧ (ptr + j0)->y ≡ -2147483648;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-struct X *memset_st_X_FF(struct X *ptr, size_t num)
+struct X *memset_st_X_FF(struct X *ptr, size_t len)
{
struct X *__retres;
- __retres = (struct X *)memset((void *)ptr,255,num);
+ __retres = (struct X *)memset((void *)ptr,255,len);
return __retres;
}
@@ -309,22 +309,22 @@ void structure(struct X * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 4;
+ \let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(ptr + j0));
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int **memset_ptr_int_FF(int **ptr, size_t num)
+int **memset_ptr_int_FF(int **ptr, size_t len)
{
int **__retres;
- __retres = (int **)memset((void *)ptr,255,num);
+ __retres = (int **)memset((void *)ptr,255,len);
return __retres;
}
@@ -335,24 +335,24 @@ void pointers(int ** /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: num % 40 ≡ 0;
+/*@ requires aligned_end: len % 40 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 40; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 40; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 40;
+ \let __fc_len = len / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ -2147483648);
ensures result: \result ≡ ptr;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from \nothing;
+ assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1] \from \nothing;
assigns \result \from ptr;
*/
-int (*memset_arr10_int_FF(int (*ptr)[10], size_t num))[10]
+int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10]
{
int (*__retres)[10];
- __retres = (int (*)[10])memset((void *)ptr,255,num);
+ __retres = (int (*)[10])memset((void *)ptr,255,len);
return __retres;
}
@@ -414,20 +414,20 @@ struct X {
};
typedef int named;
/*@ requires in_bounds_value: -128 ≤ value < 128;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
set_content:
∀ ℤ j0;
- 0 ≤ j0 < \old(num) ⇒ *(\old(ptr) + j0) ≡ \old(value);
+ 0 ≤ j0 < \old(len) ⇒ *(\old(ptr) + j0) ≡ \old(value);
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
-char *memset_char(char *ptr, char value, size_t num)
+char *memset_char(char *ptr, char value, size_t len)
{
char *__retres;
- __retres = (char *)memset((void *)ptr,(int)value,num);
+ __retres = (char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -439,21 +439,21 @@ void chars(char *dest)
}
/*@ requires in_bounds_value: 0 ≤ value < 256;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
set_content:
∀ ℤ j0;
- 0 ≤ j0 < \old(num) ⇒ *(\old(ptr) + j0) ≡ \old(value);
+ 0 ≤ j0 < \old(len) ⇒ *(\old(ptr) + j0) ≡ \old(value);
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
- size_t num)
+ size_t len)
{
unsigned char *__retres;
- __retres = (unsigned char *)memset((void *)ptr,(int)value,num);
+ __retres = (unsigned char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -467,23 +467,23 @@ void uchars(unsigned char *dest)
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires
- valid_dest: \let __fc_len = num / 10; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 10; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 10;
+ \let __fc_len = \old(len) / 10;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ \old(value));
ensures result: \result ≡ \old(ptr);
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from value;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1] \from value;
assigns \result \from ptr;
*/
-char (*memset_arr10_char(char (*ptr)[10], char value, size_t num))[10]
+char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
{
char (*__retres)[10];
- __retres = (char (*)[10])memset((void *)ptr,(int)value,num);
+ __retres = (char (*)[10])memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -494,22 +494,22 @@ void nested_chars(char (*dest)[10])
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -2147483648;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int *memset_int_FF(int *ptr, size_t num)
+int *memset_int_FF(int *ptr, size_t len)
{
int *__retres;
- __retres = (int *)memset((void *)ptr,255,num);
+ __retres = (int *)memset((void *)ptr,255,len);
return __retres;
}
@@ -520,22 +520,22 @@ void integer(int *dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 4294967295;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-unsigned int *memset_uint_FF(unsigned int *ptr, size_t num)
+unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
{
unsigned int *__retres;
- __retres = (unsigned int *)memset((void *)ptr,255,num);
+ __retres = (unsigned int *)memset((void *)ptr,255,len);
return __retres;
}
@@ -547,22 +547,22 @@ void unsigned_integer(unsigned int *dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -2147483648;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-long *memset_long_FF(long *ptr, size_t num)
+long *memset_long_FF(long *ptr, size_t len)
{
long *__retres;
- __retres = (long *)memset((void *)ptr,255,num);
+ __retres = (long *)memset((void *)ptr,255,len);
return __retres;
}
@@ -573,22 +573,22 @@ void long_integer(long *dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 4294967295;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-unsigned long *memset_ulong_FF(unsigned long *ptr, size_t num)
+unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
{
unsigned long *__retres;
- __retres = (unsigned long *)memset((void *)ptr,255,num);
+ __retres = (unsigned long *)memset((void *)ptr,255,len);
return __retres;
}
@@ -600,23 +600,23 @@ void unsigned_long_integer(unsigned long *dest)
return;
}
-/*@ requires aligned_end: num % 8 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 8; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 8;
+ \let __fc_len = \old(len) / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ -9223372036854775808;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-long long *memset_llong_FF(long long *ptr, size_t num)
+long long *memset_llong_FF(long long *ptr, size_t len)
{
long long *__retres;
- __retres = (long long *)memset((void *)ptr,255,num);
+ __retres = (long long *)memset((void *)ptr,255,len);
return __retres;
}
@@ -628,23 +628,23 @@ void long_long_integer(long long *dest)
return;
}
-/*@ requires aligned_end: num % 8 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 8; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 8;
+ \let __fc_len = \old(len) / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 18446744073709551615;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t num)
+unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len)
{
unsigned long long *__retres;
- __retres = (unsigned long long *)memset((void *)ptr,255,num);
+ __retres = (unsigned long long *)memset((void *)ptr,255,len);
return __retres;
}
@@ -656,22 +656,22 @@ void unsigned_long_long_integer(unsigned long long *dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ \is_NaN(*(\old(ptr) + j0));
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-float *memset_float_FF(float *ptr, size_t num)
+float *memset_float_FF(float *ptr, size_t len)
{
float *__retres;
- __retres = (float *)memset((void *)ptr,255,num);
+ __retres = (float *)memset((void *)ptr,255,len);
return __retres;
}
@@ -689,25 +689,25 @@ void with_named(named *dest)
return;
}
-/*@ requires aligned_end: num % 8 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 8; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 8;
+ \let __fc_len = \old(len) / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(\old(ptr) + j0)->x ≡ -2147483648 ∧
(\old(ptr) + j0)->y ≡ -2147483648;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-struct X *memset_st_X_FF(struct X *ptr, size_t num)
+struct X *memset_st_X_FF(struct X *ptr, size_t len)
{
struct X *__retres;
- __retres = (struct X *)memset((void *)ptr,255,num);
+ __retres = (struct X *)memset((void *)ptr,255,len);
return __retres;
}
@@ -718,22 +718,22 @@ void structure(struct X *dest)
return;
}
-/*@ requires aligned_end: num % 4 ≡ 0;
+/*@ requires aligned_end: len % 4 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 4; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 4;
+ \let __fc_len = \old(len) / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(\old(ptr) + j0));
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 4 - 1)), \result;
+ assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
assigns \result \from ptr;
*/
-int **memset_ptr_int_FF(int **ptr, size_t num)
+int **memset_ptr_int_FF(int **ptr, size_t len)
{
int **__retres;
- __retres = (int **)memset((void *)ptr,255,num);
+ __retres = (int **)memset((void *)ptr,255,len);
return __retres;
}
@@ -744,25 +744,25 @@ void pointers(int **dest)
return;
}
-/*@ requires aligned_end: num % 40 ≡ 0;
+/*@ requires aligned_end: len % 40 ≡ 0;
requires
- valid_dest: \let __fc_len = num / 40; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 40; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 40;
+ \let __fc_len = \old(len) / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ -2147483648);
ensures result: \result ≡ \old(ptr);
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from \nothing;
+ assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 40 - 1)))[0 .. 10 - 1] \from \nothing;
assigns \result \from ptr;
*/
-int (*memset_arr10_int_FF(int (*ptr)[10], size_t num))[10]
+int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10]
{
int (*__retres)[10];
- __retres = (int (*)[10])memset((void *)ptr,255,num);
+ __retres = (int (*)[10])memset((void *)ptr,255,len);
return __retres;
}
diff --git a/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle
index d7e37edb76c..50858d41d3c 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle
@@ -21,18 +21,18 @@ struct X {
};
typedef int named;
/*@ requires in_bounds_value: -128 ≤ value < 128;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
- set_content: ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(ptr + j0) ≡ value;
+ set_content: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(ptr + j0) ≡ value;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
-char *memset_char(char *ptr, char value, size_t num)
+char *memset_char(char *ptr, char value, size_t len)
{
char *__retres;
- __retres = (char *)memset((void *)ptr,(int)value,num);
+ __retres = (char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -44,19 +44,19 @@ void chars(char * /*[10]*/ dest, char value)
}
/*@ requires in_bounds_value: 0 ≤ value < 256;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
- set_content: ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(ptr + j0) ≡ value;
+ set_content: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(ptr + j0) ≡ value;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
- size_t num)
+ size_t len)
{
unsigned char *__retres;
- __retres = (unsigned char *)memset((void *)ptr,(int)value,num);
+ __retres = (unsigned char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -69,22 +69,22 @@ void uchars(char * /*[10]*/ dest, unsigned char value)
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires
- valid_dest: \let __fc_len = num / 10; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 10; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = num / 10;
+ \let __fc_len = len / 10;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1; 0 ≤ j1 < 10 ⇒ (*(ptr + j0))[j1] ≡ value);
ensures result: \result ≡ ptr;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from value;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1] \from value;
assigns \result \from ptr;
*/
-char (*memset_arr10_char(char (*ptr)[10], char value, size_t num))[10]
+char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
{
char (*__retres)[10];
- __retres = (char (*)[10])memset((void *)ptr,(int)value,num);
+ __retres = (char (*)[10])memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -170,20 +170,20 @@ struct X {
};
typedef int named;
/*@ requires in_bounds_value: -128 ≤ value < 128;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
set_content:
∀ ℤ j0;
- 0 ≤ j0 < \old(num) ⇒ *(\old(ptr) + j0) ≡ \old(value);
+ 0 ≤ j0 < \old(len) ⇒ *(\old(ptr) + j0) ≡ \old(value);
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
-char *memset_char(char *ptr, char value, size_t num)
+char *memset_char(char *ptr, char value, size_t len)
{
char *__retres;
- __retres = (char *)memset((void *)ptr,(int)value,num);
+ __retres = (char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -195,21 +195,21 @@ void chars(char *dest, char value)
}
/*@ requires in_bounds_value: 0 ≤ value < 256;
- requires valid_dest: \valid(ptr + (0 .. num - 1));
+ requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
set_content:
∀ ℤ j0;
- 0 ≤ j0 < \old(num) ⇒ *(\old(ptr) + j0) ≡ \old(value);
+ 0 ≤ j0 < \old(len) ⇒ *(\old(ptr) + j0) ≡ \old(value);
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. num - 1)), \result;
- assigns *(ptr + (0 .. num - 1)) \from value;
+ assigns *(ptr + (0 .. len - 1)), \result;
+ assigns *(ptr + (0 .. len - 1)) \from value;
assigns \result \from ptr;
*/
unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
- size_t num)
+ size_t len)
{
unsigned char *__retres;
- __retres = (unsigned char *)memset((void *)ptr,(int)value,num);
+ __retres = (unsigned char *)memset((void *)ptr,(int)value,len);
return __retres;
}
@@ -222,23 +222,23 @@ void uchars(char *dest, unsigned char value)
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires
- valid_dest: \let __fc_len = num / 10; \valid(ptr + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 10; \valid(ptr + (0 .. __fc_len - 1));
ensures
set_content:
- \let __fc_len = \old(num) / 10;
+ \let __fc_len = \old(len) / 10;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
0 ≤ j1 < 10 ⇒ (*(\old(ptr) + j0))[j1] ≡ \old(value));
ensures result: \result ≡ \old(ptr);
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1], \result;
- assigns (*(ptr + (0 .. num - 1)))[0 .. 10 - 1] \from value;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1], \result;
+ assigns (*(ptr + (0 .. len / 10 - 1)))[0 .. 10 - 1] \from value;
assigns \result \from ptr;
*/
-char (*memset_arr10_char(char (*ptr)[10], char value, size_t num))[10]
+char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
{
char (*__retres)[10];
- __retres = (char (*)[10])memset((void *)ptr,(int)value,num);
+ __retres = (char (*)[10])memset((void *)ptr,(int)value,len);
return __retres;
}
--
GitLab