diff --git a/man/frama-c.1 b/man/frama-c.1
index 24d66d9cad8a800beb9afdb9d3445abef1b62e89..b2b5cfc68717f3ed2add02df1f35cd3e7e529c7c 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -401,7 +401,9 @@ uses \f[I]machine\f[R] as the current machine-dependent configuration
(size of the various integer types, endiandness, \&...).
The list of currently supported machines is available through option
\f[I]-machdep help\f[R].
-Default is \f[B]x86_32\f[R].
+Default is \f[B]x86_64\f[R].
+The environment variable FRAMAC_MACHDEP can be used to override the default
+value. The command line parameter still has priority over the default value.
.TP
.B -main \f[I]f\f[R]
sets \f[I]f\f[R] as the entry point of the analysis.
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index d3509da86d048606107660bfeb550cdf49616d67..5c30b36f614a0626ebb02eadf0d57c285e1bc164 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -941,11 +941,15 @@ module Machdep =
(struct
let module_name = "Machdep"
let option_name = "-machdep"
- let default = "x86_32"
+ let default =
+ try Sys.getenv "FRAMAC_MACHDEP"
+ with Not_found -> "x86_64"
let arg_name = "machine"
let help =
"use <machine> as the current machine dependent configuration. \
- See \"-machdep help\" for a list"
+ See \"-machdep help\" for a list. The environment variable \
+ FRAMAC_MACHDEP can be used to override the default value. The command \
+ line parameter still has priority over the default value"
end)
let () = Parameter_customize.set_group parsing
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index 43699ce9ec7abf7b39c5d535b758c4b7e908d813..924f3f034437969ed4962e44e7adc894e8367e12 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -118,7 +118,7 @@ int decode_int(char *s)
int __retres;
char c;
/*@ ghost decode_int_pre_func(s); */
- int intmax = ~ (1 << (sizeof(int) * (unsigned int)8 - (unsigned int)1));
+ int intmax = ~ (1 << (sizeof(int) * (unsigned long)8 - (unsigned long)1));
int cutlim = intmax % 10;
int cutoff = intmax / 10;
int value = 0;
diff --git a/src/plugins/dive/tests/dive/exceptional.i b/src/plugins/dive/tests/dive/exceptional.i
index c65084f9539f908baf2ac70c605ddfe4efa437d1..62791ed36e0e5d3293f1cbd97cb62eb17ac3145b 100644
--- a/src/plugins/dive/tests/dive/exceptional.i
+++ b/src/plugins/dive/tests/dive/exceptional.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-absolute-valid-range 0x10000000-0x1fffffff -dive-from-variables main::__retres -dive-depth-limit 5"
+STDOPT: #"-machdep x86_32" +"-absolute-valid-range 0x10000000-0x1fffffff -dive-from-variables main::__retres -dive-depth-limit 5"
*/
int* gm(int *p) { return (int *) ((unsigned int) p * 2 / 2); }
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index 42142cc28c44a5064df718b6d0499850aff7bca7..0faa0e41124ff41340e4db42bac30e685cf54c43 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -73,11 +73,8 @@ let make_axiomatic_is_allocable loc () =
let lv_i = Cil_const.make_logic_var_quant "i" Linteger in
let t_i = tvar lv_i in
let zero = tinteger 0 in
- let max =
- tinteger
- (Integer.to_int
- (Cil.max_unsigned_number (Cil.bitsSizeOf (size_t ()))))
- in
+ let max_value = Cil.max_unsigned_number (Cil.bitsSizeOf (size_t ())) in
+ let max = term ~loc (TConst (Integer (max_value, None))) Linteger in
let label = FormalLabel("L") in
let cond = pand (prel (Rlt, t_i, zero), prel (Rgt, t_i, max)) in
let app = pnot (papp (is_allocable,[label],[t_i])) in
diff --git a/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c b/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
index 21498c2ef2b5ab29516316267bc33c5af6d46bbd..81ef28cf12683af085eef8f39248f5526e97fb2d 100644
--- a/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
+++ b/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
@@ -9,4 +9,4 @@ void foo(void){
int * q = calloc(2, sizeof(int));
free(p);
free(q);
-}
\ No newline at end of file
+}
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index 1670641826813ce9b10d06d60f85849cf9e55a57..e2656fb94612807dd7810669096e9d83aebf1549 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -300,17 +300,17 @@ int *calloc_int(size_t num, size_t size)
int main(void)
{
int __retres;
- int *pi = calloc_int((unsigned int)10,sizeof(int));
- enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E));
- float *pf = calloc_float((unsigned int)10,sizeof(float));
- struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
- char *pc = calloc_char((unsigned int)10,sizeof(char));
- int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
+ int *pi = calloc_int((unsigned long)10,sizeof(int));
+ enum E *pe = calloc_e_E((unsigned long)10,sizeof(enum E));
+ float *pf = calloc_float((unsigned long)10,sizeof(float));
+ struct X *px = calloc_st_X((unsigned long)10,sizeof(struct X));
+ char *pc = calloc_char((unsigned long)10,sizeof(char));
+ int (*pa)[10] = calloc_arr10_int((unsigned long)10,sizeof(int [10]));
struct Flex *f =
- calloc_st_Flex((unsigned int)1,
- sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
- void *v = calloc((unsigned int)10,sizeof(char));
- struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
+ calloc_st_Flex((unsigned long)1,
+ sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
+ void *v = calloc((unsigned long)10,sizeof(char));
+ struct incomplete *inc = calloc((unsigned long)10,(unsigned long)10);
__retres = 0;
return __retres;
}
@@ -619,17 +619,17 @@ int *calloc_int(size_t num, size_t size)
int main(void)
{
int __retres;
- int *pi = calloc_int((unsigned int)10,sizeof(int));
- enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E));
- float *pf = calloc_float((unsigned int)10,sizeof(float));
- struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
- char *pc = calloc_char((unsigned int)10,sizeof(char));
- int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
+ int *pi = calloc_int((unsigned long)10,sizeof(int));
+ enum E *pe = calloc_e_E((unsigned long)10,sizeof(enum E));
+ float *pf = calloc_float((unsigned long)10,sizeof(float));
+ struct X *px = calloc_st_X((unsigned long)10,sizeof(struct X));
+ char *pc = calloc_char((unsigned long)10,sizeof(char));
+ int (*pa)[10] = calloc_arr10_int((unsigned long)10,sizeof(int [10]));
struct Flex *f =
- calloc_st_Flex((unsigned int)1,
- sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
- void *v = calloc((unsigned int)10,sizeof(char));
- struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
+ calloc_st_Flex((unsigned long)1,
+ sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
+ void *v = calloc((unsigned long)10,sizeof(char));
+ struct incomplete *inc = calloc((unsigned long)10,(unsigned long)10);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index 9aff502467ca08d49dc7d2f346e2e05c6894c995..5fc593cb30dbecee8f1301238a8e35148decf5a5 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -204,15 +204,15 @@ int *malloc_int(size_t size)
int main(void)
{
int __retres;
- int *pi = malloc_int(sizeof(int) * (unsigned int)10);
- float *pf = malloc_float(sizeof(float) * (unsigned int)10);
- struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
- char *pc = malloc_char((unsigned int)10);
- int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
+ int *pi = malloc_int(sizeof(int) * (unsigned long)10);
+ float *pf = malloc_float(sizeof(float) * (unsigned long)10);
+ struct X *px = malloc_st_X(sizeof(struct X) * (unsigned long)10);
+ char *pc = malloc_char((unsigned long)10);
+ int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned long)10);
struct Flex *f =
- malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
- void *v = malloc(sizeof(char) * (unsigned int)10);
- struct incomplete *inc = malloc((unsigned int)10);
+ malloc_st_Flex(sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
+ void *v = malloc(sizeof(char) * (unsigned long)10);
+ struct incomplete *inc = malloc((unsigned long)10);
__retres = 0;
return __retres;
}
@@ -420,15 +420,15 @@ int *malloc_int(size_t size)
int main(void)
{
int __retres;
- int *pi = malloc_int(sizeof(int) * (unsigned int)10);
- float *pf = malloc_float(sizeof(float) * (unsigned int)10);
- struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
- char *pc = malloc_char((unsigned int)10);
- int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
+ int *pi = malloc_int(sizeof(int) * (unsigned long)10);
+ float *pf = malloc_float(sizeof(float) * (unsigned long)10);
+ struct X *px = malloc_st_X(sizeof(struct X) * (unsigned long)10);
+ char *pc = malloc_char((unsigned long)10);
+ int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned long)10);
struct Flex *f =
- malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
- void *v = malloc(sizeof(char) * (unsigned int)10);
- struct incomplete *inc = malloc((unsigned int)10);
+ malloc_st_Flex(sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
+ void *v = malloc(sizeof(char) * (unsigned long)10);
+ struct incomplete *inc = malloc((unsigned long)10);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle
index baa036c870fb4e23d59d27155db86156ea9f5bfb..fd611034c64ab0b4253de89eaf7e4e2453515080 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle
@@ -9,7 +9,7 @@ axiomatic dynamic_allocation {
reads __fc_heap_status;
axiom never_allocable{L}:
- ∀ ℤ i; i < 0 ∧ i > 4294967295 ⇒ ¬is_allocable(i);
+ ∀ ℤ i; i < 0 ∧ i > 18446744073709551615 ⇒ ¬is_allocable(i);
}
@@ -117,7 +117,7 @@ int *malloc_int(size_t size)
void foo(void)
{
int *p = malloc_int(sizeof(int));
- int *q = calloc_int((unsigned int)2,sizeof(int));
+ int *q = calloc_int((unsigned long)2,sizeof(int));
free_int(p);
free_int(q);
return;
@@ -135,7 +135,7 @@ axiomatic dynamic_allocation {
reads __fc_heap_status;
axiom never_allocable{L}:
- ∀ ℤ i; i < 0 ∧ i > 4294967295 ⇒ ¬is_allocable(i);
+ ∀ ℤ i; i < 0 ∧ i > 18446744073709551615 ⇒ ¬is_allocable(i);
}
@@ -244,7 +244,7 @@ int *malloc_int(size_t size)
void foo(void)
{
int *p = malloc_int(sizeof(int));
- int *q = calloc_int((unsigned int)2,sizeof(int));
+ int *q = calloc_int((unsigned long)2,sizeof(int));
free_int(p);
free_int(q);
return;
diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index 1f82bcd57b000001f672deb6a8e1f9f34dd3f699..dd2862c8e5fdd14f69919031b75ba4948b247896 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -48,14 +48,14 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
int integer(int * /*[10]*/ s1, int * /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_int(s1,s2,(unsigned int)10 * sizeof(int));
+ tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(int));
return tmp;
}
int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_int(s1,s2,(unsigned int)10 * sizeof(named));
+ tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(named));
return tmp;
}
@@ -86,26 +86,26 @@ int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
int structure(struct X * /*[10]*/ s1, struct X * /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_st_X(s1,s2,(unsigned int)10 * sizeof(struct X));
+ tmp = memcmp_st_X(s1,s2,(unsigned long)10 * sizeof(struct X));
return tmp;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
valid_read_s1:
- \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1));
+ \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
requires
valid_read_s2:
- \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1));
+ \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
ensures
equals:
- \let __fc_len = len / 4;
+ \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 / 4 - 1))),
- (indirect: *(s2 + (0 .. len / 4 - 1)));
+ \from (indirect: *(s1 + (0 .. len / 8 - 1))),
+ (indirect: *(s2 + (0 .. len / 8 - 1)));
*/
int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{
@@ -117,7 +117,7 @@ int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
int pointers(int ** /*[10]*/ s1, int ** /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_ptr_int(s1,s2,(unsigned int)10 * sizeof(int *));
+ tmp = memcmp_ptr_int(s1,s2,(unsigned long)10 * sizeof(int *));
return tmp;
}
@@ -151,32 +151,32 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
int nested(int (*s1)[10], int (*s2)[10], int n)
{
int tmp;
- tmp = memcmp_arr10_int(s1,s2,(unsigned int)n * sizeof(int [10]));
+ tmp = memcmp_arr10_int(s1,s2,(unsigned long)n * sizeof(int [10]));
return tmp;
}
int with_void(void *s1, void *s2, int n)
{
int tmp;
- tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)10);
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)10);
return tmp;
}
int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
{
int tmp;
- tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)n);
return tmp;
}
void with_null_or_int(int * /*[10]*/ p)
{
- memcmp((void const *)0,(void const *)p,(unsigned int)10 * sizeof(int));
- memcmp((void const *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+ memcmp((void const *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+ memcmp((void const *)p,(void const *)0,(unsigned long)10 * sizeof(int));
memcmp((void const *)((int const *)42),(void const *)p,
- (unsigned int)10 * sizeof(int));
+ (unsigned long)10 * sizeof(int));
memcmp((void const *)p,(void const *)((int const *)42),
- (unsigned int)10 * sizeof(int));
+ (unsigned long)10 * sizeof(int));
return;
}
@@ -221,7 +221,7 @@ int integer(int *s1, int *s2)
{
int tmp;
tmp = memcmp_int((int const *)s1,(int const *)s2,
- (unsigned int)10 * sizeof(int));
+ (unsigned long)10 * sizeof(int));
return tmp;
}
@@ -229,7 +229,7 @@ int with_named(named *s1, named *s2)
{
int tmp;
tmp = memcmp_int((int const *)s1,(int const *)s2,
- (unsigned int)10 * sizeof(named));
+ (unsigned long)10 * sizeof(named));
return tmp;
}
@@ -262,27 +262,27 @@ int structure(struct X *s1, struct X *s2)
{
int tmp;
tmp = memcmp_st_X((struct X const *)s1,(struct X const *)s2,
- (unsigned int)10 * sizeof(struct X));
+ (unsigned long)10 * sizeof(struct X));
return tmp;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
valid_read_s1:
- \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1));
+ \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
requires
valid_read_s2:
- \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1));
+ \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
ensures
equals:
- \let __fc_len = \old(len) / 4;
+ \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 / 4 - 1))),
- (indirect: *(s2 + (0 .. len / 4 - 1)));
+ \from (indirect: *(s1 + (0 .. len / 8 - 1))),
+ (indirect: *(s2 + (0 .. len / 8 - 1)));
*/
int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{
@@ -295,7 +295,7 @@ int pointers(int **s1, int **s2)
{
int tmp;
tmp = memcmp_ptr_int((int * const *)s1,(int * const *)s2,
- (unsigned int)10 * sizeof(int *));
+ (unsigned long)10 * sizeof(int *));
return tmp;
}
@@ -331,32 +331,32 @@ int nested(int (*s1)[10], int (*s2)[10], int n)
{
int tmp;
tmp = memcmp_arr10_int((int const (*)[10])s1,(int const (*)[10])s2,
- (unsigned int)n * sizeof(int [10]));
+ (unsigned long)n * sizeof(int [10]));
return tmp;
}
int with_void(void *s1, void *s2, int n)
{
int tmp;
- tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)10);
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)10);
return tmp;
}
int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
{
int tmp;
- tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)n);
return tmp;
}
void with_null_or_int(int *p)
{
- memcmp((void const *)0,(void const *)p,(unsigned int)10 * sizeof(int));
- memcmp((void const *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+ memcmp((void const *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+ memcmp((void const *)p,(void const *)0,(unsigned long)10 * sizeof(int));
memcmp((void const *)((int const *)42),(void const *)p,
- (unsigned int)10 * sizeof(int));
+ (unsigned long)10 * sizeof(int));
memcmp((void const *)p,(void const *)((int const *)42),
- (unsigned int)10 * sizeof(int));
+ (unsigned long)10 * sizeof(int));
return;
}
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 899dd8afefc6053b12a354ddcec1ba03c5f71842..259a1cacb16867e3efdd89d5e0c0740b641955ef 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -53,15 +53,15 @@ int *memcpy_int(int *dest, int const *src, size_t len)
void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
{
- int *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(int));
- memcpy_int(src,res,(unsigned int)10 * sizeof(int));
+ int *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(int));
+ memcpy_int(src,res,(unsigned long)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));
+ named *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(named));
+ memcpy_int(src,res,(unsigned long)10 * sizeof(named));
return;
}
@@ -93,28 +93,28 @@ struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
{
- struct X *res = memcpy_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
- memcpy_st_X(src,res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memcpy_st_X(dest,src,(unsigned long)10 * sizeof(struct X));
+ memcpy_st_X(src,res,(unsigned long)10 * sizeof(struct X));
return;
}
/*@ requires
separation:
- \let __fc_len = len / 4;
+ \let __fc_len = len / 8;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
- requires aligned_end: len % 4 ≡ 0;
+ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
- \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+ \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
ensures
copied:
- \let __fc_len = len / 4;
+ \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
ensures result: \result ≡ dest;
- assigns *(dest + (0 .. len / 4 - 1)), \result;
- assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
+ assigns *(dest + (0 .. len / 8 - 1)), \result;
+ assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest;
*/
int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
@@ -126,8 +126,8 @@ int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
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 *));
+ int **res = memcpy_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
+ memcpy_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
return;
}
@@ -165,32 +165,32 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
void nested(int (*src)[10], int (*dest)[10], int 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]));
+ memcpy_arr10_int(dest,src,(unsigned long)n * sizeof(int [10]));
+ memcpy_arr10_int(src,res,(unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *src, void *dest, int n)
{
- void *res = memcpy(dest,(void const *)src,(unsigned int)n);
- memcpy(src,(void const *)res,(unsigned int)n);
+ void *res = memcpy(dest,(void const *)src,(unsigned long)n);
+ memcpy(src,(void const *)res,(unsigned long)n);
return;
}
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
struct incomplete *res =
- memcpy((void *)dest,(void const *)src,(unsigned int)n);
- memcpy((void *)src,(void const *)res,(unsigned int)n);
+ memcpy((void *)dest,(void const *)src,(unsigned long)n);
+ memcpy((void *)src,(void const *)res,(unsigned long)n);
return;
}
void with_null_or_int(int * /*[10]*/ p)
{
- memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
- memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
- memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
- memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+ memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+ memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
+ memcpy((void *)((int *)42),(void const *)p,(unsigned long)10 * sizeof(int));
+ memcpy((void *)p,(void const *)((int *)42),(unsigned long)10 * sizeof(int));
return;
}
@@ -236,16 +236,16 @@ int *memcpy_int(int *dest, int const *src, size_t len)
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));
+ memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
+ memcpy_int(src,(int const *)res,(unsigned long)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));
+ memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
+ memcpy_int(src,(int const *)res,(unsigned long)10 * sizeof(named));
return;
}
@@ -280,29 +280,29 @@ void structure(struct X *src, struct X *dest)
{
struct X *res =
memcpy_st_X(dest,(struct X const *)src,
- (unsigned int)10 * sizeof(struct X));
- memcpy_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+ (unsigned long)10 * sizeof(struct X));
+ memcpy_st_X(src,(struct X const *)res,(unsigned long)10 * sizeof(struct X));
return;
}
/*@ requires
separation:
- \let __fc_len = len / 4;
+ \let __fc_len = len / 8;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
- requires aligned_end: len % 4 ≡ 0;
+ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
- \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+ \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
ensures
copied:
- \let __fc_len = \old(len) / 4;
+ \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 / 4 - 1)), \result;
- assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
+ assigns *(dest + (0 .. len / 8 - 1)), \result;
+ assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest;
*/
int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
@@ -315,8 +315,8 @@ int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
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 *));
+ memcpy_ptr_int(dest,(int * const *)src,(unsigned long)10 * sizeof(int *));
+ memcpy_ptr_int(src,(int * const *)res,(unsigned long)10 * sizeof(int *));
return;
}
@@ -356,33 +356,33 @@ void nested(int (*src)[10], int (*dest)[10], int n)
{
int (*res)[10] =
memcpy_arr10_int(dest,(int const (*)[10])src,
- (unsigned int)n * sizeof(int [10]));
+ (unsigned long)n * sizeof(int [10]));
memcpy_arr10_int(src,(int const (*)[10])res,
- (unsigned int)n * sizeof(int [10]));
+ (unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *src, void *dest, int n)
{
- void *res = memcpy(dest,(void const *)src,(unsigned int)n);
- memcpy(src,(void const *)res,(unsigned int)n);
+ void *res = memcpy(dest,(void const *)src,(unsigned long)n);
+ memcpy(src,(void const *)res,(unsigned long)n);
return;
}
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
struct incomplete *res =
- memcpy((void *)dest,(void const *)src,(unsigned int)n);
- memcpy((void *)src,(void const *)res,(unsigned int)n);
+ memcpy((void *)dest,(void const *)src,(unsigned long)n);
+ memcpy((void *)src,(void const *)res,(unsigned long)n);
return;
}
void with_null_or_int(int *p)
{
- memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
- memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
- memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
- memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+ memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+ memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
+ memcpy((void *)((int *)42),(void const *)p,(unsigned long)10 * sizeof(int));
+ memcpy((void *)p,(void const *)((int *)42),(unsigned long)10 * sizeof(int));
return;
}
diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index f327581499bdc3f2393d4bd573a08d587761e1df..fc4bf6922137156c245f4e5f980663b4e20c8f66 100644
--- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
@@ -49,15 +49,15 @@ int *memmove_int(int *dest, int const *src, size_t len)
void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
{
- int *res = memmove_int(dest,src,(unsigned int)10 * sizeof(int));
- memmove_int(src,res,(unsigned int)10 * sizeof(int));
+ int *res = memmove_int(dest,src,(unsigned long)10 * sizeof(int));
+ memmove_int(src,res,(unsigned long)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));
+ named *res = memmove_int(dest,src,(unsigned long)10 * sizeof(named));
+ memmove_int(src,res,(unsigned long)10 * sizeof(named));
return;
}
@@ -85,24 +85,25 @@ struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
{
- struct X *res = memmove_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
- memmove_st_X(src,res,(unsigned int)10 * sizeof(struct X));
+ struct X *res =
+ memmove_st_X(dest,src,(unsigned long)10 * sizeof(struct X));
+ memmove_st_X(src,res,(unsigned long)10 * sizeof(struct X));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
- \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+ \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
ensures
moved:
- \let __fc_len = len / 4;
+ \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
ensures result: \result ≡ dest;
- assigns *(dest + (0 .. len / 4 - 1)), \result;
- assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
+ assigns *(dest + (0 .. len / 8 - 1)), \result;
+ assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest;
*/
int **memmove_ptr_int(int **dest, int * const *src, size_t len)
@@ -114,8 +115,8 @@ int **memmove_ptr_int(int **dest, int * const *src, size_t len)
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 *));
+ int **res = memmove_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
+ memmove_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
return;
}
@@ -149,32 +150,34 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
void nested(int (*src)[10], int (*dest)[10], int 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]));
+ memmove_arr10_int(dest,src,(unsigned long)n * sizeof(int [10]));
+ memmove_arr10_int(src,res,(unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *src, void *dest, int n)
{
- void *res = memmove(dest,(void const *)src,(unsigned int)n);
- memmove(src,(void const *)res,(unsigned int)n);
+ void *res = memmove(dest,(void const *)src,(unsigned long)n);
+ memmove(src,(void const *)res,(unsigned long)n);
return;
}
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
struct incomplete *res =
- memmove((void *)dest,(void const *)src,(unsigned int)n);
- memmove((void *)src,(void const *)res,(unsigned int)n);
+ memmove((void *)dest,(void const *)src,(unsigned long)n);
+ memmove((void *)src,(void const *)res,(unsigned long)n);
return;
}
void with_null_or_int(int * /*[10]*/ p)
{
- memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
- memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
- memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
- memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+ memmove((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+ memmove((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
+ memmove((void *)((int *)42),(void const *)p,
+ (unsigned long)10 * sizeof(int));
+ memmove((void *)p,(void const *)((int *)42),
+ (unsigned long)10 * sizeof(int));
return;
}
@@ -216,16 +219,16 @@ int *memmove_int(int *dest, int const *src, size_t len)
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));
+ memmove_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
+ memmove_int(src,(int const *)res,(unsigned long)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));
+ memmove_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
+ memmove_int(src,(int const *)res,(unsigned long)10 * sizeof(named));
return;
}
@@ -256,25 +259,26 @@ void structure(struct X *src, struct X *dest)
{
struct X *res =
memmove_st_X(dest,(struct X const *)src,
- (unsigned int)10 * sizeof(struct X));
- memmove_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+ (unsigned long)10 * sizeof(struct X));
+ memmove_st_X(src,(struct X const *)res,
+ (unsigned long)10 * sizeof(struct X));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+ valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
- \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+ \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
ensures
moved:
- \let __fc_len = \old(len) / 4;
+ \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 / 4 - 1)), \result;
- assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
+ assigns *(dest + (0 .. len / 8 - 1)), \result;
+ assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest;
*/
int **memmove_ptr_int(int **dest, int * const *src, size_t len)
@@ -287,8 +291,9 @@ int **memmove_ptr_int(int **dest, int * const *src, size_t len)
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 *));
+ memmove_ptr_int(dest,(int * const *)src,
+ (unsigned long)10 * sizeof(int *));
+ memmove_ptr_int(src,(int * const *)res,(unsigned long)10 * sizeof(int *));
return;
}
@@ -324,33 +329,35 @@ void nested(int (*src)[10], int (*dest)[10], int n)
{
int (*res)[10] =
memmove_arr10_int(dest,(int const (*)[10])src,
- (unsigned int)n * sizeof(int [10]));
+ (unsigned long)n * sizeof(int [10]));
memmove_arr10_int(src,(int const (*)[10])res,
- (unsigned int)n * sizeof(int [10]));
+ (unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *src, void *dest, int n)
{
- void *res = memmove(dest,(void const *)src,(unsigned int)n);
- memmove(src,(void const *)res,(unsigned int)n);
+ void *res = memmove(dest,(void const *)src,(unsigned long)n);
+ memmove(src,(void const *)res,(unsigned long)n);
return;
}
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
struct incomplete *res =
- memmove((void *)dest,(void const *)src,(unsigned int)n);
- memmove((void *)src,(void const *)res,(unsigned int)n);
+ memmove((void *)dest,(void const *)src,(unsigned long)n);
+ memmove((void *)src,(void const *)res,(unsigned long)n);
return;
}
void with_null_or_int(int *p)
{
- memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
- memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
- memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
- memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+ memmove((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+ memmove((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
+ memmove((void *)((int *)42),(void const *)p,
+ (unsigned long)10 * sizeof(int));
+ memmove((void *)p,(void const *)((int *)42),
+ (unsigned long)10 * sizeof(int));
return;
}
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
index dae2db7eba374181cfa6fe5705cbcd211dfeaed5..f0925319e7706c383fc2beb1a359ab5b0c68293f 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -39,8 +39,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char * /*[10]*/ dest)
{
- char *res = memset_char(dest,(char)0,(unsigned int)10);
- memset_char(res,(char)0,(unsigned int)10);
+ char *res = memset_char(dest,(char)0,(unsigned long)10);
+ memset_char(res,(char)0,(unsigned long)10);
return;
}
@@ -63,8 +63,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(unsigned char * /*[10]*/ dest)
{
- unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned int)10);
- memset_uchar(res,(unsigned char)0,(unsigned int)10);
+ unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned long)10);
+ memset_uchar(res,(unsigned char)0,(unsigned long)10);
return;
}
@@ -91,8 +91,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (* /*[10]*/ dest)[10])
{
- char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned int)100);
- memset_arr10_char(res,(char)0,(unsigned int)100);
+ char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned long)100);
+ memset_arr10_char(res,(char)0,(unsigned long)100);
return;
}
@@ -117,8 +117,8 @@ int *memset_int_0(int *ptr, size_t len)
void integer(int * /*[10]*/ dest)
{
- int *res = memset_int_0(dest,(unsigned int)10 * sizeof(int));
- memset_int_0(res,(unsigned int)10 * sizeof(int));
+ int *res = memset_int_0(dest,(unsigned long)10 * sizeof(int));
+ memset_int_0(res,(unsigned long)10 * sizeof(int));
return;
}
@@ -143,8 +143,8 @@ enum E *memset_e_E_0(enum E *ptr, size_t len)
void with_enum(enum E * /*[10]*/ dest)
{
- enum E *res = memset_e_E_0(dest,(unsigned int)10 * sizeof(enum E));
- memset_e_E_0(res,(unsigned int)10 * sizeof(enum E));
+ enum E *res = memset_e_E_0(dest,(unsigned long)10 * sizeof(enum E));
+ memset_e_E_0(res,(unsigned long)10 * sizeof(enum E));
return;
}
@@ -169,15 +169,15 @@ float *memset_float_0(float *ptr, size_t len)
void floats(float * /*[10]*/ dest)
{
- float *res = memset_float_0(dest,(unsigned int)10 * sizeof(float));
- memset_float_0(res,(unsigned int)10 * sizeof(float));
+ float *res = memset_float_0(dest,(unsigned long)10 * sizeof(float));
+ memset_float_0(res,(unsigned long)10 * sizeof(float));
return;
}
void with_named(named * /*[10]*/ dest)
{
- named *res = memset_int_0(dest,(unsigned int)10 * sizeof(named));
- memset_int_0(res,(unsigned int)10 * sizeof(named));
+ named *res = memset_int_0(dest,(unsigned long)10 * sizeof(named));
+ memset_int_0(res,(unsigned long)10 * sizeof(named));
return;
}
@@ -203,21 +203,21 @@ struct X *memset_st_X_0(struct X *ptr, size_t len)
void structure(struct X * /*[10]*/ dest)
{
- struct X *res = memset_st_X_0(dest,(unsigned int)10 * sizeof(struct X));
- memset_st_X_0(res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memset_st_X_0(dest,(unsigned long)10 * sizeof(struct X));
+ memset_st_X_0(res,(unsigned long)10 * sizeof(struct X));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \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 = len / 4;
+ \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ \null;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. len / 4 - 1)), \result;
- assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
int **memset_ptr_int_0(int **ptr, size_t len)
@@ -229,8 +229,8 @@ int **memset_ptr_int_0(int **ptr, size_t len)
void pointers(int ** /*[10]*/ dest)
{
- int **res = memset_ptr_int_0(dest,(unsigned int)10 * sizeof(int *));
- memset_ptr_int_0(res,(unsigned int)10 * sizeof(int *));
+ int **res = memset_ptr_int_0(dest,(unsigned long)10 * sizeof(int *));
+ memset_ptr_int_0(res,(unsigned long)10 * sizeof(int *));
return;
}
@@ -258,22 +258,22 @@ int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10]
void nested(int (*dest)[10], int n)
{
int (*res)[10] =
- memset_arr10_int_0(dest,(unsigned int)n * sizeof(int [10]));
- memset_arr10_int_0(res,(unsigned int)n * sizeof(int [10]));
+ memset_arr10_int_0(dest,(unsigned long)n * sizeof(int [10]));
+ memset_arr10_int_0(res,(unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *dest)
{
- void *res = memset(dest,0,(unsigned int)10);
- memset(res,0,(unsigned int)10);
+ void *res = memset(dest,0,(unsigned long)10);
+ memset(res,0,(unsigned long)10);
return;
}
void with_null_or_int(void)
{
- memset((void *)0,0,(unsigned int)10);
- memset((void *)((int *)42),0,(unsigned int)10);
+ memset((void *)0,0,(unsigned long)10);
+ memset((void *)((int *)42),0,(unsigned long)10);
return;
}
@@ -313,8 +313,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char *dest)
{
- char *res = memset_char(dest,(char)0,(unsigned int)10);
- memset_char(res,(char)0,(unsigned int)10);
+ char *res = memset_char(dest,(char)0,(unsigned long)10);
+ memset_char(res,(char)0,(unsigned long)10);
return;
}
@@ -339,8 +339,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(unsigned char *dest)
{
- unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned int)10);
- memset_uchar(res,(unsigned char)0,(unsigned int)10);
+ unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned long)10);
+ memset_uchar(res,(unsigned char)0,(unsigned long)10);
return;
}
@@ -368,8 +368,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (*dest)[10])
{
- char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned int)100);
- memset_arr10_char(res,(char)0,(unsigned int)100);
+ char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned long)100);
+ memset_arr10_char(res,(char)0,(unsigned long)100);
return;
}
@@ -394,8 +394,8 @@ int *memset_int_0(int *ptr, size_t len)
void integer(int *dest)
{
- int *res = memset_int_0(dest,(unsigned int)10 * sizeof(int));
- memset_int_0(res,(unsigned int)10 * sizeof(int));
+ int *res = memset_int_0(dest,(unsigned long)10 * sizeof(int));
+ memset_int_0(res,(unsigned long)10 * sizeof(int));
return;
}
@@ -420,8 +420,8 @@ enum E *memset_e_E_0(enum E *ptr, size_t len)
void with_enum(enum E *dest)
{
- enum E *res = memset_e_E_0(dest,(unsigned int)10 * sizeof(enum E));
- memset_e_E_0(res,(unsigned int)10 * sizeof(enum E));
+ enum E *res = memset_e_E_0(dest,(unsigned long)10 * sizeof(enum E));
+ memset_e_E_0(res,(unsigned long)10 * sizeof(enum E));
return;
}
@@ -446,15 +446,15 @@ float *memset_float_0(float *ptr, size_t len)
void floats(float *dest)
{
- float *res = memset_float_0(dest,(unsigned int)10 * sizeof(float));
- memset_float_0(res,(unsigned int)10 * sizeof(float));
+ float *res = memset_float_0(dest,(unsigned long)10 * sizeof(float));
+ memset_float_0(res,(unsigned long)10 * sizeof(float));
return;
}
void with_named(named *dest)
{
- named *res = memset_int_0(dest,(unsigned int)10 * sizeof(named));
- memset_int_0(res,(unsigned int)10 * sizeof(named));
+ named *res = memset_int_0(dest,(unsigned long)10 * sizeof(named));
+ memset_int_0(res,(unsigned long)10 * sizeof(named));
return;
}
@@ -481,21 +481,21 @@ struct X *memset_st_X_0(struct X *ptr, size_t len)
void structure(struct X *dest)
{
- struct X *res = memset_st_X_0(dest,(unsigned int)10 * sizeof(struct X));
- memset_st_X_0(res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memset_st_X_0(dest,(unsigned long)10 * sizeof(struct X));
+ memset_st_X_0(res,(unsigned long)10 * sizeof(struct X));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \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(len) / 4;
+ \let __fc_len = \old(len) / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ \null;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. len / 4 - 1)), \result;
- assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
int **memset_ptr_int_0(int **ptr, size_t len)
@@ -507,8 +507,8 @@ int **memset_ptr_int_0(int **ptr, size_t len)
void pointers(int **dest)
{
- int **res = memset_ptr_int_0(dest,(unsigned int)10 * sizeof(int *));
- memset_ptr_int_0(res,(unsigned int)10 * sizeof(int *));
+ int **res = memset_ptr_int_0(dest,(unsigned long)10 * sizeof(int *));
+ memset_ptr_int_0(res,(unsigned long)10 * sizeof(int *));
return;
}
@@ -536,22 +536,22 @@ int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10]
void nested(int (*dest)[10], int n)
{
int (*res)[10] =
- memset_arr10_int_0(dest,(unsigned int)n * sizeof(int [10]));
- memset_arr10_int_0(res,(unsigned int)n * sizeof(int [10]));
+ memset_arr10_int_0(dest,(unsigned long)n * sizeof(int [10]));
+ memset_arr10_int_0(res,(unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *dest)
{
- void *res = memset(dest,0,(unsigned int)10);
- memset(res,0,(unsigned int)10);
+ void *res = memset(dest,0,(unsigned long)10);
+ memset(res,0,(unsigned long)10);
return;
}
void with_null_or_int(void)
{
- memset((void *)0,0,(unsigned int)10);
- memset((void *)((int *)42),0,(unsigned int)10);
+ memset((void *)0,0,(unsigned long)10);
+ memset((void *)((int *)42),0,(unsigned long)10);
return;
}
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
index 137dd1c21a070c374f27367c3e82beb2b47a79aa..798296c18a980b5a0097406083c7dc48f66302de 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -39,8 +39,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char * /*[10]*/ dest)
{
- char *res = memset_char(dest,(char)0xFF,(unsigned int)10);
- memset_char(res,(char)0xFF,(unsigned int)10);
+ char *res = memset_char(dest,(char)0xFF,(unsigned long)10);
+ memset_char(res,(char)0xFF,(unsigned long)10);
return;
}
@@ -64,8 +64,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(unsigned char * /*[10]*/ dest)
{
unsigned char *res =
- memset_uchar(dest,(unsigned char)0xFF,(unsigned int)10);
- memset_uchar(res,(unsigned char)0xFF,(unsigned int)10);
+ memset_uchar(dest,(unsigned char)0xFF,(unsigned long)10);
+ memset_uchar(res,(unsigned char)0xFF,(unsigned long)10);
return;
}
@@ -92,8 +92,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (* /*[10]*/ dest)[10])
{
- char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned int)100);
- memset_arr10_char(res,(char)0xFF,(unsigned int)100);
+ char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned long)100);
+ memset_arr10_char(res,(char)0xFF,(unsigned long)100);
return;
}
@@ -118,8 +118,8 @@ int *memset_int_FF(int *ptr, size_t len)
void integer(int * /*[10]*/ dest)
{
- int *res = memset_int_FF(dest,(unsigned int)10 * sizeof(int));
- memset_int_FF(res,(unsigned int)10 * sizeof(int));
+ int *res = memset_int_FF(dest,(unsigned long)10 * sizeof(int));
+ memset_int_FF(res,(unsigned long)10 * sizeof(int));
return;
}
@@ -144,8 +144,8 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len)
void with_enum(enum E * /*[10]*/ dest)
{
- enum E *res = memset_e_E_FF(dest,(unsigned int)10 * sizeof(enum E));
- memset_e_E_FF(res,(unsigned int)10 * sizeof(enum E));
+ enum E *res = memset_e_E_FF(dest,(unsigned long)10 * sizeof(enum E));
+ memset_e_E_FF(res,(unsigned long)10 * sizeof(enum E));
return;
}
@@ -171,21 +171,21 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
void unsigned_integer(unsigned int * /*[10]*/ dest)
{
unsigned int *res =
- memset_uint_FF(dest,(unsigned int)10 * sizeof(unsigned int));
- memset_uint_FF(res,(unsigned int)10 * sizeof(unsigned int));
+ memset_uint_FF(dest,(unsigned long)10 * sizeof(unsigned int));
+ memset_uint_FF(res,(unsigned long)10 * sizeof(unsigned int));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \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 = len / 4;
+ \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((long)0);
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. len / 4 - 1)), \result;
- assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
long *memset_long_FF(long *ptr, size_t len)
@@ -197,21 +197,22 @@ long *memset_long_FF(long *ptr, size_t len)
void long_integer(long * /*[10]*/ dest)
{
- long *res = memset_long_FF(dest,(unsigned int)10 * sizeof(long));
- memset_long_FF(res,(unsigned int)10 * sizeof(long));
+ long *res = memset_long_FF(dest,(unsigned long)10 * sizeof(long));
+ memset_long_FF(res,(unsigned long)10 * sizeof(long));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \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 = len / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 4294967295;
+ \let __fc_len = len / 8;
+ ∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 18446744073709551615;
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. len / 4 - 1)), \result;
- assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
@@ -224,8 +225,8 @@ unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
void unsigned_long_integer(unsigned long * /*[10]*/ dest)
{
unsigned long *res =
- memset_ulong_FF(dest,(unsigned int)10 * sizeof(unsigned long));
- memset_ulong_FF(res,(unsigned int)10 * sizeof(unsigned long));
+ memset_ulong_FF(dest,(unsigned long)10 * sizeof(unsigned long));
+ memset_ulong_FF(res,(unsigned long)10 * sizeof(unsigned long));
return;
}
@@ -251,8 +252,8 @@ long long *memset_llong_FF(long long *ptr, size_t len)
void long_long_integer(long long * /*[10]*/ dest)
{
long long *res =
- memset_llong_FF(dest,(unsigned int)10 * sizeof(long long));
- memset_llong_FF(res,(unsigned int)10 * sizeof(long long));
+ memset_llong_FF(dest,(unsigned long)10 * sizeof(long long));
+ memset_llong_FF(res,(unsigned long)10 * sizeof(long long));
return;
}
@@ -279,8 +280,8 @@ unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len)
void unsigned_long_long_integer(unsigned long long * /*[10]*/ dest)
{
unsigned long long *res =
- memset_ullong_FF(dest,(unsigned int)10 * sizeof(unsigned long long));
- memset_ullong_FF(res,(unsigned int)10 * sizeof(unsigned long long));
+ memset_ullong_FF(dest,(unsigned long)10 * sizeof(unsigned long long));
+ memset_ullong_FF(res,(unsigned long)10 * sizeof(unsigned long long));
return;
}
@@ -305,15 +306,15 @@ float *memset_float_FF(float *ptr, size_t len)
void floats(float * /*[10]*/ dest)
{
- float *res = memset_float_FF(dest,(unsigned int)10 * sizeof(float));
- memset_float_FF(res,(unsigned int)10 * sizeof(float));
+ float *res = memset_float_FF(dest,(unsigned long)10 * sizeof(float));
+ memset_float_FF(res,(unsigned long)10 * sizeof(float));
return;
}
void with_named(named * /*[10]*/ dest)
{
- named *res = memset_int_FF(dest,(unsigned int)10 * sizeof(named));
- memset_int_FF(res,(unsigned int)10 * sizeof(named));
+ named *res = memset_int_FF(dest,(unsigned long)10 * sizeof(named));
+ memset_int_FF(res,(unsigned long)10 * sizeof(named));
return;
}
@@ -340,21 +341,21 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len)
void structure(struct X * /*[10]*/ dest)
{
- struct X *res = memset_st_X_FF(dest,(unsigned int)10 * sizeof(struct X));
- memset_st_X_FF(res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memset_st_X_FF(dest,(unsigned long)10 * sizeof(struct X));
+ memset_st_X_FF(res,(unsigned long)10 * sizeof(struct X));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \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 = len / 4;
+ \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(ptr + j0));
ensures result: \result ≡ ptr;
- assigns *(ptr + (0 .. len / 4 - 1)), \result;
- assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
int **memset_ptr_int_FF(int **ptr, size_t len)
@@ -366,8 +367,8 @@ int **memset_ptr_int_FF(int **ptr, size_t len)
void pointers(int ** /*[10]*/ dest)
{
- int **res = memset_ptr_int_FF(dest,(unsigned int)10 * sizeof(int *));
- memset_ptr_int_FF(res,(unsigned int)10 * sizeof(int *));
+ int **res = memset_ptr_int_FF(dest,(unsigned long)10 * sizeof(int *));
+ memset_ptr_int_FF(res,(unsigned long)10 * sizeof(int *));
return;
}
@@ -395,22 +396,22 @@ int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10]
void nested(int (*dest)[10], int n)
{
int (*res)[10] =
- memset_arr10_int_FF(dest,(unsigned int)n * sizeof(int [10]));
- memset_arr10_int_FF(res,(unsigned int)n * sizeof(int [10]));
+ memset_arr10_int_FF(dest,(unsigned long)n * sizeof(int [10]));
+ memset_arr10_int_FF(res,(unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *dest)
{
- void *res = memset(dest,0xFF,(unsigned int)10);
- memset(res,0xFF,(unsigned int)10);
+ void *res = memset(dest,0xFF,(unsigned long)10);
+ memset(res,0xFF,(unsigned long)10);
return;
}
void with_null_or_int(void)
{
- memset((void *)0,0xFF,(unsigned int)10);
- memset((void *)((int *)42),0xFF,(unsigned int)10);
+ memset((void *)0,0xFF,(unsigned long)10);
+ memset((void *)((int *)42),0xFF,(unsigned long)10);
return;
}
@@ -450,8 +451,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char *dest)
{
- char *res = memset_char(dest,(char)0xFF,(unsigned int)10);
- memset_char(res,(char)0xFF,(unsigned int)10);
+ char *res = memset_char(dest,(char)0xFF,(unsigned long)10);
+ memset_char(res,(char)0xFF,(unsigned long)10);
return;
}
@@ -477,8 +478,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(unsigned char *dest)
{
unsigned char *res =
- memset_uchar(dest,(unsigned char)0xFF,(unsigned int)10);
- memset_uchar(res,(unsigned char)0xFF,(unsigned int)10);
+ memset_uchar(dest,(unsigned char)0xFF,(unsigned long)10);
+ memset_uchar(res,(unsigned char)0xFF,(unsigned long)10);
return;
}
@@ -506,8 +507,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (*dest)[10])
{
- char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned int)100);
- memset_arr10_char(res,(char)0xFF,(unsigned int)100);
+ char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned long)100);
+ memset_arr10_char(res,(char)0xFF,(unsigned long)100);
return;
}
@@ -532,8 +533,8 @@ int *memset_int_FF(int *ptr, size_t len)
void integer(int *dest)
{
- int *res = memset_int_FF(dest,(unsigned int)10 * sizeof(int));
- memset_int_FF(res,(unsigned int)10 * sizeof(int));
+ int *res = memset_int_FF(dest,(unsigned long)10 * sizeof(int));
+ memset_int_FF(res,(unsigned long)10 * sizeof(int));
return;
}
@@ -558,8 +559,8 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len)
void with_enum(enum E *dest)
{
- enum E *res = memset_e_E_FF(dest,(unsigned int)10 * sizeof(enum E));
- memset_e_E_FF(res,(unsigned int)10 * sizeof(enum E));
+ enum E *res = memset_e_E_FF(dest,(unsigned long)10 * sizeof(enum E));
+ memset_e_E_FF(res,(unsigned long)10 * sizeof(enum E));
return;
}
@@ -585,21 +586,21 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
void unsigned_integer(unsigned int *dest)
{
unsigned int *res =
- memset_uint_FF(dest,(unsigned int)10 * sizeof(unsigned int));
- memset_uint_FF(res,(unsigned int)10 * sizeof(unsigned int));
+ memset_uint_FF(dest,(unsigned long)10 * sizeof(unsigned int));
+ memset_uint_FF(res,(unsigned long)10 * sizeof(unsigned int));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \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(len) / 4;
+ \let __fc_len = \old(len) / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((long)0);
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. len / 4 - 1)), \result;
- assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
long *memset_long_FF(long *ptr, size_t len)
@@ -611,21 +612,22 @@ long *memset_long_FF(long *ptr, size_t len)
void long_integer(long *dest)
{
- long *res = memset_long_FF(dest,(unsigned int)10 * sizeof(long));
- memset_long_FF(res,(unsigned int)10 * sizeof(long));
+ long *res = memset_long_FF(dest,(unsigned long)10 * sizeof(long));
+ memset_long_FF(res,(unsigned long)10 * sizeof(long));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \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(len) / 4;
- ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 4294967295;
+ \let __fc_len = \old(len) / 8;
+ ∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 18446744073709551615;
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. len / 4 - 1)), \result;
- assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
@@ -638,8 +640,8 @@ unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
void unsigned_long_integer(unsigned long *dest)
{
unsigned long *res =
- memset_ulong_FF(dest,(unsigned int)10 * sizeof(unsigned long));
- memset_ulong_FF(res,(unsigned int)10 * sizeof(unsigned long));
+ memset_ulong_FF(dest,(unsigned long)10 * sizeof(unsigned long));
+ memset_ulong_FF(res,(unsigned long)10 * sizeof(unsigned long));
return;
}
@@ -666,8 +668,8 @@ long long *memset_llong_FF(long long *ptr, size_t len)
void long_long_integer(long long *dest)
{
long long *res =
- memset_llong_FF(dest,(unsigned int)10 * sizeof(long long));
- memset_llong_FF(res,(unsigned int)10 * sizeof(long long));
+ memset_llong_FF(dest,(unsigned long)10 * sizeof(long long));
+ memset_llong_FF(res,(unsigned long)10 * sizeof(long long));
return;
}
@@ -694,8 +696,8 @@ unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len)
void unsigned_long_long_integer(unsigned long long *dest)
{
unsigned long long *res =
- memset_ullong_FF(dest,(unsigned int)10 * sizeof(unsigned long long));
- memset_ullong_FF(res,(unsigned int)10 * sizeof(unsigned long long));
+ memset_ullong_FF(dest,(unsigned long)10 * sizeof(unsigned long long));
+ memset_ullong_FF(res,(unsigned long)10 * sizeof(unsigned long long));
return;
}
@@ -720,15 +722,15 @@ float *memset_float_FF(float *ptr, size_t len)
void floats(float *dest)
{
- float *res = memset_float_FF(dest,(unsigned int)10 * sizeof(float));
- memset_float_FF(res,(unsigned int)10 * sizeof(float));
+ float *res = memset_float_FF(dest,(unsigned long)10 * sizeof(float));
+ memset_float_FF(res,(unsigned long)10 * sizeof(float));
return;
}
void with_named(named *dest)
{
- named *res = memset_int_FF(dest,(unsigned int)10 * sizeof(named));
- memset_int_FF(res,(unsigned int)10 * sizeof(named));
+ named *res = memset_int_FF(dest,(unsigned long)10 * sizeof(named));
+ memset_int_FF(res,(unsigned long)10 * sizeof(named));
return;
}
@@ -756,21 +758,21 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len)
void structure(struct X *dest)
{
- struct X *res = memset_st_X_FF(dest,(unsigned int)10 * sizeof(struct X));
- memset_st_X_FF(res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memset_st_X_FF(dest,(unsigned long)10 * sizeof(struct X));
+ memset_st_X_FF(res,(unsigned long)10 * sizeof(struct X));
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
requires
- valid_dest: \let __fc_len = len / 4; \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(len) / 4;
+ \let __fc_len = \old(len) / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(\old(ptr) + j0));
ensures result: \result ≡ \old(ptr);
- assigns *(ptr + (0 .. len / 4 - 1)), \result;
- assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+ assigns *(ptr + (0 .. len / 8 - 1)), \result;
+ assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr;
*/
int **memset_ptr_int_FF(int **ptr, size_t len)
@@ -782,8 +784,8 @@ int **memset_ptr_int_FF(int **ptr, size_t len)
void pointers(int **dest)
{
- int **res = memset_ptr_int_FF(dest,(unsigned int)10 * sizeof(int *));
- memset_ptr_int_FF(res,(unsigned int)10 * sizeof(int *));
+ int **res = memset_ptr_int_FF(dest,(unsigned long)10 * sizeof(int *));
+ memset_ptr_int_FF(res,(unsigned long)10 * sizeof(int *));
return;
}
@@ -812,22 +814,22 @@ int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10]
void nested(int (*dest)[10], int n)
{
int (*res)[10] =
- memset_arr10_int_FF(dest,(unsigned int)n * sizeof(int [10]));
- memset_arr10_int_FF(res,(unsigned int)n * sizeof(int [10]));
+ memset_arr10_int_FF(dest,(unsigned long)n * sizeof(int [10]));
+ memset_arr10_int_FF(res,(unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *dest)
{
- void *res = memset(dest,0xFF,(unsigned int)10);
- memset(res,0xFF,(unsigned int)10);
+ void *res = memset(dest,0xFF,(unsigned long)10);
+ memset(res,0xFF,(unsigned long)10);
return;
}
void with_null_or_int(void)
{
- memset((void *)0,0xFF,(unsigned int)10);
- memset((void *)((int *)42),0xFF,(unsigned int)10);
+ memset((void *)0,0xFF,(unsigned long)10);
+ memset((void *)((int *)42),0xFF,(unsigned long)10);
return;
}
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
index 5ece8370f6baf098afc773974cb82a40f53df732..d355aff8a40e29537ff7c18ffb93fd057512fd4b 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -68,8 +68,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char * /*[10]*/ dest, char value)
{
- char *res = memset_char(dest,value,(unsigned int)10);
- memset_char(res,value,(unsigned int)10);
+ char *res = memset_char(dest,value,(unsigned long)10);
+ memset_char(res,value,(unsigned long)10);
return;
}
@@ -92,8 +92,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(char * /*[10]*/ dest, unsigned char value)
{
- unsigned char *res = memset_char(dest,(char)value,(unsigned int)10);
- memset_uchar(res,value,(unsigned int)10);
+ unsigned char *res = memset_char(dest,(char)value,(unsigned long)10);
+ memset_uchar(res,value,(unsigned long)10);
return;
}
@@ -120,73 +120,74 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (* /*[10]*/ dest)[10], char value)
{
- char (*res)[10] = memset_arr10_char(dest,value,(unsigned int)100);
- memset_arr10_char(res,value,(unsigned int)100);
+ char (*res)[10] = memset_arr10_char(dest,value,(unsigned long)100);
+ memset_arr10_char(res,value,(unsigned long)100);
return;
}
void integer(int * /*[10]*/ dest, int value)
{
- int *res = memset((void *)dest,value,(unsigned int)10 * sizeof(int));
- memset((void *)res,value,(unsigned int)10 * sizeof(int));
+ int *res = memset((void *)dest,value,(unsigned long)10 * sizeof(int));
+ memset((void *)res,value,(unsigned long)10 * sizeof(int));
return;
}
void with_enum(enum E * /*[10]*/ dest, int value)
{
- enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E));
- memset((void *)res,value,(unsigned int)10 * sizeof(enum E));
+ enum E *res =
+ memset((void *)dest,value,(unsigned long)10 * sizeof(enum E));
+ memset((void *)res,value,(unsigned long)10 * sizeof(enum E));
return;
}
void with_named(named * /*[10]*/ dest, int value)
{
- named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named));
- memset((void *)res,value,(unsigned int)10 * sizeof(named));
+ named *res = memset((void *)dest,value,(unsigned long)10 * sizeof(named));
+ memset((void *)res,value,(unsigned long)10 * sizeof(named));
return;
}
void structure(struct X * /*[10]*/ dest, int value)
{
struct X *res =
- memset((void *)dest,value,(unsigned int)10 * sizeof(struct X));
- memset((void *)res,value,(unsigned int)10 * sizeof(struct X));
+ memset((void *)dest,value,(unsigned long)10 * sizeof(struct X));
+ memset((void *)res,value,(unsigned long)10 * sizeof(struct X));
return;
}
void pointers(int ** /*[10]*/ dest, int value)
{
- int **res = memset((void *)dest,value,(unsigned int)10 * sizeof(int *));
- memset((void *)res,value,(unsigned int)10 * sizeof(int *));
+ int **res = memset((void *)dest,value,(unsigned long)10 * sizeof(int *));
+ memset((void *)res,value,(unsigned long)10 * sizeof(int *));
return;
}
void nested(int (*dest)[10], int n, int value)
{
int (*res)[10] =
- memset((void *)dest,value,(unsigned int)n * sizeof(int [10]));
- memset((void *)res,value,(unsigned int)n * sizeof(int [10]));
+ memset((void *)dest,value,(unsigned long)n * sizeof(int [10]));
+ memset((void *)res,value,(unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *dest, int value)
{
- void *res = memset(dest,value,(unsigned int)10);
- memset(res,value,(unsigned int)10);
+ void *res = memset(dest,value,(unsigned long)10);
+ memset(res,value,(unsigned long)10);
return;
}
void with_incomplete(struct incomplete *dest, int value)
{
- struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
- memset((void *)res,value,(unsigned int)10);
+ struct incomplete *res = memset((void *)dest,value,(unsigned long)10);
+ memset((void *)res,value,(unsigned long)10);
return;
}
void with_null_or_int(int value)
{
- memset((void *)0,value,(unsigned int)10);
- memset((void *)((int *)42),value,(unsigned int)10);
+ memset((void *)0,value,(unsigned long)10);
+ memset((void *)((int *)42),value,(unsigned long)10);
return;
}
@@ -227,8 +228,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char *dest, char value)
{
- char *res = memset_char(dest,value,(unsigned int)10);
- memset_char(res,value,(unsigned int)10);
+ char *res = memset_char(dest,value,(unsigned long)10);
+ memset_char(res,value,(unsigned long)10);
return;
}
@@ -253,8 +254,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(char *dest, unsigned char value)
{
- unsigned char *res = memset_char(dest,(char)value,(unsigned int)10);
- memset_uchar(res,value,(unsigned int)10);
+ unsigned char *res = memset_char(dest,(char)value,(unsigned long)10);
+ memset_uchar(res,value,(unsigned long)10);
return;
}
@@ -282,73 +283,74 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (*dest)[10], char value)
{
- char (*res)[10] = memset_arr10_char(dest,value,(unsigned int)100);
- memset_arr10_char(res,value,(unsigned int)100);
+ char (*res)[10] = memset_arr10_char(dest,value,(unsigned long)100);
+ memset_arr10_char(res,value,(unsigned long)100);
return;
}
void integer(int *dest, int value)
{
- int *res = memset((void *)dest,value,(unsigned int)10 * sizeof(int));
- memset((void *)res,value,(unsigned int)10 * sizeof(int));
+ int *res = memset((void *)dest,value,(unsigned long)10 * sizeof(int));
+ memset((void *)res,value,(unsigned long)10 * sizeof(int));
return;
}
void with_enum(enum E *dest, int value)
{
- enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E));
- memset((void *)res,value,(unsigned int)10 * sizeof(enum E));
+ enum E *res =
+ memset((void *)dest,value,(unsigned long)10 * sizeof(enum E));
+ memset((void *)res,value,(unsigned long)10 * sizeof(enum E));
return;
}
void with_named(named *dest, int value)
{
- named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named));
- memset((void *)res,value,(unsigned int)10 * sizeof(named));
+ named *res = memset((void *)dest,value,(unsigned long)10 * sizeof(named));
+ memset((void *)res,value,(unsigned long)10 * sizeof(named));
return;
}
void structure(struct X *dest, int value)
{
struct X *res =
- memset((void *)dest,value,(unsigned int)10 * sizeof(struct X));
- memset((void *)res,value,(unsigned int)10 * sizeof(struct X));
+ memset((void *)dest,value,(unsigned long)10 * sizeof(struct X));
+ memset((void *)res,value,(unsigned long)10 * sizeof(struct X));
return;
}
void pointers(int **dest, int value)
{
- int **res = memset((void *)dest,value,(unsigned int)10 * sizeof(int *));
- memset((void *)res,value,(unsigned int)10 * sizeof(int *));
+ int **res = memset((void *)dest,value,(unsigned long)10 * sizeof(int *));
+ memset((void *)res,value,(unsigned long)10 * sizeof(int *));
return;
}
void nested(int (*dest)[10], int n, int value)
{
int (*res)[10] =
- memset((void *)dest,value,(unsigned int)n * sizeof(int [10]));
- memset((void *)res,value,(unsigned int)n * sizeof(int [10]));
+ memset((void *)dest,value,(unsigned long)n * sizeof(int [10]));
+ memset((void *)res,value,(unsigned long)n * sizeof(int [10]));
return;
}
void with_void(void *dest, int value)
{
- void *res = memset(dest,value,(unsigned int)10);
- memset(res,value,(unsigned int)10);
+ void *res = memset(dest,value,(unsigned long)10);
+ memset(res,value,(unsigned long)10);
return;
}
void with_incomplete(struct incomplete *dest, int value)
{
- struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
- memset((void *)res,value,(unsigned int)10);
+ struct incomplete *res = memset((void *)dest,value,(unsigned long)10);
+ memset((void *)res,value,(unsigned long)10);
return;
}
void with_null_or_int(int value)
{
- memset((void *)0,value,(unsigned int)10);
- memset((void *)((int *)42),value,(unsigned int)10);
+ memset((void *)0,value,(unsigned long)10);
+ memset((void *)((int *)42),value,(unsigned long)10);
return;
}
diff --git a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
index 7369a68d0b2dff785f411483c5f39da4584de845..8b7c3751760dd97356c018c963be9e2e7b33ef1b 100644
--- a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
@@ -53,7 +53,7 @@ int *pack(int first, void * const *__va_params)
if (! tmp) break;
size ++;
}
- ret = (int *)malloc(sizeof(int) * (unsigned int)(size + 1));
+ ret = (int *)malloc(sizeof(int) * (unsigned long)(size + 1));
*(ret + 0) = first;
list = __va_params;
i = 0;
diff --git a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
index 83a0ba4f9cf11e5afd51b149f043b7ed155f2658..f67c309b1b9ea8688ab4937b23366b6d7178504f 100644
--- a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
@@ -54,7 +54,7 @@ int *pack(int first, void * const *__va_params)
if (! tmp) break;
size ++;
}
- ret = (int *)malloc(sizeof(int) * (unsigned int)(size + 1));
+ ret = (int *)malloc(sizeof(int) * (unsigned long)(size + 1));
*(ret + 0) = first;
i = 0;
while (i < size) {
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 5dfc5110fbc51a13382b0667c59193994327797f..cac34c3b81106e48fc46ce258937ba54cea5230e 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -468,7 +468,7 @@ int printf_va_18(char const * __restrict format, size_t param0,
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_19(char const * __restrict format, unsigned long long param0);
+int printf_va_19(char const * __restrict format, unsigned long param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -494,7 +494,7 @@ int printf_va_20(char const * __restrict format, int param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_21(char const * __restrict format, unsigned long long param0);
+int printf_va_21(char const * __restrict format, unsigned long param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -617,9 +617,9 @@ int main(void)
uintmax_t uj = (unsigned long long)42;
double f = (double)42.0f;
long double L = 42.0l;
- uint64_t u64 = (unsigned long long)42ul;
+ uint64_t u64 = 42ul;
int8_t i8 = (signed char)42;
- uint_least64_t uleast64 = (unsigned long long)42u;
+ uint_least64_t uleast64 = (unsigned long)42u;
int_fast32_t ifast32 = 42;
printf("Hello world !\n"); /* printf_va_1 */
printf("%s%n",string,& i); /* printf_va_2 */
@@ -639,9 +639,9 @@ int main(void)
printf("%llu ",ull); /* printf_va_16 */
printf("%jo ",uj); /* printf_va_17 */
printf("%zx %tX\n",z,t); /* printf_va_18 */
- printf("%llu",u64); /* printf_va_19 */
+ printf("%lu",u64); /* printf_va_19 */
printf("%hhi",(int)i8); /* printf_va_20 */
- printf("%llx",uleast64); /* printf_va_21 */
+ printf("%lx",uleast64); /* printf_va_21 */
printf("%d",ifast32); /* printf_va_22 */
printf("%f %Le\n",f,L); /* printf_va_23 */
printf("%c\n",(int)c); /* printf_va_24 */
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 18e298855651f28719771d12be1b821e2af2e8ee..3cecd8f9b1e42365b8af2c9e3217c941bd59aea4 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -26,7 +26,7 @@
The imprecision originates from Arithmetic
{tests/known/printf_garbled_mix.c:6}
[eva:alarm] tests/known/printf_garbled_mix.c:7: Warning:
- pointer downcast. assert (unsigned int)b ≤ 2147483647;
+ pointer downcast. assert (unsigned long)b ≤ 2147483647;
[eva] using specification for function printf_va_1
[eva] tests/known/printf_garbled_mix.c:8:
Frama_C_show_each_nb_printed: [-2147483648..2147483647]
@@ -68,8 +68,8 @@ int printf_va_1(char const * __restrict format, int param0);
void main(void)
{
int a[2] = {1, 2};
- int *b = (int *)((unsigned int)(a) * (unsigned int)2);
- /*@ assert Eva: pointer_downcast: (unsigned int)b ≤ 2147483647; */
+ int *b = (int *)((unsigned long)(a) * (unsigned long)2);
+ /*@ assert Eva: pointer_downcast: (unsigned long)b ≤ 2147483647; */
int nb_printed = printf_va_1("%d",(int)b);
Frama_C_show_each_nb_printed(nb_printed);
b = (int *)0;
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index e7804a787db53d028ac81c30cf7c26577f43b559..a9e71214ada7413c87b1325f0974ba0acf0d8d72 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -438,12 +438,20 @@ int main(void)
Incorrect type for argument 2. The argument will be cast from int to unsigned int.
[variadic] tests/known/printf_wrong_types.c:21:
Translating call to printf to a call to the specialized version printf_va_4.
+[variadic] tests/known/printf_wrong_types.c:21: Warning:
+ Incorrect type for argument 2. The argument will be cast from int to long.
[variadic] tests/known/printf_wrong_types.c:22:
Translating call to printf to a call to the specialized version printf_va_5.
+[variadic] tests/known/printf_wrong_types.c:22: Warning:
+ Incorrect type for argument 2. The argument will be cast from long to int.
[variadic] tests/known/printf_wrong_types.c:23:
Translating call to printf to a call to the specialized version printf_va_6.
+[variadic] tests/known/printf_wrong_types.c:23: Warning:
+ Incorrect type for argument 2. The argument will be cast from unsigned int to unsigned long.
[variadic] tests/known/printf_wrong_types.c:24:
Translating call to printf to a call to the specialized version printf_va_7.
+[variadic] tests/known/printf_wrong_types.c:24: Warning:
+ Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
[variadic] tests/known/printf_wrong_types.c:25:
Translating call to printf to a call to the specialized version printf_va_8.
[variadic] tests/known/printf_wrong_types.c:25: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index e8e49846730a17c80917b05866bcf50eea92871e..a55e9b9b9051ebaf7bd0333d33c1eaa6b3cad380 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -84,7 +84,7 @@ int main(void)
int __retres;
char data[100];
size_t tmp_0;
- memset((void *)(data),'A',(unsigned int)99);
+ memset((void *)(data),'A',(unsigned long)99);
data[99] = (char)0;
char dest[50] = {(char)'\000'};
if (nondet) {
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 338a605bafc35c6667d7b4da2917eda828ad264c..505fe9d8346afc035f367aaf1005fad87644e19c 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -97,7 +97,7 @@ int main(void)
int __retres;
wchar_t data[100];
size_t tmp_0;
- wmemset(data,65,(unsigned int)99);
+ wmemset(data,65,(unsigned long)99);
data[99] = 0;
wchar_t dest[50] = {0};
if (nondet) {
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index 631396fece92093dd91c3a852c1af15dec335c3c..b0188cdf1525b78c8f76532497dad499c2bfd2ff 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -263,7 +263,7 @@ int main(void)
"%" "E" "\\n" ,42.0,42.0,42.0); /* wprintf_va_4 */
wprintf((wchar_t const *)L"%" "*" "d" " " "\\n" ,4,2); /* wprintf_va_5 */
wprintf((wchar_t const *)L"%" "l" "s" " " "\\n" ,(wchar_t *)L"4" "2" ); /* wprintf_va_6 */
- swprintf(wstring,(unsigned int)0x100,(wchar_t const *)L"%" "s" " " "=" " "
+ swprintf(wstring,(unsigned long)0x100,(wchar_t const *)L"%" "s" " " "=" " "
"%" "d" ,(char *)L"4" "2" " " "+" " " "4" "2" ,42 + 42); /* swprintf_va_1 */
wscanf((wchar_t const *)L"%" "l" "s" ,wstring); /* wscanf_va_1 */
wscanf((wchar_t const *)L"%" "d" " " "%" "d" ,& i,& j); /* wscanf_va_2 */
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
index d2b0d3de19a44706760e2805d7c14e3c949490cf..b0e1722d9dc81cfbda055c5e99e3d235dad9eda0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
@@ -11,22 +11,22 @@ Prove: true.
------------------------------------------------------------
-Goal Assertion 'a01' (file tests/wp_plugin/overflow2.c, line 20):
+Goal Assertion 'a01' (file tests/wp_plugin/overflow2.c, line 27):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'a02' (file tests/wp_plugin/overflow2.c, line 21):
+Goal Assertion 'a02' (file tests/wp_plugin/overflow2.c, line 28):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'a03' (file tests/wp_plugin/overflow2.c, line 22):
+Goal Assertion 'a03' (file tests/wp_plugin/overflow2.c, line 29):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'a04' (file tests/wp_plugin/overflow2.c, line 23):
+Goal Assertion 'a04' (file tests/wp_plugin/overflow2.c, line 30):
Assume {
Type: is_sint16(distance_0) /\ is_uint32(p1_off_0).
(* Pre-condition *)
@@ -36,7 +36,7 @@ Prove: (p1_off_0 + to_uint16(distance_0)) <= 65545.
------------------------------------------------------------
-Goal Assertion 'a05' (file tests/wp_plugin/overflow2.c, line 24):
+Goal Assertion 'a05' (file tests/wp_plugin/overflow2.c, line 31):
Let x = p1_off_0 + to_uint16(distance_0).
Assume {
Type: is_sint16(distance_0) /\ is_uint32(p1_off_0).
@@ -49,7 +49,7 @@ Prove: x = to_uint32(x).
------------------------------------------------------------
-Goal Assigns (file tests/wp_plugin/overflow2.c, line 14) in 'pointers_and_companions':
+Goal Assigns (file tests/wp_plugin/overflow2.c, line 21) in 'pointers_and_companions':
Prove: true.
------------------------------------------------------------
@@ -62,22 +62,22 @@ Prove: true.
------------------------------------------------------------
-Goal Assertion 'a06' (file tests/wp_plugin/overflow2.c, line 39):
+Goal Assertion 'a06' (file tests/wp_plugin/overflow2.c, line 46):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'a07' (file tests/wp_plugin/overflow2.c, line 40):
+Goal Assertion 'a07' (file tests/wp_plugin/overflow2.c, line 47):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'a08' (file tests/wp_plugin/overflow2.c, line 41):
+Goal Assertion 'a08' (file tests/wp_plugin/overflow2.c, line 48):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'a09' (file tests/wp_plugin/overflow2.c, line 42):
+Goal Assertion 'a09' (file tests/wp_plugin/overflow2.c, line 49):
Assume {
Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
(* Pre-condition *)
@@ -87,7 +87,7 @@ Prove: (p1_off_alt_0 + to_uint16(distance_0)) <= 65545.
------------------------------------------------------------
-Goal Assertion 'a10' (file tests/wp_plugin/overflow2.c, line 43):
+Goal Assertion 'a10' (file tests/wp_plugin/overflow2.c, line 50):
Let x = p1_off_alt_0 + to_uint16(distance_0).
Assume {
Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
@@ -100,7 +100,7 @@ Prove: x = to_uint32(x).
------------------------------------------------------------
-Goal Assigns (file tests/wp_plugin/overflow2.c, line 33) in 'pointers_and_companions_ulong':
+Goal Assigns (file tests/wp_plugin/overflow2.c, line 40) in 'pointers_and_companions_ulong':
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
index aa233aaddc79ff44a7e2d47e4989bc411e4ac984..1774140d9e302ec8df478218bdb65ad6665dd498 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
@@ -7,7 +7,7 @@ Goal Post-condition 'copied_contents' in 'memcpy':
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Assume {
- Type: is_uint32(i) /\ is_uint32(n).
+ Type: is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -37,7 +37,7 @@ Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 3
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Assume {
- Type: is_uint32(i) /\ is_uint32(n).
+ Type: is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -53,13 +53,13 @@ Assume {
(* Then *)
Have: i < n.
}
-Prove: to_uint32(1 + i) <= n.
+Prove: to_uint64(1 + i) <= n.
------------------------------------------------------------
Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
Assume {
- Type: is_uint32(n).
+ Type: is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0).
@@ -77,12 +77,12 @@ Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = a_1[shift_sint8(dest_0, i) <- a_1[shift_sint8(src_0, i)]].
Assume {
- Type: is_uint32(i) /\ is_uint32(n).
+ Type: is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+ When: (0 <= i_1) /\ (i_1 < to_uint64(1 + i)).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n) /\
@@ -121,7 +121,7 @@ Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(dest_0, i).
Assume {
- Type: is_uint32(i) /\ is_uint32(n).
+ Type: is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -153,7 +153,7 @@ Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 3
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Assume {
- Type: is_uint32(i) /\ is_uint32(n).
+ Type: is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -169,7 +169,7 @@ Assume {
(* Then *)
Have: i < n.
}
-Prove: i < to_uint32(1 + i).
+Prove: i < to_uint64(1 + i).
------------------------------------------------------------
@@ -180,8 +180,8 @@ Prove: true.
Goal Post-condition 'copied_contents' in 'memmove':
Assume {
- Type: is_uint32(i) /\ is_uint32(i_1) /\ is_uint32(n) /\
- is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(i_1) /\
+ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -252,7 +252,7 @@ Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -280,7 +280,7 @@ Assume {
(* Then *)
Have: i < n.
}
-Prove: to_uint32(1 + i) <= n.
+Prove: to_uint64(1 + i) <= n.
------------------------------------------------------------
@@ -288,7 +288,7 @@ Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line
Let a = shift_sint8(d, 0).
Let a_1 = shift_sint8(s, 0).
Assume {
- Type: is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
@@ -314,12 +314,12 @@ Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(s, 0).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0) /\
sconst(Mchar_0).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+ When: (0 <= i_1) /\ (i_1 < to_uint64(1 + i)).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
@@ -360,12 +360,12 @@ Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(s, 0).
Let a_3 = shift_sint8(s, i_1).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0) /\
sconst(Mchar_0).
(* Goal *)
- When: (i_1 < n) /\ (to_uint32(1 + i) <= i_1).
+ When: (i_1 < n) /\ (to_uint64(1 + i) <= i_1).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
@@ -404,7 +404,7 @@ Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -432,7 +432,7 @@ Assume {
(* Then *)
Have: 0 < i.
}
-Prove: to_uint32(i - 1) < n.
+Prove: to_uint64(i - 1) < n.
------------------------------------------------------------
@@ -440,7 +440,7 @@ Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line
Let a = shift_sint8(d, 0).
Let a_1 = shift_sint8(s, 0).
Assume {
- Type: is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
@@ -457,7 +457,7 @@ Assume {
(* Else *)
Have: 0 < memoverlap_0.
}
-Prove: to_uint32(n - 1) < n.
+Prove: to_uint64(n - 1) < n.
------------------------------------------------------------
@@ -466,12 +466,12 @@ Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(s, 0).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0) /\
sconst(Mchar_0).
(* Goal *)
- When: (i_1 < n) /\ (to_uint32(i - 1) < i_1).
+ When: (i_1 < n) /\ (to_uint64(i - 1) < i_1).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
@@ -505,12 +505,12 @@ Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line
Let a = shift_sint8(dest_0, 0).
Let a_1 = shift_sint8(src_0, 0).
Assume {
- Type: is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
- When: (i < n) /\ (to_uint32(n - 1) < i).
+ When: (i < n) /\ (to_uint64(n - 1) < i).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
@@ -535,12 +535,12 @@ Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(s, 0).
Let a_3 = shift_sint8(s, i_1).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0) /\
sconst(Mchar_0).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 <= to_uint32(i - 1)).
+ When: (0 <= i_1) /\ (i_1 <= to_uint64(i - 1)).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
@@ -592,7 +592,7 @@ Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
Let a_3 = shift_sint8(d, i).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -644,7 +644,7 @@ Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
Let a_3 = shift_sint8(d, i).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -718,7 +718,7 @@ Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -763,7 +763,7 @@ Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -791,7 +791,7 @@ Assume {
(* Then *)
Have: i < n.
}
-Prove: i < to_uint32(1 + i).
+Prove: i < to_uint64(1 + i).
------------------------------------------------------------
@@ -805,7 +805,7 @@ Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
Assume {
- Type: is_uint32(i) /\ is_uint32(n) /\ is_sint32(memoverlap_0).
+ Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
@@ -833,7 +833,7 @@ Assume {
(* Then *)
Have: 0 < i.
}
-Prove: to_uint32(i - 1) < i.
+Prove: to_uint64(i - 1) < i.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/overflow2.c b/src/plugins/wp/tests/wp_plugin/overflow2.c
index f2a27e3b194a6c9b7d4b28557390cf44a082e05a..da847d4d3562491444bacd4a818ff35c4312eb34 100644
--- a/src/plugins/wp/tests/wp_plugin/overflow2.c
+++ b/src/plugins/wp/tests/wp_plugin/overflow2.c
@@ -1,3 +1,10 @@
+/* run.config
+ OPT: -machdep x86_32
+*/
+/* run.config_qualif
+ OPT: -machdep x86_32
+*/
+
/* run with: frama-c-gui -wp -wp-rte strange_work_again.c */
// uproven: a04, a05, a09, a10
// note that when the type of distance is ushort, all is proven
diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot
index eb1fa949b61292f0492473059be5e7da8c88292c..c6648e78e8fafdbed4725292d27a9c09e54893e1 100644
--- a/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot
+++ b/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot
@@ -15,12 +15,12 @@ digraph "job" {
_003 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ];
{ rank=same; A001; _003; }
_003 -> A001 [ arrowhead="tee" ];
- _004 [ shape="record", label="<_p1> 128..159: D32|<_p2> 160..191: D32" ];
+ _004 [ shape="record", label="<_p1> 256..319: D64|<_p2> 320..383: D64" ];
_004:_p2 -> A003 [ style="dotted" ];
_004:_p1 -> A002 [ style="dotted" ];
A001 -> _004:w [ arrowhead="tee" ];
A002 [ label="D", shape="oval" ];
- _005 [ label="roots:&fb+128", style="filled", color="lightblue",
+ _005 [ label="roots:&fb+256", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A002; _005; }
@@ -29,7 +29,7 @@ digraph "job" {
_006:_p1 -> A004:w [ taillabel="*", labelangle="+30", color="red" ];
A002 -> _006:w [ arrowhead="tee" ];
A003 [ label="D", shape="oval" ];
- _007 [ label="roots:&fb+160", style="filled", color="lightblue",
+ _007 [ label="roots:&fb+320", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A003; _007; }
@@ -38,7 +38,7 @@ digraph "job" {
_008:_p1 -> A005:w [ taillabel="*", labelangle="+30", color="red" ];
A003 -> _008:w [ arrowhead="tee" ];
A004 [ label="", shape="oval" ];
- _009 [ label="roots:&fb+128", style="filled", color="lightblue",
+ _009 [ label="roots:&fb+256", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A004; _009; }
@@ -48,7 +48,7 @@ digraph "job" {
_010:_p1 -> A006 [ style="dotted" ];
A004 -> _010:w [ arrowhead="tee" ];
A005 [ label="", shape="oval" ];
- _011 [ label="roots:&fb+160", style="filled", color="lightblue",
+ _011 [ label="roots:&fb+320", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A005; _011; }
@@ -58,7 +58,7 @@ digraph "job" {
_012:_p1 -> A008 [ style="dotted" ];
A005 -> _012:w [ arrowhead="tee" ];
A006 [ label="RW", shape="oval", fillcolor="green", style="filled" ];
- _013 [ label="roots:&fb+128", style="filled", color="lightblue",
+ _013 [ label="roots:&fb+256", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A006; _013; }
@@ -66,7 +66,7 @@ digraph "job" {
_014 [ shape="record", label="Var float64" ];
A006 -> _014:w [ arrowhead="tee" ];
A007 [ label="RW", shape="oval", fillcolor="green", style="filled" ];
- _015 [ label="roots:&fb+192", style="filled", color="lightblue",
+ _015 [ label="roots:&fb+320", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A007; _015; }
@@ -74,7 +74,7 @@ digraph "job" {
_016 [ shape="record", label="Var sint32" ];
A007 -> _016:w [ arrowhead="tee" ];
A008 [ label="R", shape="oval", fillcolor="green", style="filled" ];
- _017 [ label="roots:&fb+160", style="filled", color="lightblue",
+ _017 [ label="roots:&fb+320", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A008; _017; }
@@ -82,7 +82,7 @@ digraph "job" {
_018 [ shape="record", label="Var float64" ];
A008 -> _018:w [ arrowhead="tee" ];
A009 [ label="R", shape="oval", fillcolor="green", style="filled" ];
- _019 [ label="roots:&fb+224", style="filled", color="lightblue",
+ _019 [ label="roots:&fb+384", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A009; _019; }
diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot
index 4cbd5b27d23593f242fbdb78151766885a29f883..c278bffd20975f825e0e81a8884920114b062563 100644
--- a/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot
+++ b/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot
@@ -45,7 +45,7 @@ digraph "job" {
{ rank=same; A005; _011; }
_011 -> A005 [ arrowhead="tee" ];
_012 [ shape="record",
- label="<_p1> 0..31: D32|<_p2> 32..127: D32[3]|<_p3> 128..223: D32[3]|<_p4> 224..319: D32[3]|<_p5> 320..351: D32"
+ label="<_p1> 0..63: D64|<_p2> 64..255: D64[3]|<_p3> 256..447: D64[3]|<_p4> 448..639: D64[3]|<_p5> 640..703: D64"
];
_012:_p5 -> A010 [ style="dotted" ];
_012:_p4 -> A008 [ style="dotted" ];
@@ -82,7 +82,7 @@ digraph "job" {
_020:_p1 -> A014:w [ taillabel="*", labelangle="+30", color="red" ];
A009 -> _020:w [ arrowhead="tee" ];
A010 [ label="D", shape="oval" ];
- _021 [ label="roots:&fb+320", style="filled", color="lightblue",
+ _021 [ label="roots:&fb+640", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A010; _021; }
@@ -122,7 +122,7 @@ digraph "job" {
_030:_p1 -> A022 [ style="dotted" ];
A014 -> _030:w [ arrowhead="tee" ];
A015 [ label="", shape="oval" ];
- _031 [ label="roots:&fb+320", style="filled", color="lightblue",
+ _031 [ label="roots:&fb+640", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A015; _031; }
@@ -174,7 +174,7 @@ digraph "job" {
_046 [ shape="record", label="Var float64" ];
A022 -> _046:w [ arrowhead="tee" ];
A023 [ label="W", shape="oval", fillcolor="green", style="filled" ];
- _047 [ label="roots:&fb+320", style="filled", color="lightblue",
+ _047 [ label="roots:&fb+640", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A023; _047; }
@@ -182,7 +182,7 @@ digraph "job" {
_048 [ shape="record", label="Var float64" ];
A023 -> _048:w [ arrowhead="tee" ];
A024 [ label="W", shape="oval", fillcolor="green", style="filled" ];
- _049 [ label="roots:&fb+384", style="filled", color="lightblue",
+ _049 [ label="roots:&fb+704", style="filled", color="lightblue",
shape="box"
];
{ rank=same; A024; _049; }
diff --git a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
index 227396b81fc86ba80567eeabd929f294548f09d9..81c5c6cc27c89fb40c7d4fd8e0da2b62242ca279 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
@@ -25,7 +25,7 @@ theory Matrix
predicate IsArray_uint32 (t:int -> int) = forall i:int. is_uint32 (get t i)
- predicate IsArray_sint32 (t:int -> int) = forall i:int. is_sint32 (get t i)
+ predicate IsArray_sint64 (t:int -> int) = forall i:int. is_sint64 (get t i)
predicate EqArray_int (n:int) (t:int -> int) (t1:int -> int) =
forall i:int. 0 <= i -> i < n -> get t1 i = get t i
@@ -54,7 +54,7 @@ theory S1_S
(* use Matrix *)
predicate IsS1_S (s:S1_S) =
- (IsArray_sint32 (F1_S_b s) /\ IsArray_uint32 (F1_S_a s)) /\
+ (IsArray_sint64 (F1_S_b s) /\ IsArray_uint32 (F1_S_a s)) /\
is_sint32 (F1_S_f s)
predicate EqS1_S (s:S1_S) (s1:S1_S) =
@@ -91,16 +91,17 @@ theory Compound
function shiftfield_F1_S_b (p:addr) : addr = shift p 6
- function shift_sint32 (p:addr) (k:int) : addr = shift p k
+ function shift_sint64 (p:addr) (k:int) : addr = shift p k
- function Array_sint32 addr int (addr -> int) : int -> int
+ function Array_sint64 addr int (addr -> int) : int -> int
(* use S1_S *)
- function Load_S1_S (p:addr) (mint:addr -> int) (mint1:addr -> int) : S1_S =
+ function Load_S1_S (p:addr) (mint:addr -> int) (mint1:addr -> int) (mint2:
+ addr -> int) : S1_S =
S1_S1 (get mint1 (shiftfield_F1_S_f p))
(Array_uint32 (shiftfield_F1_S_a p) 5 mint)
- (Array_sint32 (shiftfield_F1_S_b p) 5 mint1)
+ (Array_sint64 (shiftfield_F1_S_b p) 5 mint2)
Q_Array_uint32_access :
forall mint:addr -> int, i:int, n:int, p:addr
@@ -126,67 +127,98 @@ theory Compound
separated p 1 q n1 ->
Array_uint32 p n (havoc mint1 mint q n1) = Array_uint32 p n mint
- Q_Array_sint32_access :
+ Q_Array_sint64_access :
forall mint:addr -> int, i:int, n:int, p:addr
- [get (Array_sint32 p n mint) i].
+ [get (Array_sint64 p n mint) i].
0 <= i ->
- i < n -> get (Array_sint32 p n mint) i = get mint (shift_sint32 p i)
+ i < n -> get (Array_sint64 p n mint) i = get mint (shift_sint64 p i)
- Q_Array_sint32_update_Mint0 :
+ Q_Array_sint64_update_Mint0 :
forall mint:addr -> int, n:int, p:addr, q:addr, v:int
- [Array_sint32 p n (set mint q v)].
- not q = p -> Array_sint32 p n (set mint q v) = Array_sint32 p n mint
+ [Array_sint64 p n (set mint q v)].
+ not q = p -> Array_sint64 p n (set mint q v) = Array_sint64 p n mint
- Q_Array_sint32_eqmem_Mint0 :
+ Q_Array_sint64_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
- [Array_sint32 p n mint, eqmem mint mint1 q n1| Array_sint32 p n mint1,
+ [Array_sint64 p n mint, eqmem mint mint1 q n1| Array_sint64 p n mint1,
eqmem mint mint1 q n1].
included p 1 q n1 ->
- eqmem mint mint1 q n1 -> Array_sint32 p n mint1 = Array_sint32 p n mint
+ eqmem mint mint1 q n1 -> Array_sint64 p n mint1 = Array_sint64 p n mint
- Q_Array_sint32_havoc_Mint0 :
+ Q_Array_sint64_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
- [Array_sint32 p n (havoc mint1 mint q n1)].
+ [Array_sint64 p n (havoc mint1 mint q n1)].
separated p 1 q n1 ->
- Array_sint32 p n (havoc mint1 mint q n1) = Array_sint32 p n mint
+ Array_sint64 p n (havoc mint1 mint q n1) = Array_sint64 p n mint
Q_Load_S1_S_update_Mint0 :
- forall mint:addr -> int, mint1:addr -> int, p:addr, q:addr, v:int
- [Load_S1_S p (set mint q v) mint1].
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
+ addr, v:int [Load_S1_S p (set mint q v) mint1 mint2].
separated p 11 q 1 ->
- Load_S1_S p (set mint q v) mint1 = Load_S1_S p mint mint1
+ Load_S1_S p (set mint q v) mint1 mint2 = Load_S1_S p mint mint1 mint2
Q_Load_S1_S_eqmem_Mint0 :
- forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
- addr, q:addr [Load_S1_S p mint mint2, eqmem mint mint1 q n|
- Load_S1_S p mint1 mint2, eqmem mint mint1 q n].
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
+ -> int, n:int, p:addr, q:addr [Load_S1_S p mint mint2 mint3,
+ eqmem mint mint1 q n| Load_S1_S p mint1 mint2 mint3,
+ eqmem mint mint1 q n].
included p 11 q n ->
- eqmem mint mint1 q n -> Load_S1_S p mint1 mint2 = Load_S1_S p mint mint2
+ eqmem mint mint1 q n ->
+ Load_S1_S p mint1 mint2 mint3 = Load_S1_S p mint mint2 mint3
Q_Load_S1_S_havoc_Mint0 :
- forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
- addr, q:addr [Load_S1_S p (havoc mint1 mint q n) mint2].
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
+ -> int, n:int, p:addr, q:addr
+ [Load_S1_S p (havoc mint1 mint q n) mint2 mint3].
separated p 11 q n ->
- Load_S1_S p (havoc mint1 mint q n) mint2 = Load_S1_S p mint mint2
+ Load_S1_S p (havoc mint1 mint q n) mint2 mint3
+ = Load_S1_S p mint mint2 mint3
Q_Load_S1_S_update_Mint1 :
- forall mint:addr -> int, mint1:addr -> int, p:addr, q:addr, v:int
- [Load_S1_S p mint1 (set mint q v)].
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
+ addr, v:int [Load_S1_S p mint2 (set mint1 q v) mint].
separated p 11 q 1 ->
- Load_S1_S p mint1 (set mint q v) = Load_S1_S p mint1 mint
+ Load_S1_S p mint2 (set mint1 q v) mint = Load_S1_S p mint2 mint1 mint
Q_Load_S1_S_eqmem_Mint1 :
- forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
- addr, q:addr [Load_S1_S p mint2 mint, eqmem mint mint1 q n|
- Load_S1_S p mint2 mint1, eqmem mint mint1 q n].
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
+ -> int, n:int, p:addr, q:addr [Load_S1_S p mint3 mint1 mint,
+ eqmem mint1 mint2 q n| Load_S1_S p mint3 mint2 mint,
+ eqmem mint1 mint2 q n].
included p 11 q n ->
- eqmem mint mint1 q n -> Load_S1_S p mint2 mint1 = Load_S1_S p mint2 mint
+ eqmem mint1 mint2 q n ->
+ Load_S1_S p mint3 mint2 mint = Load_S1_S p mint3 mint1 mint
Q_Load_S1_S_havoc_Mint1 :
- forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
- addr, q:addr [Load_S1_S p mint2 (havoc mint1 mint q n)].
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
+ -> int, n:int, p:addr, q:addr
+ [Load_S1_S p mint3 (havoc mint2 mint1 q n) mint].
separated p 11 q n ->
- Load_S1_S p mint2 (havoc mint1 mint q n) = Load_S1_S p mint2 mint
+ Load_S1_S p mint3 (havoc mint2 mint1 q n) mint
+ = Load_S1_S p mint3 mint1 mint
+
+ Q_Load_S1_S_update_Mint2 :
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
+ addr, v:int [Load_S1_S p mint1 mint (set mint2 q v)].
+ separated p 11 q 1 ->
+ Load_S1_S p mint1 mint (set mint2 q v) = Load_S1_S p mint1 mint mint2
+
+ Q_Load_S1_S_eqmem_Mint2 :
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
+ -> int, n:int, p:addr, q:addr [Load_S1_S p mint1 mint mint2,
+ eqmem mint2 mint3 q n| Load_S1_S p mint1 mint mint3,
+ eqmem mint2 mint3 q n].
+ included p 11 q n ->
+ eqmem mint2 mint3 q n ->
+ Load_S1_S p mint1 mint mint3 = Load_S1_S p mint1 mint mint2
+
+ Q_Load_S1_S_havoc_Mint2 :
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
+ -> int, n:int, p:addr, q:addr
+ [Load_S1_S p mint1 mint (havoc mint3 mint2 q n)].
+ separated p 11 q n ->
+ Load_S1_S p mint1 mint (havoc mint3 mint2 q n)
+ = Load_S1_S p mint1 mint mint2
end
[wp:print-generated]
theory WP
@@ -211,9 +243,9 @@ end
(* use Compound *)
goal wp_goal :
- forall t:addr -> int, t1:addr -> int, a:addr, i:int.
- let a1 = Load_S1_S a t t1 in
- let a2 = Load_S1_S a t (set t1 (shiftfield_F1_S_f a) i) in
+ forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, i:int.
+ let a1 = Load_S1_S a t t2 t1 in
+ let a2 = Load_S1_S a t (set t2 (shiftfield_F1_S_f a) i) t1 in
region (base a) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
end
[wp] 1 goal generated
@@ -222,8 +254,8 @@ end
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/multi_matrix_types.i, line 10) in 'job':
-Let a = Load_S1_S(p, Mint_0, Mint_1).
-Let a_1 = Load_S1_S(p, Mint_0, Mint_1[shiftfield_F1_S_f(p) <- v]).
+Let a = Load_S1_S(p, Mint_0, Mint_1, Mint_2).
+Let a_1 = Load_S1_S(p, Mint_0, Mint_1[shiftfield_F1_S_f(p) <- v], Mint_2).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
index 6bddd899e5d968db9988a8569ae23c1ecafcadfd..80bd40ad07f2f205835223f78db2855a2747d30e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
@@ -175,7 +175,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file tests/wp_typed/unit_bitwise.c, line 170):
-Let x = land(1, a). Assume { Type: is_uint32(a) /\ is_uint32(x). }
+Let x = land(1, a). Assume { Type: is_uint64(a) /\ is_uint64(x). }
Prove: 0 <= x.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/user_string.i b/src/plugins/wp/tests/wp_typed/user_string.i
index ccadee77578d841643733fd8ebae1cc3bee7d6ce..228942a2a3778ab4f79800bcb2cca303f5504707 100644
--- a/src/plugins/wp/tests/wp_typed/user_string.i
+++ b/src/plugins/wp/tests/wp_typed/user_string.i
@@ -22,7 +22,7 @@
assigns \nothing;
ensures \exists integer i; Length_of_str_is(s,i) && \result == i;
@*/
-int strlen(const char *s) {
+long long strlen(const char *s) {
const char *ss = s;
/*@
loop invariant BASE: \base_addr(s) == \base_addr(ss) ;
diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config
+++ b/tests/builtins/test_config
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_apron b/tests/builtins/test_config_apron
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_apron
+++ b/tests/builtins/test_config_apron
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_bitwise b/tests/builtins/test_config_bitwise
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_bitwise
+++ b/tests/builtins/test_config_bitwise
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_equalities b/tests/builtins/test_config_equalities
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_equalities
+++ b/tests/builtins/test_config_equalities
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_gauges b/tests/builtins/test_config_gauges
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_gauges
+++ b/tests/builtins/test_config_gauges
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_octagons b/tests/builtins/test_config_octagons
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_octagons
+++ b/tests/builtins/test_config_octagons
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_symblocs b/tests/builtins/test_config_symblocs
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_symblocs
+++ b/tests/builtins/test_config_symblocs
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/cil/mkBinOp.i b/tests/cil/mkBinOp.i
index 1bab30cf83cef46281180438db232f21b9d1224b..ebf24f803a0115aca137855c9a076f888475e119 100644
--- a/tests/cil/mkBinOp.i
+++ b/tests/cil/mkBinOp.i
@@ -1,6 +1,6 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print -constfold
+OPT: -machdep x86_32 -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print -constfold
*/
int main(void) {
diff --git a/tests/constant_propagation/const_globals.c b/tests/constant_propagation/const_globals.c
index 41d302fc9106813b0a3da4c52b48ffac1de18349..355a01b498734788a754838b8bde297d78ced63c 100644
--- a/tests/constant_propagation/const_globals.c
+++ b/tests/constant_propagation/const_globals.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -constfold -print -journal-disable
+ OPT: -constfold -print -journal-disable -machdep x86_32
*/
#include <stddef.h>
diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config
index 850779adb25d797c03ebc59655d31bec1c50cadf..c9ce20f05d9b350fd5d065e1d08f26e53fc065b6 100644
--- a/tests/constant_propagation/test_config
+++ b/tests/constant_propagation/test_config
@@ -1 +1 @@
-OPT: -journal-disable -scf @EVA_OPTIONS@
+OPT: -journal-disable -scf @EVA_OPTIONS@ -machdep x86_32
diff --git a/tests/fc_script/oracle/make_template.res b/tests/fc_script/oracle/make_template.res
index 9d0864ff3369f45daef50da92ab4eb1211236f0c..95bf74b99516143166cc1e73874e0d1d7555dd30 100644
--- a/tests/fc_script/oracle/make_template.res
+++ b/tests/fc_script/oracle/make_template.res
@@ -10,7 +10,7 @@ warning: result/GNUmakefile already exists. Overwrite? [y/N] Main target name: S
warning: 'main' seems to be defined multiple times.
Is this ok? [Y/n] compile_commands.json exists, add option -json-compilation-database? [Y/n] Add stub for function main (only needed if it uses command-line arguments)? [y/N] Please define the architectural model (machdep) of the target machine.
Known machdeps: x86_16 x86_32 x86_64 gcc_x86_16 gcc_x86_32 gcc_x86_64 ppc_32 msvc_x86_64
-Please enter the machdep [x86_32]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_32]: warning: result/fc_stubs.c already exists. Overwrite? [y/N] Created stub for main function: result/fc_stubs.c
+Please enter the machdep [x86_64]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_64]: warning: result/fc_stubs.c already exists. Overwrite? [y/N] Created stub for main function: result/fc_stubs.c
Template created: result/GNUmakefile
Path to Frama-C binaries written to: result/path.mk
Running ptests: cleaning up after tests...
diff --git a/tests/float/sqrt.c b/tests/float/sqrt.c
index da6743b0866b14d00ea51c2886806bc546008c96..5164d15353f3b7de3e8d88d96e72821f3ef53280 100644
--- a/tests/float/sqrt.c
+++ b/tests/float/sqrt.c
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-eva-slevel 10 -big-ints-hex 257"
- STDOPT: #"-eva-slevel 10 -big-ints-hex 257 -machdep ppc_32"
+ STDOPT: #"-eva-slevel 10 -big-ints-hex 257" +"-machdep ppc_32"
*/
#include <math.h>
@@ -27,5 +27,5 @@ void main() {
for (k=0; k<8; k++)
c[k] = ((unsigned char*)&i)[k];
-
+
}
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 5ad226916ca36cd0496df4992e45e78d79a22da2..096e9927c8d52cb5f445c140e07155ffa3064a6b 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -5,7 +5,7 @@
EXECNOW: make -s @PTEST_DIR@/check_libc_anonymous_tags.cmxs
EXECNOW: make -s @PTEST_DIR@/check_compliance.cmxs
OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
- OPT: -print -print-libc
+ OPT: -print -print-libc -machdep x86_32
OPT: -load-module @PTEST_DIR@/check_parsing_individual_headers
OPT: -load-module @PTEST_DIR@/check_libc_anonymous_tags
OPT: -load-module @PTEST_DIR@/check_compliance -kernel-msg-key printer:attrs
diff --git a/tests/libc/limits_h.c b/tests/libc/limits_h.c
index 8b124df5a62f28a4e70c99720e8db71c00323347..2c663b2c5645c1ac80856c0c08a53b438939debf 100644
--- a/tests/libc/limits_h.c
+++ b/tests/libc/limits_h.c
@@ -1,12 +1,12 @@
/*run.config
- STDOPT: #"-machdep x86_16"
- STDOPT: #"-machdep x86_32"
- STDOPT: #"-machdep x86_64"
- STDOPT: #"-machdep gcc_x86_16"
- STDOPT: #"-machdep gcc_x86_32"
- STDOPT: #"-machdep gcc_x86_64"
- STDOPT: #"-machdep ppc_32"
- STDOPT: #"-machdep msvc_x86_64"
+ STDOPT: +"-machdep x86_16"
+ STDOPT: +"-machdep x86_32"
+ STDOPT: +"-machdep x86_64"
+ STDOPT: +"-machdep gcc_x86_16"
+ STDOPT: +"-machdep gcc_x86_32"
+ STDOPT: +"-machdep gcc_x86_64"
+ STDOPT: +"-machdep ppc_32"
+ STDOPT: +"-machdep msvc_x86_64"
*/
#include <sys/types.h>
#include <stdint.h>
diff --git a/tests/libc/more_gcc_builtins.c b/tests/libc/more_gcc_builtins.c
index d3d023ac786338c8701dd77e2a3baaefbc959b03..614aae666d6e492da1fd8807c239cfe0b305cff8 100644
--- a/tests/libc/more_gcc_builtins.c
+++ b/tests/libc/more_gcc_builtins.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-machdep gcc_x86_32"
+ STDOPT: +"-machdep gcc_x86_32"
*/
volatile int v;
diff --git a/tests/libc/stdlib_h.c b/tests/libc/stdlib_h.c
index ea1b69046d2c3e6452c948df14cccd81439d8ac2..39d9378e90ec0d16f5fdf8ec1b207681e922517c 100644
--- a/tests/libc/stdlib_h.c
+++ b/tests/libc/stdlib_h.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-machdep msvc_x86_64"
+ STDOPT: +"-machdep msvc_x86_64"
*/
// Note: machdep MSVC is used to avoid warnings due to
// "non implemented long double" when testing strtold.
diff --git a/tests/misc/oracle/print_machdep.res.oracle b/tests/misc/oracle/print_machdep.res.oracle
index 4902716c8fc08e7971dd7cee455314ab41f65599..e0ef03b220dadd48a509cd8d00a25151499d3f9b 100644
--- a/tests/misc/oracle/print_machdep.res.oracle
+++ b/tests/misc/oracle/print_machdep.res.oracle
@@ -1,17 +1,17 @@
-Machine: gcc 4.0.3 - X86-32bits mode
+Machine: gcc 4.0.3 AMD64
sizeof short = 2 (16 bits, aligned on 16 bits)
sizeof int = 4 (32 bits, aligned on 32 bits)
- sizeof long = 4 (32 bits, aligned on 32 bits)
- sizeof long long = 8 (64 bits, aligned on 32 bits)
+ sizeof long = 8 (64 bits, aligned on 64 bits)
+ sizeof long long = 8 (64 bits, aligned on 64 bits)
sizeof float = 4 (32 bits, aligned on 32 bits)
- sizeof double = 8 (64 bits, aligned on 32 bits)
- sizeof long double = 12 (96 bits, aligned on 32 bits)
- sizeof pointer = 4 (32 bits, aligned on 32 bits)
+ sizeof double = 8 (64 bits, aligned on 64 bits)
+ sizeof long double = 16 (128 bits, aligned on 128 bits)
+ sizeof pointer = 8 (64 bits, aligned on 64 bits)
sizeof void = 1 (8 bits, aligned on 8 bits)
sizeof function = error (alignof error)
- typeof sizeof(T) = unsigned int
+ typeof sizeof(T) = unsigned long
typeof wchar_t = int
- typeof ptrdiff_t = int
+ typeof ptrdiff_t = long
char is signed
machine is little endian
strings are const chars
diff --git a/tests/misc/pragma-pack.c b/tests/misc/pragma-pack.c
index 6b0b00ff1cb21e7124a3dc03999945a5ef9fbe4d..b2e44f3f65464fb533c965f48beb09ce1d9be20a 100644
--- a/tests/misc/pragma-pack.c
+++ b/tests/misc/pragma-pack.c
@@ -1,7 +1,7 @@
/*run.config
- STDOPT: #"-machdep gcc_x86_64 -kernel-msg-key typing:pragma"
- STDOPT: #"-machdep gcc_x86_32"
- STDOPT: #"-machdep msvc_x86_64"
+ STDOPT: +"-machdep gcc_x86_64 -kernel-msg-key typing:pragma"
+ STDOPT: +"-machdep gcc_x86_32"
+ STDOPT: +"-machdep msvc_x86_64"
*/
#include "pragma-pack-utils.h"
diff --git a/tests/misc/pragma_pack_zero.c b/tests/misc/pragma_pack_zero.c
index 6a89215bebbdb079321c448fe2c89a718a30a57b..22f956bd3c37c453f011aee30726b8f443dfd79e 100644
--- a/tests/misc/pragma_pack_zero.c
+++ b/tests/misc/pragma_pack_zero.c
@@ -1,6 +1,6 @@
/* run.config
- STDOPT: #"-machdep gcc_x86_64"
- STDOPT: #"-machdep msvc_x86_64"
+ STDOPT: +"-machdep gcc_x86_64"
+ STDOPT: +"-machdep msvc_x86_64"
*/
// #pragma pack(0) is not supported by MSVC, but allowed in GCC.
// In MSVC mode, we ignore it.
diff --git a/tests/rte/array_index.c b/tests/rte/array_index.c
index b976e42cce80e05920e1870208d858e4db473a18..77df7919a2332a91172e6cb5790e609d1ff02aad 100644
--- a/tests/rte/array_index.c
+++ b/tests/rte/array_index.c
@@ -1,6 +1,6 @@
/* run.config
- OPT: -rte -warn-signed-overflow -print -then -rte-trivial-annotations
- OPT: -rte -warn-signed-overflow -print -unsafe-arrays
+ OPT: -machdep x86_32 -rte -warn-signed-overflow -print -then -rte-trivial-annotations
+ OPT: -machdep x86_32 -rte -warn-signed-overflow -print -unsafe-arrays
*/
int t[10];
diff --git a/tests/rte/castoncall.c b/tests/rte/castoncall.c
index 35340269152d9036a0425ae03148ce991143e4ad..65401d7a0354fe74e0e8ff61326915dd4e4a5856 100644
--- a/tests/rte/castoncall.c
+++ b/tests/rte/castoncall.c
@@ -1,15 +1,15 @@
/* run.config
- OPT: -rte -warn-signed-overflow -warn-signed-downcast -print
- OPT: -rte -warn-signed-overflow -warn-signed-downcast -no-collapse-call-cast -print
+ OPT: -machdep x86_32 -rte -warn-signed-overflow -warn-signed-downcast -print
+ OPT: -machdep x86_32 -rte -warn-signed-overflow -warn-signed-downcast -no-collapse-call-cast -print
*/
-/*@
+/*@
ensures (\result == a) || (\result == b);
assigns \result \from a,b;
*/
int nondet(int a, int b);
-/*@
+/*@
ensures (\result == a) || (\result == b);
assigns \result \from a,b;
*/
diff --git a/tests/rte/u64.i b/tests/rte/u64.i
index 173468db18f77ba40b8145d10e9aeef6d7b1277b..8f23354dfb741c264df216e93520a3d94097ec5d 100644
--- a/tests/rte/u64.i
+++ b/tests/rte/u64.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -rte -warn-unsigned-overflow -print -journal-disable
+ OPT: -rte -warn-unsigned-overflow -print -journal-disable -machdep x86_32
OPT: -rte -warn-unsigned-overflow -print -journal-disable -machdep x86_64
*/
unsigned long f(unsigned int n)
diff --git a/tests/rte_manual/machdep.i b/tests/rte_manual/machdep.i
index 31828d04e860c5b079963c8f4123ee1a5c1b6c53..65edbbb4caa30e2af31b9c85d4d01e6a68804a54 100644
--- a/tests/rte_manual/machdep.i
+++ b/tests/rte_manual/machdep.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -rte -then -print
+ OPT: -machdep x86_32 -rte -then -print
OPT: -machdep x86_64 -rte -then -print
*/
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index 5f757c7f0cf39a6306df9054d570f2ef8bb52c8f..8b313889c4bb740461194736e696f5ec1b0807cf 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -1,5 +1,5 @@
/* run.config
- EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/bool.sav -eva @EVA_OPTIONS@ ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
+ EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
STDOPT: +"-load ./tests/saveload/result/bool.sav -out -input -deps"
STDOPT: +"-load ./tests/saveload/result/bool.sav -eva @EVA_OPTIONS@"
*/
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index 94edfab69b08faf9a5480298c9c557bcd43226c0..a709a3c91d35fd4abeee2660f7e99d245df4287e 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1,2 +1,2 @@
EXECNOW: make -s tests/slicing/libSelect.cmxs tests/slicing/libAnim.cmxs
-OPT: @EVA_OPTIONS@
+OPT: @EVA_OPTIONS@ -machdep x86_32
diff --git a/tests/spec/test_config b/tests/spec/test_config
index 55c0f5b0128562d71d83efd28ff2c3d025a3fc25..6f16db895cb99190e93d744819de7c21e7358ebe 100644
--- a/tests/spec/test_config
+++ b/tests/spec/test_config
@@ -2,4 +2,4 @@ COMMENT: for now, this directory mainly tests the annotations syntax,
COMMENT: no analysis is performed.
COMMENT: we continue on annotation errors, as this allows to put
COMMENT: various variations of the same test in one file.
-OPT: -pp-annot -print -journal-disable -kernel-warn-key=annot-error=active -check
+OPT: -pp-annot -print -journal-disable -kernel-warn-key=annot-error=active -check -machdep x86_32
diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c
index 7fc8bf5cf27e3745c21e73aa17ae1eb474b729a6..b508b543b6b25745f437b481935ab3e1add8fa02 100644
--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
@@ -1,8 +1,8 @@
/* run.config*
FILTER: sed "s:/[^ ]*/cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::; s: -m32::"
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
- OPT: -no-autoload-plugins -print-cpp-commands
+ OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
+ OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
+ OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
+ OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
+ OPT: -machdep x86_32 -no-autoload-plugins -print-cpp-commands
*/
diff --git a/tests/syntax/enum_repr.i b/tests/syntax/enum_repr.i
index 455e1c4aad4a1d5b923538016a82773032a30a24..8cf7d3d4b1fca5a3becbcb2dd97297ce76f22f92 100644
--- a/tests/syntax/enum_repr.i
+++ b/tests/syntax/enum_repr.i
@@ -1,11 +1,11 @@
/* run.config
EXECNOW: make -s tests/syntax/Enum_repr.cmxs
-OPT: -load-module tests/syntax/Enum_repr.cmxs -enums int -print
-OPT: -load-module tests/syntax/Enum_repr.cmxs -enums gcc-short-enums -print
-OPT: -load-module tests/syntax/Enum_repr.cmxs -enums gcc-enums -print
+OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums int -print
+OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums gcc-short-enums -print
+OPT: -machdep x86_32 -load-module tests/syntax/Enum_repr.cmxs -enums gcc-enums -print
*/
-// is represented by | int | gcc-enums | gcc-short-enums
+// is represented by | int | gcc-enums | gcc-short-enums
// foo | int | unsigned int | unsigned char
// bar | int | unsigned char | unsigned char
// bu1 | int | unsigned int | unsigned int
diff --git a/tests/syntax/gnu-asm-aesni.c b/tests/syntax/gnu-asm-aesni.c
index 57f21d3dc98c7b9c984f0e4f43bd4eba384026c1..1e2b0f7f4526aa2e71a85d9f31114959b086f0dc 100644
--- a/tests/syntax/gnu-asm-aesni.c
+++ b/tests/syntax/gnu-asm-aesni.c
@@ -7,7 +7,7 @@
COMMENT: TEST_TITLE: Chiffrement via AES-NI
COMMENT: TEST_MAIN: encrypt_aesni
COMMENT: TEST_DESCRIPTION: Un message de 64 octets est initialisé à une valeur précise. Le nombre de tours est fixé à 12 et la clé de chiffrement étendue est initialisée à une valeur abstraite. L'appel à la fonction do_aesni_enc effectue le chiffrement et place le résultat à l'adresse mémoire pointée par le paramètre b. On vérifie ensuite que les cases du tableau b ont bien été initialisées et que le tableau a n'a pas été modifié.
- OPT: -cpp-extra-args='-DUSE_AESNI' -print
+ OPT: -machdep x86_32 -cpp-extra-args='-DUSE_AESNI' -print
-------------------------
*/
#ifdef __FRAMAC__
diff --git a/tests/syntax/no-print-libc-reparse.c b/tests/syntax/no-print-libc-reparse.c
index bf0b39507c3aa985e8c30eef3ab7c52166399f8a..b7dea45f9df034e9d1d84b0063324b19c1364cff 100644
--- a/tests/syntax/no-print-libc-reparse.c
+++ b/tests/syntax/no-print-libc-reparse.c
@@ -1,5 +1,5 @@
/*run.config
- STDOPT: #"-no-print-libc -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.c"
+ STDOPT: +"-no-print-libc -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.c"
*/
// tests that using -no-print-libc on a file with an enum produces output that
diff --git a/tests/syntax/offset.c b/tests/syntax/offset.c
index 271b4450362ee830e85f0c9cb93d6903e21066e8..39b1c35f8c49f9e2b5b7409e72c756873e646e5d 100644
--- a/tests/syntax/offset.c
+++ b/tests/syntax/offset.c
@@ -1,5 +1,5 @@
/* run.config
-OPT: -cpp-extra-args="-Ishare/libc" -print
+OPT: -machdep x86_32 -cpp-extra-args="-Ishare/libc" -print
*/
#include "__fc_define_off_t.h"
diff --git a/tests/syntax/test_config b/tests/syntax/test_config
index a513714e6d0bb6d4a08951df5e1ae4c3ec1b7e55..df749c62084f1dff34265d08aa76546e4a89949e 100644
--- a/tests/syntax/test_config
+++ b/tests/syntax/test_config
@@ -1,4 +1,4 @@
COMMENT: this directory is meant to test exclusively the front-end
COMMENT: (parser, type-checker, linker, syntactic transformations)
-OPT: -print -journal-disable -check
+OPT: -print -journal-disable -check -machdep x86_32
FILEREG:.*\.\(c\|i\|ci\)$
diff --git a/tests/test_config b/tests/test_config
index 3349a7b04de557ca065dddc3267824bed2662dbb..11d75bf850c7c2f65ff98bf5fd486ec47200f499 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_apron b/tests/test_config_apron
index 9756305b89f7a2b23fb4e4ac2f85278695cfa612..568bc84e0ab1763640485b94c48d108a868c76b1 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains apron-octagon -eva-warn-key experimental=inactive
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise
index 2de393bf539f8cf6a0e4b402b7693073f9b5fcc8..9a4d5dfea1a205e217149f186c5341ca046a5189 100644
--- a/tests/test_config_bitwise
+++ b/tests/test_config_bitwise
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_equalities b/tests/test_config_equalities
index 2758bbcdc4c9947e736388b45e175af3ab527c0f..45664b6c91351aae50544f999ad2d98142ee818e 100644
--- a/tests/test_config_equalities
+++ b/tests/test_config_equalities
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index 9c8f47712455d77cef4f1985cbbb45e57cb572a4..ee46c34eb9c1a5f4dfb63334ee41a14f19fcfb40 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_octagons b/tests/test_config_octagons
index 27c9bcc81711c7516b7669081b30ee458cf29077..689c4edbfbb0fe5a6259aa03d4971a16a5b6387c 100644
--- a/tests/test_config_octagons
+++ b/tests/test_config_octagons
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-domains octagon
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index c90d71b9e632ed8b8933b8ca2316b533858a0d27..b4a58bcd9f85e32c18b992356b7ad4fb1e21dafd 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/const_typedef.i b/tests/value/const_typedef.i
index d9f7f3677ca57b9fe40bdc4bfe5b83857a99bc2b..a2a0a3544f0c7304e5a2073be6bde7d35663e549 100644
--- a/tests/value/const_typedef.i
+++ b/tests/value/const_typedef.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
+ OPT: -machdep x86_32 -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
*/
typedef int INT[3][3];
diff --git a/tests/value/diff_apron b/tests/value/diff_apron
index b8f9fbe7d8c8bbc8d910d97e3d71e2b1413b6746..2baa50c4f0082a47ce6e55782d3ac0b56dbd05f1 100644
--- a/tests/value/diff_apron
+++ b/tests/value/diff_apron
@@ -1074,7 +1074,7 @@ diff tests/value/oracle/loopinv.res.oracle tests/value/oracle_apron/loopinv.res.
> 3 To be validated
> 12 Total
diff tests/value/oracle/memexec.res.oracle tests/value/oracle_apron/memexec.res.oracle
-27,32c27,50
+29,34c29,52
< [eva] tests/value/memexec.c:13: Reusing old results for call to f11
< [eva] tests/value/memexec.c:14: Reusing old results for call to f11
< [eva] tests/value/memexec.c:16: Reusing old results for call to f11
@@ -1106,21 +1106,21 @@ diff tests/value/oracle/memexec.res.oracle tests/value/oracle_apron/memexec.res.
> Called from tests/value/memexec.c:21.
> [eva] Recording results for f11
> [eva] Done for function f11
-106c124,127
+108c126,129
< [eva] tests/value/memexec.c:113: Reusing old results for call to f5_aux
---
> [eva] computing for function f5_aux <- f5 <- main.
> Called from tests/value/memexec.c:113.
> [eva] Recording results for f5_aux
> [eva] Done for function f5_aux
-129c150,153
+131c152,155
< [eva] tests/value/memexec.c:137: Reusing old results for call to f7_1
---
> [eva] computing for function f7_1 <- f7 <- main.
> Called from tests/value/memexec.c:137.
> [eva] Recording results for f7_1
> [eva] Done for function f7_1
-144c168,171
+146c170,173
< [eva] tests/value/memexec.c:150: Reusing old results for call to f8_1
---
> [eva] computing for function f8_1 <- f8 <- main.
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index f6010fb62ca6b8e732c4cdfb986167352b43e100..4459f5ccfc6425a1b87171f42525c3e3306dc715 100644
--- a/tests/value/diff_gauges
+++ b/tests/value/diff_gauges
@@ -764,7 +764,7 @@ diff tests/value/oracle/loopfun.1.res.oracle tests/value/oracle_gauges/loopfun.1
13a18
> [eva] tests/value/loopfun.i:27: starting to merge loop iterations
diff tests/value/oracle/memexec.res.oracle tests/value/oracle_gauges/memexec.res.oracle
-101a102
+103a104
> [eva] tests/value/memexec.c:98: starting to merge loop iterations
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.oracle
40a41,123
diff --git a/tests/value/div.i b/tests/value/div.i
index 3ac38b6068dae4271ea190752b7b1efcac5fe878..04ff9505aa3095d18d08dc320a2ae1b7ec1966b0 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-load-module scope -eva-remove-redundant-alarms"
- OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @EVA_CONFIG@
+ OPT: -machdep x86_32 -no-autoload-plugins -load-module eva,inout -rte -then -eva @EVA_CONFIG@
*/
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
int a,b,d1,d2,d0,e;
diff --git a/tests/value/empty_base.c b/tests/value/empty_base.c
index 72501efab3452a7994dd50e645c45334d0ff90f2..1a5baf64c3b8456b030aee0bebc15c0b9cf9ca9f 100644
--- a/tests/value/empty_base.c
+++ b/tests/value/empty_base.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-machdep gcc_x86_32"
+ STDOPT: +"-machdep gcc_x86_32"
STDOPT:
*/
// the tests above must be done separately because both fail:
diff --git a/tests/value/memexec.c b/tests/value/memexec.c
index 36b1a450f3bf5c18f1fd93e513a762d7d41802e8..1023354a4332f15a43204c40d955c226bf5699be 100644
--- a/tests/value/memexec.c
+++ b/tests/value/memexec.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #" -no-eva -rte-select fbug -rte -then -eva"
+ STDOPT: +"-rte-select fbug -rte -then -eva"
*/
int x1, y1, z1, z2; volatile int c, nondet;
diff --git a/tests/value/precond2.c b/tests/value/precond2.c
index be7006c890e03461fa2cc4e79f8cf0d8096d4125..20b7ad01306ebe270fdfe52d1426116f9958c8a8 100644
--- a/tests/value/precond2.c
+++ b/tests/value/precond2.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @EVA_CONFIG@ -then -report -report-print-properties
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @EVA_CONFIG@ -then -rte -then -report -report-print-properties
+ OPT: -machdep x86_32 -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @EVA_CONFIG@ -then -report -report-print-properties
+ OPT: -machdep x86_32 -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @EVA_CONFIG@ -then -rte -then -report -report-print-properties
*/
// Fuse with precond.c when bts #1208 is solved