From 2d43ad6087b7366015cd7e19016fda29e86397ad Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 31 Aug 2017 11:24:59 +0200
Subject: [PATCH] Fix typing issues in several tests and oracles
---
src/plugins/wp/tests/wp_bts/bts_1382.i | 2 +-
.../oracle/reference_array.res.oracle | 70 ++++++++-----------
.../oracle/reference_array_simple.res.oracle | 2 +-
.../oracle_qualif/reference_array.res.oracle | 8 +--
.../wp/tests/wp_hoare/reference_array.i | 6 +-
.../tests/wp_hoare/reference_array_simple.i | 2 +-
tests/metrics/variadic-stdlib-generated.c | 2 +-
tests/misc/oracle/wstring_phase6.res.oracle | 31 ++++----
.../{wstring_phase6.i => wstring_phase6.c} | 3 +-
tests/non-free/imprecise-malloc-free.i | 2 +-
tests/non-free/long_init.c | 2 +-
tests/non-free/long_init2.c | 2 +-
tests/non-free/long_init3.c | 2 +-
tests/non-free/memcpy.c | 2 +-
tests/non-free/memset.i | 4 +-
tests/non-free/strchr.c | 32 ++++-----
tests/non-free/strlen.c | 12 ++--
tests/non-free/strnlen2.c | 28 ++++----
tests/non-free/wcslen.c | 12 ++--
tests/slicing/unravel-variance.i | 2 +-
tests/spec/if.c | 2 +-
tests/spec/second.c | 2 +-
tests/syntax/gnu-asm-aesni.c | 2 +-
tests/syntax/sizeof_bts1414.i | 2 +-
tests/value/alias.i | 8 +--
tests/value/array_ptr.i | 2 +-
tests/value/assigns.i | 6 +-
tests/value/behaviors1.i | 8 +--
tests/value/call.i | 2 +-
tests/value/const.i | 6 +-
tests/value/context_free.i | 2 +-
tests/value/gauges.i | 2 +-
tests/value/initialized.c | 6 +-
tests/value/leaf2.i | 2 +-
tests/value/oracle/gauges.res.oracle | 2 +-
tests/value/reduce_formals.i | 2 +-
tests/value/strings_cond.i | 2 +-
37 files changed, 139 insertions(+), 145 deletions(-)
rename tests/misc/{wstring_phase6.i => wstring_phase6.c} (87%)
diff --git a/src/plugins/wp/tests/wp_bts/bts_1382.i b/src/plugins/wp/tests/wp_bts/bts_1382.i
index b7c631213a7..3db2033624a 100644
--- a/src/plugins/wp/tests/wp_bts/bts_1382.i
+++ b/src/plugins/wp/tests/wp_bts/bts_1382.i
@@ -14,7 +14,7 @@ void loop (void) {
i=0 ;
//@ loop assigns i, dest;
while (i<100) {
- f(&dest);
+ f((unsigned char*)&dest);
copy(&dest, &src, sizeof(dest));
i++;
}
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
index 19ec39d6f47..85e444ea122 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
@@ -219,77 +219,71 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition 'Pload' in 'calls_on_array_dim_2_to_1':
-Let a = shift_A5_sint32(global(G_tt_64), 0).
-Let a_1 = shift_sint32(a, 0).
+Let m = tt_1[0].
+Let m_1 = tt_0[0].
Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 4).
- (* Heap *)
- Have: linked(Malloc_0).
(* Call 'load_5' *)
- Have: valid_rw(Malloc_0, a_1, 5) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (Mint_0[shift_sint32(a, i_1)] = reg_load_0[i_1])))).
- (* Call 'reset_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (Mint_1[shift_sint32(a, i_1)] = 0))).
+ (m_1[i_1] = reg_load_0[i_1]))).
+ (* Call 'reset_5' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
(* Call Effects *)
- Have: havoc(Mint_0, Mint_1, a_1, 5).
+ Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1]))) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
+ (((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
(* Call 'add_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (reg_add_0[i_1] = (reg_load_0[i_1] + Mint_1[shift_sint32(a, i_1)])))).
+ (reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
}
-Prove: Mint_0[shift_sint32(a, i)] = reg_load_0[i].
+Prove: m_1[i] = reg_load_0[i].
------------------------------------------------------------
Goal Post-condition 'Preset' in 'calls_on_array_dim_2_to_1':
-Let a = shift_A5_sint32(global(G_tt_64), 0).
-Let a_1 = shift_sint32(a, 0).
+Let m = tt_0[0].
+Let m_1 = tt_1[0].
Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 4).
- (* Heap *)
- Have: linked(Malloc_0).
(* Call 'load_5' *)
- Have: valid_rw(Malloc_0, a_1, 5) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (Mint_1[shift_sint32(a, i_1)] = reg_load_0[i_1])))).
- (* Call 'reset_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (Mint_0[shift_sint32(a, i_1)] = 0))).
+ (m_1[i_1] = reg_load_0[i_1]))).
+ (* Call 'reset_5' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
(* Call Effects *)
- Have: havoc(Mint_1, Mint_0, a_1, 5).
+ Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_1[i_1] = tt_0[i_1]))) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
+ (((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
(* Call 'add_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (reg_add_0[i_1] = (reg_load_0[i_1] + Mint_0[shift_sint32(a, i_1)])))).
+ (reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
}
-Prove: Mint_0[shift_sint32(a, i)] = 0.
+Prove: m[i] = 0.
------------------------------------------------------------
Goal Post-condition 'Padd' in 'calls_on_array_dim_2_to_1':
-Let a = shift_A5_sint32(global(G_tt_64), 0).
-Let a_1 = shift_sint32(a, 0).
+Let m = tt_1[0].
+Let m_1 = tt_0[0].
Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 4).
- (* Heap *)
- Have: linked(Malloc_0).
(* Call 'load_5' *)
- Have: valid_rw(Malloc_0, a_1, 5) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (Mint_0[shift_sint32(a, i_1)] = reg_load_0[i_1])))).
- (* Call 'reset_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (Mint_1[shift_sint32(a, i_1)] = 0))).
+ (m_1[i_1] = reg_load_0[i_1]))).
+ (* Call 'reset_5' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
(* Call Effects *)
- Have: havoc(Mint_0, Mint_1, a_1, 5).
+ Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1]))) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
+ (((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
(* Call 'add_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
- (reg_add_0[i_1] = (reg_load_0[i_1] + Mint_1[shift_sint32(a, i_1)])))).
+ (reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
}
-Prove: Mint_0[shift_sint32(a, i)] = reg_add_0[i].
+Prove: m_1[i] = reg_add_0[i].
------------------------------------------------------------
@@ -305,9 +299,7 @@ Prove: true.
Goal Instance of 'Pre-condition (file tests/wp_hoare/reference_array.i, line 19) in 'load_5'' in 'calls_on_array_dim_2_to_1' at call 'load_5' (file tests/wp_hoare/reference_array.i, line 83)
:
-Assume { (* Heap *) Have: linked(Malloc_0). }
-Prove: valid_rw(Malloc_0,
- shift_sint32(shift_A5_sint32(global(G_tt_64), 0), 0), 5).
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
index 2af732936d0..b7a5144c966 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
@@ -12,7 +12,7 @@
i
............
... Function call_f1
- &tt
+ tt
tmp
............
... Function f2
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
index 14e02d7bd20..fdae55d041f 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
@@ -29,7 +29,7 @@
[wp] [Alt-Ergo] Goal typed_ref_calls_on_array_dim_2_to_1_post_Padd : Valid
[wp] [Qed] Goal typed_ref_calls_on_array_dim_2_to_1_assign_exit : Valid
[wp] [Qed] Goal typed_ref_calls_on_array_dim_2_to_1_assign_normal : Valid
-[wp] [Alt-Ergo] Goal typed_ref_calls_on_array_dim_2_to_1_call_load_5_pre : Valid
+[wp] [Qed] Goal typed_ref_calls_on_array_dim_2_to_1_call_load_5_pre : Valid
[wp] [Qed] Goal typed_ref_calls_on_array_dim_2_to_1_call_reset_5_pre : Valid
[wp] [Qed] Goal typed_ref_calls_on_array_dim_2_to_1_call_add_5_pre : Valid
[wp] [Alt-Ergo] Goal typed_ref_load_1_5_post : Valid
@@ -41,14 +41,14 @@
[wp] [Qed] Goal typed_ref_reset_1_5_assign_normal : Valid
[wp] [Qed] Goal typed_ref_reset_1_5_call_reset_5_pre : Valid
[wp] Proved goals: 36 / 36
- Qed: 23
- Alt-Ergo: 13
+ Qed: 24
+ Alt-Ergo: 12
----------------------------------------------------------
Functions WP Alt-Ergo Total Success
reset_1_5 3 1 (18) 4 100%
load_1_5 3 1 (16) 4 100%
add_1_5 3 1 (16) 4 100%
calls_on_array_dim_1 5 3 (14) 8 100%
-calls_on_array_dim_2_to_1 4 4 (44) 8 100%
+calls_on_array_dim_2_to_1 5 3 (16) 8 100%
calls_on_array_dim_2 5 3 (13) 8 100%
----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_hoare/reference_array.i b/src/plugins/wp/tests/wp_hoare/reference_array.i
index 10b95518f06..f10fb46b32c 100644
--- a/src/plugins/wp/tests/wp_hoare/reference_array.i
+++ b/src/plugins/wp/tests/wp_hoare/reference_array.i
@@ -80,9 +80,9 @@ void calls_on_array_dim_1 (void)
*/
void calls_on_array_dim_2_to_1 (void)
{
- load_5(&(tt[0]));
- reset_5(&(tt[0]));
- add_5(&(tt[0]));
+ load_5(tt[0]);
+ reset_5(tt[0]);
+ add_5(tt[0]);
}
diff --git a/src/plugins/wp/tests/wp_hoare/reference_array_simple.i b/src/plugins/wp/tests/wp_hoare/reference_array_simple.i
index 6b80daee6a5..958c2825cba 100644
--- a/src/plugins/wp/tests/wp_hoare/reference_array_simple.i
+++ b/src/plugins/wp/tests/wp_hoare/reference_array_simple.i
@@ -15,7 +15,7 @@ int f1 (int * p1,int i) ;
int call_f1(void)
{
tt[0][3] = 5;
- return f1(tt,3);
+ return f1(tt[0],3);
}
diff --git a/tests/metrics/variadic-stdlib-generated.c b/tests/metrics/variadic-stdlib-generated.c
index 5dbb4919140..c4f61f11834 100644
--- a/tests/metrics/variadic-stdlib-generated.c
+++ b/tests/metrics/variadic-stdlib-generated.c
@@ -8,7 +8,7 @@
// not be reported as part of the stdlib.
int rand(void);
-void my_printf(char *s) {}
+void my_printf(char const *s) {}
void printf2(char *s);
diff --git a/tests/misc/oracle/wstring_phase6.res.oracle b/tests/misc/oracle/wstring_phase6.res.oracle
index 908098b8708..c6f623ed780 100644
--- a/tests/misc/oracle/wstring_phase6.res.oracle
+++ b/tests/misc/oracle/wstring_phase6.res.oracle
@@ -1,30 +1,31 @@
-[kernel] Parsing tests/misc/wstring_phase6.i (no preprocessing)
-tests/misc/wstring_phase6.i:8:[kernel] warning: Calling undeclared function printf. Old style K&R code?
-[kernel] Constant "%s\n" location: Start line 8, char 8; End line 8, char 14
-[kernel] Constant "123456" location: Start line 8, char 16; End line 8, char 27
-[kernel] Constant "%ls\n" location: Start line 9, char 8; End line 9, char 15
-[kernel] Constant L"1" "2" "3" "4" "5" "6"
- location: Start line 9, char 17; End line 9, char 30
+[kernel] Parsing tests/misc/wstring_phase6.c (with preprocessing)
+[kernel] Constant "%s\n" location: Start line 9, char 8; End line 9, char 14
+[kernel] Constant "123456" location: Start line 9, char 16; End line 9, char 27
[kernel] Constant "%ls\n" location: Start line 10, char 8; End line 10, char 15
[kernel] Constant L"1" "2" "3" "4" "5" "6"
- location: Start line 10, char 17; End line 10, char 29
+ location: Start line 10, char 17; End line 10, char 30
[kernel] Constant "%ls\n" location: Start line 11, char 8; End line 11, char 15
[kernel] Constant L"1" "2" "3" "4" "5" "6"
location: Start line 11, char 17; End line 11, char 29
[kernel] Constant "%ls\n" location: Start line 12, char 8; End line 12, char 15
[kernel] Constant L"1" "2" "3" "4" "5" "6"
- location: Start line 12, char 17; End line 12, char 30
+ location: Start line 12, char 17; End line 12, char 29
+[kernel] Constant "%ls\n" location: Start line 13, char 8; End line 13, char 15
+[kernel] Constant L"1" "2" "3" "4" "5" "6"
+ location: Start line 13, char 17; End line 13, char 30
/* Generated by Frama-C */
-extern int ( /* missing proto */ printf)(char const *x_0, char const *x_1);
-
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
int main(void)
{
int __retres;
printf("%s\n","123456");
- printf("%ls\n",(char const *)L"1" "2" "3" "4" "5" "6" );
- printf("%ls\n",(char const *)L"1" "2" "3" "4" "5" "6" );
- printf("%ls\n",(char const *)L"1" "2" "3" "4" "5" "6" );
- printf("%ls\n",(char const *)L"1" "2" "3" "4" "5" "6" );
+ printf("%ls\n",L"1" "2" "3" "4" "5" "6" );
+ printf("%ls\n",L"1" "2" "3" "4" "5" "6" );
+ printf("%ls\n",L"1" "2" "3" "4" "5" "6" );
+ printf("%ls\n",L"1" "2" "3" "4" "5" "6" );
__retres = 0;
return __retres;
}
diff --git a/tests/misc/wstring_phase6.i b/tests/misc/wstring_phase6.c
similarity index 87%
rename from tests/misc/wstring_phase6.i
rename to tests/misc/wstring_phase6.c
index f1310628130..138decbbc0e 100644
--- a/tests/misc/wstring_phase6.i
+++ b/tests/misc/wstring_phase6.c
@@ -1,7 +1,8 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -journal-disable -print -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -journal-disable -print -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -variadic-no-translation
*/
+#include <stdio.h>
// See http://stackoverflow.com/questions/18102502/mixing-wide-and-narrow-string-literals-in-c
main(){
diff --git a/tests/non-free/imprecise-malloc-free.i b/tests/non-free/imprecise-malloc-free.i
index bf9ff9515b1..9e84a2190bd 100644
--- a/tests/non-free/imprecise-malloc-free.i
+++ b/tests/non-free/imprecise-malloc-free.i
@@ -11,7 +11,7 @@ void main() {
int size1, size2;
size1 = &size1 + i;
size2 = i + ((int)&size2 >> 1);
- int *p = Frama_C_malloc_by_stack(&i+(int)&i);
+ int *p = Frama_C_malloc_by_stack((unsigned long)&i+(int)&i);
int *q = Frama_C_malloc_by_stack(size1);
int *r = Frama_C_malloc_by_stack(size2);
diff --git a/tests/non-free/long_init.c b/tests/non-free/long_init.c
index ebb68157fc7..3627ca5d601 100644
--- a/tests/non-free/long_init.c
+++ b/tests/non-free/long_init.c
@@ -51,7 +51,7 @@ typedef int (*i_fp_i)(int);
i_fp_i fp = &fun;
//@ assigns a1[..], stuff, *pr, *pr2, *pr_escaping, *alloc1, *alloc2;
-void init_inner(int n, char *tea) {
+void init_inner(int n, char const *tea) {
int i;
/*@ slevel N3; */
for (i = 0; i < N1; i++) {
diff --git a/tests/non-free/long_init2.c b/tests/non-free/long_init2.c
index bc54a48a9c9..4703ca88ece 100644
--- a/tests/non-free/long_init2.c
+++ b/tests/non-free/long_init2.c
@@ -51,7 +51,7 @@ typedef int (*i_fp_i)(int);
i_fp_i fp = &fun;
//@ assigns a1[..], stuff, *pr, *pr2, *pr_escaping, *alloc1, *alloc2;
-void init_inner(int n, char *tea) {
+void init_inner(int n, char const *tea) {
int i;
/*@ slevel N3; */
for (i = 0; i < N1; i++) {
diff --git a/tests/non-free/long_init3.c b/tests/non-free/long_init3.c
index 0940cd2d2cc..5deed97d0ed 100644
--- a/tests/non-free/long_init3.c
+++ b/tests/non-free/long_init3.c
@@ -51,7 +51,7 @@ typedef int (*i_fp_i)(int);
i_fp_i fp = &fun;
//@ assigns a1[..], stuff, *pr, *pr2, *pr_escaping, *alloc1, *alloc2;
-void init_inner(int n, char *tea) {
+void init_inner(int n, char const *tea) {
int i;
/*@ slevel N3; */
for (i = 0; i < N1; i++) {
diff --git a/tests/non-free/memcpy.c b/tests/non-free/memcpy.c
index beb4bbe2011..a31ddae8d0b 100644
--- a/tests/non-free/memcpy.c
+++ b/tests/non-free/memcpy.c
@@ -142,7 +142,7 @@ void main (int a, int b){
// Size is a garbled mix
char garbledsize[100];
int* pgarbledsize = &garbledsize[10];
- Frama_C_memcpy(pgarbledsize, src, garbledsize);
+ Frama_C_memcpy(pgarbledsize, src, (unsigned int)garbledsize);
// Sure size may be zero
char dstmaybesize1[15], dstmaybesize2[150];
diff --git a/tests/non-free/memset.i b/tests/non-free/memset.i
index 53ea070b65d..eba8f318462 100644
--- a/tests/non-free/memset.i
+++ b/tests/non-free/memset.i
@@ -32,13 +32,13 @@ volatile int vol;
void main() {
void * dst = Frama_C_memset(t1, 0x11, sizeof(t1)); // basic
Frama_C_memset(t2+(int)t2, 0x12, sizeof(t2)); // garbled dest
- Frama_C_memset(t3+10, 0x11, t1); // garbled size
+ Frama_C_memset(t3+10, 0x11, (unsigned long)t1); // garbled size
if (vol) {
Frama_C_memset(t4+1, 1, sizeof(t4)); // out of bounds
}
- Frama_C_memset(t5, t1, sizeof(t4)); // garbled char
+ Frama_C_memset(t5, (int)t1, sizeof(t4)); // garbled char
int *p = vol ? t6+10 : t7;
Frama_C_memset(p, 0x22, 16); // multiple dest
diff --git a/tests/non-free/strchr.c b/tests/non-free/strchr.c
index 77353eab236..e065f100f03 100644
--- a/tests/non-free/strchr.c
+++ b/tests/non-free/strchr.c
@@ -175,9 +175,9 @@ void strchr_bitfields2() {
//@assert (z1 == 2);
}
-void init_array_nondet(char *a, int from, int to, int val1, int val2) {
+void init_array_nondet(void *a, int from, int to, int val1, int val2) {
int val = NONDET(val1, val2);
- Frama_C_memset(a + from, val, to-from+1);
+ Frama_C_memset(((char*)a) + from, val, to-from+1);
from = to = val1 = val2 = -1; // reset to minimize oracle changes
}
@@ -356,17 +356,17 @@ void strchr_big_array () {
long len_t;
// without initialization, most accesses are invalid, so the result is precise
- len_u = my_strchr(u, 0, c); // below plevel; precise
- len_r = my_strchr(r, 0, c); // above plevel; imprecise
- len_t = my_strchr(t, 0, c); // *far* above plevel
+ len_u = my_strchr((char const *)u, 0, c); // below plevel; precise
+ len_r = my_strchr((char const *)r, 0, c); // above plevel; imprecise
+ len_t = my_strchr((char const *)t, 0, c); // *far* above plevel
Frama_C_show_each(len_u, len_r, len_t);
//@ assert (len_u == 1);
//@ assert (len_r == 1);
//@ assert (len_t == 1);
- len_u = my_strchr(u, nondet, c); // should be precise
- len_r = my_strchr(r, nondet, c);
- len_t = my_strchr(t, nondet, c);
+ len_u = my_strchr((char const *)u, nondet, c); // should be precise
+ len_r = my_strchr((char const *)r, nondet, c);
+ len_t = my_strchr((char const *)t, nondet, c);
Frama_C_show_each(len_u, len_r, len_t);
//@ assert (len_u >= -1 && len_u <= 799);
//@ assert (len_r >= -1 && len_r <= 803);
@@ -384,17 +384,17 @@ void strchr_big_array () {
*p = 0x10230067;
p = &t[nondet];
*p = 0x10230067;
- len_u = my_strchr(u, 0, c); // below plevel; precise
- len_r = my_strchr(r, 0, c); // above plevel; imprecise
- len_t = my_strchr(t, 0, c); // *far* above plevel
+ len_u = my_strchr((char const *)u, 0, c); // below plevel; precise
+ len_r = my_strchr((char const *)r, 0, c); // above plevel; imprecise
+ len_t = my_strchr((char const *)t, 0, c); // *far* above plevel
Frama_C_show_each(len_u, len_r, len_t);
//@ assert (len_u >= 0 && len_u <= 799);
//@ assert (len_r >= 0 && len_r <= 803);
//@ assert (len_t >= 0 && len_t <= 3999999);
- len_u = my_strchr(u, nondet, c); // should be precise
- len_r = my_strchr(r, nondet, c);
- len_t = my_strchr(t, nondet, c);
+ len_u = my_strchr((char const *)u, nondet, c); // should be precise
+ len_r = my_strchr((char const *)r, nondet, c);
+ len_t = my_strchr((char const *)t, nondet, c);
Frama_C_show_each(len_u, len_r, len_t);
//@ assert (len_u >= -1 && len_u <= 799);
//@ assert (len_r >= -1 && len_r <= 803);
@@ -525,13 +525,13 @@ void strchr_unbounded() {
void strchr_invalid() {
CHAR_PTR(s);
STRING(s,"hello");
- my_strchr(s, &s, 1);
+ my_strchr(s, (unsigned int)&s, 1);
}
void strchr_garbled_mix_in_char() {
int x;
char *garbled = ((int)(&x + (int)&x));
- strchr(garbled, garbled); // must not crash
+ strchr(garbled, (int)garbled); // must not crash
}
int main () {
diff --git a/tests/non-free/strlen.c b/tests/non-free/strlen.c
index f45980a6d36..f1e34b98345 100644
--- a/tests/non-free/strlen.c
+++ b/tests/non-free/strlen.c
@@ -294,14 +294,14 @@ void big_array () {
unsigned long len_r;
unsigned long len_t;
- len_u = strlen(u); // below plevel; precise
- len_r = strlen(r); // above plevel; imprecise
- len_t = strlen(t); // *far* above plevel
+ len_u = strlen((char const *)u); // below plevel; precise
+ len_r = strlen((char const *)r); // above plevel; imprecise
+ len_t = strlen((char const *)t); // *far* above plevel
Frama_C_show_each(len_u, len_r, len_t);
- len_u = strlen(u+nondet); // should be precise
- len_r = strlen(r+nondet);
- len_t = strlen(t+nondet);
+ len_u = strlen((char const *)(u+nondet)); // should be precise
+ len_r = strlen((char const *)(r+nondet));
+ len_t = strlen((char const *)(t+nondet));
Frama_C_show_each(len_u, len_r, len_t);
}
diff --git a/tests/non-free/strnlen2.c b/tests/non-free/strnlen2.c
index dd3a006258b..7a1a31b9b09 100644
--- a/tests/non-free/strnlen2.c
+++ b/tests/non-free/strnlen2.c
@@ -133,9 +133,9 @@ void bitfields2() {
//@assert (z1 == 2);
}
-void init_array_nondet(char *a, int from, int to, int val1, int val2) {
+void init_array_nondet(void *a, int from, int to, int val1, int val2) {
int val = nondet ? val1 : val2;
- Frama_C_memset(a + from, val, to-from+1);
+ Frama_C_memset(((char*)a) + from, val, to-from+1);
from = to = val1 = val2 = -1; // reset to minimize oracle changes
}
@@ -269,9 +269,9 @@ void big_array () {
unsigned long len_t;
// without initialization, most accesses are invalid, so the result is precise
- len_u = strnlen(u, 800); // below plevel; precise
- len_r = strnlen(r, 804); // above plevel; imprecise
- len_t = strnlen(t, 4000000); // *far* above plevel
+ len_u = strnlen((char const *)u, 800); // below plevel; precise
+ len_r = strnlen((char const *)r, 804); // above plevel; imprecise
+ len_t = strnlen((char const *)t, 4000000); // *far* above plevel
//@ assert len_u == 1;
//@ assert len_r == 1;
//@ assert len_t == 1;
@@ -279,9 +279,9 @@ void big_array () {
// less precise results here, but uninitialized values at the end of the
// arrays ensure a slightly better result than afterwards
- len_u = strnlen(u+nondet,801); // should be precise
- len_r = strnlen(r+nondet,805);
- len_t = strnlen(t+nondet,4000001);
+ len_u = strnlen((char const *)(u+nondet),801); // should be precise
+ len_r = strnlen((char const *)(r+nondet),805);
+ len_t = strnlen((char const *)(t+nondet),4000001);
//@ assert len_u >= 0 && len_u <= 3;
//@ assert len_r >= 0 && len_r <= 800;
//@ assert len_t >= 0 && len_t <= 3999996;
@@ -297,17 +297,17 @@ void big_array () {
*p = 0x10230067;
p = &t[nondet];
*p = 0x10230067;
- len_u = strnlen(u, 800); // below plevel; precise
- len_r = strnlen(r, 804); // above plevel; imprecise
- len_t = strnlen(t, 4000000); // *far* above plevel
+ len_u = strnlen((char const *)u, 800); // below plevel; precise
+ len_r = strnlen((char const *)r, 804); // above plevel; imprecise
+ len_t = strnlen((char const *)t, 4000000); // *far* above plevel
//@ assert len_u >= 0 && len_u <= 800;
//@ assert len_r >= 0 && len_r <= 804;
//@ assert len_t >= 0 && len_t <= 4000000;
Frama_C_show_each(len_u, len_r, len_t);
- len_u = strnlen(u+nondet,801); // should be precise
- len_r = strnlen(r+nondet,805);
- len_t = strnlen(t+nondet,4000001);
+ len_u = strnlen((char const *)(u+nondet),801); // should be precise
+ len_r = strnlen((char const *)(r+nondet),805);
+ len_t = strnlen((char const *)(t+nondet),4000001);
//@ assert len_u >= 0 && len_u <= 799;
//@ assert len_r >= 0 && len_r <= 803;
//@ assert len_t >= 0 && len_t <= 3999999;
diff --git a/tests/non-free/wcslen.c b/tests/non-free/wcslen.c
index 8d9d2db1d7b..634278f96ee 100644
--- a/tests/non-free/wcslen.c
+++ b/tests/non-free/wcslen.c
@@ -298,14 +298,14 @@ void big_array () {
unsigned long len_r;
unsigned long len_t;
- len_u = wcslen(u); // below plevel; precise
- len_r = wcslen(r); // above plevel; imprecise
- len_t = wcslen(t); // *far* above plevel
+ len_u = wcslen((wchar_t const *)u); // below plevel; precise
+ len_r = wcslen((wchar_t const *)r); // above plevel; imprecise
+ len_t = wcslen((wchar_t const *)t); // *far* above plevel
Frama_C_show_each(len_u, len_r, len_t);
- len_u = wcslen(u+nondet); // should be precise
- len_r = wcslen(r+nondet);
- len_t = wcslen(t+nondet);
+ len_u = wcslen((wchar_t const *)(u+nondet)); // should be precise
+ len_r = wcslen((wchar_t const *)(r+nondet));
+ len_t = wcslen((wchar_t const *)(t+nondet));
Frama_C_show_each(len_u, len_r, len_t);
}
diff --git a/tests/slicing/unravel-variance.i b/tests/slicing/unravel-variance.i
index 4901c685022..bb639777c85 100644
--- a/tests/slicing/unravel-variance.i
+++ b/tests/slicing/unravel-variance.i
@@ -31,7 +31,7 @@ main()
scanf ("%d", &n);
for ( i = 0 ; i < n ; i = i + 1)
{
- scanf ("%f", &x[i]);
+ scanf ("%f", (int*)&x[i]);
t1 = t1 + x[i];
ssq = ssq + x[i] * x[i];
}
diff --git a/tests/spec/if.c b/tests/spec/if.c
index 3deec3c6a54..3b600c03123 100644
--- a/tests/spec/if.c
+++ b/tests/spec/if.c
@@ -10,5 +10,5 @@ void g(char*s);
void f() {
int x = 0;
//@ assert P(x);
- g(x);
+ g((char*)x);
}
diff --git a/tests/spec/second.c b/tests/spec/second.c
index a4d9edd4f55..87a73a0b910 100644
--- a/tests/spec/second.c
+++ b/tests/spec/second.c
@@ -8,6 +8,6 @@
int bar(int *second);
void sub (char * c) {
- bar(c);
+ bar((int*)c);
}
diff --git a/tests/syntax/gnu-asm-aesni.c b/tests/syntax/gnu-asm-aesni.c
index c629ec9f859..57f21d3dc98 100644
--- a/tests/syntax/gnu-asm-aesni.c
+++ b/tests/syntax/gnu-asm-aesni.c
@@ -160,7 +160,7 @@ void encrypt_aesni(void)
for(i=0; i<MAXROUNDS+1; i++)
for(j=0; j<4; j++)
for(k=0; k<4; k++){
- Frama_C_make_unknown(&ctx.keyschenc[i][j][k], sizeof(byte));
+ Frama_C_make_unknown((char*)&ctx.keyschenc[i][j][k], sizeof(byte));
}
ctx.rounds = 12;
ctx.use_aesni = 1;
diff --git a/tests/syntax/sizeof_bts1414.i b/tests/syntax/sizeof_bts1414.i
index 42b8870df11..a52489892c2 100644
--- a/tests/syntax/sizeof_bts1414.i
+++ b/tests/syntax/sizeof_bts1414.i
@@ -2,7 +2,7 @@ int f(int b);
int g(int *a)
{
int x ;
- x = sizeof(f(a));
+ x = sizeof(f(*a));
switch (x) {
case (sizeof(x++)): return 1;
default: return 0;
diff --git a/tests/value/alias.i b/tests/value/alias.i
index cc69a358a8f..048db091421 100644
--- a/tests/value/alias.i
+++ b/tests/value/alias.i
@@ -42,9 +42,9 @@ void main (void) {
/* SECTION 1 */
A=1;
B=2;
- f(&A,&B);
- f(&A,&A);
- f(&p,&B);
+ f((char*)&A,&B);
+ f((char*)&A,&A);
+ f((char*)&p,&B);
/* SECTION 2 */
x = 1;
@@ -265,7 +265,7 @@ void main11(void)
}
D = *PTR3;
- f2(p2);
+ f2((char*)p2);
t = c2?0:1;
ll1 = (c2+1)?15:16;
diff --git a/tests/value/array_ptr.i b/tests/value/array_ptr.i
index e605a00e5c7..74ddfa99602 100644
--- a/tests/value/array_ptr.i
+++ b/tests/value/array_ptr.i
@@ -12,5 +12,5 @@ param_check l={1};
int main() {
int g = &l;
- f(&g);
+ f((param_check **)&g);
}
diff --git a/tests/value/assigns.i b/tests/value/assigns.i
index 96e6e4fd57a..940d04ab5cd 100644
--- a/tests/value/assigns.i
+++ b/tests/value/assigns.i
@@ -46,12 +46,12 @@ void main1(void)
F1(T);
for (int i=0;i<=5;i++)
- f(&t[i].f2);
+ f((char*)&t[i].f2);
g(2 * (int)(&T) );
- h(2 * (int)(&t3) );
+ h((int*)(2 * (int)(&t3)));
- j(T+9);
+ j((int*)(T+9));
assigns_post(18);
}
diff --git a/tests/value/behaviors1.i b/tests/value/behaviors1.i
index c5f7a0fa28c..d3e9105309a 100644
--- a/tests/value/behaviors1.i
+++ b/tests/value/behaviors1.i
@@ -470,9 +470,9 @@ void test_assigns() {
int a, b;
int *p1, *p2, *p3;
- p1 = f(&a, &b); // garbled_mix of &{a}
- p2 = f(0, &b); // garbled_mix of &{b}
- p3 = f(0, 0); // [0..+oo]
+ p1 = (int*)f(&a, &b); // garbled_mix of &{a}
+ p2 = (int*)f(0, &b); // garbled_mix of &{b}
+ p3 = (int*)f(0, 0); // [0..+oo]
}
char T[10];
@@ -602,7 +602,7 @@ void test_small6_bis() {
ensures \result == 1;
complete behaviors;
*/
-int f9(char* s, int n);
+int f9(char const* s, int n);
void test_promote() {
int x = nondet;
diff --git a/tests/value/call.i b/tests/value/call.i
index c88401bb7b8..28370c23b38 100644
--- a/tests/value/call.i
+++ b/tests/value/call.i
@@ -16,7 +16,7 @@ void leaf_fun_charp(char* x);
@*/
void main(int c, char **v)
{
- if (c&1) leaf_fun_int(v[1]);
+ if (c&1) leaf_fun_int((int)v[1]);
if (c&2) leaf_fun_charp(v[1]);
int lcount= 0;
res= 1111;
diff --git a/tests/value/const.i b/tests/value/const.i
index 340e8018926..ed1a7b1b5da 100644
--- a/tests/value/const.i
+++ b/tests/value/const.i
@@ -37,7 +37,7 @@ void modify_I (){
Frama_C_show_each(I);
if (v) I++;
if (v) pointer_to_const(&I);
- if (v) const_destination(&I);
+ if (v) const_destination((int *)&I);
}
void modify_J (){
@@ -51,14 +51,14 @@ void modify_s (){
Frama_C_show_each(s.i1);
if (v) s.i1 ++;
if (v) pointer_to_const(&s.i2);
- if (v) const_destination(&s.i2);
+ if (v) const_destination((int *)&s.i2);
}
void modify_t(){
Frama_C_show_each(t[5]);
if (v) t[5] ++;
if (v) pointer_to_const(&t[3]);
- if (v) const_destination(&t[2]);
+ if (v) const_destination((int *)&t[2]);
}
diff --git a/tests/value/context_free.i b/tests/value/context_free.i
index 4af95e92fc0..b5a4573306d 100644
--- a/tests/value/context_free.i
+++ b/tests/value/context_free.i
@@ -36,7 +36,7 @@ extern struct {
extern void *qvoid; // void* pointer: valid, size unknown
-void f(int x, float y, int **p, int (*g)(char *), void *vv, void **vvv, int ta[5])
+void f(int x, float y, int **p, int (*g)(char const*), void *vv, void **vvv, int ta[5])
{
if (x >= 0) a = x;
b = s.s1 ;
diff --git a/tests/value/gauges.i b/tests/value/gauges.i
index 19452432fea..5a8888cec98 100644
--- a/tests/value/gauges.i
+++ b/tests/value/gauges.i
@@ -206,7 +206,7 @@ int main10() {
float p = 1;
float A[10] = {1};
float B[10] = {2};
- return (int)main10_aux(&p, &A, &B, 10);
+ return (int)main10_aux(&p, A, B, 10);
}
void main11 () {
diff --git a/tests/value/initialized.c b/tests/value/initialized.c
index cad6b37c561..a91a0ad32ea 100644
--- a/tests/value/initialized.c
+++ b/tests/value/initialized.c
@@ -95,8 +95,8 @@ void g3() {
if (b3) x3 = 1;
r3 = x3 + 1;
- f(b6, &t1, 4);
- f(b6, &t2, 250); // above plevel. Works because the location is contiguous
+ f(b6, t1, 4);
+ f(b6, t2, 250); // above plevel. Works because the location is contiguous
}
void g4() {
@@ -150,7 +150,7 @@ void g6() {
void g7() {
unsigned char key[128];
- Frama_C_make_unknown(key, 64);
+ Frama_C_make_unknown((char*)key, 64);
//@ assert !\initialized(&key[0..127]);
}
diff --git a/tests/value/leaf2.i b/tests/value/leaf2.i
index d72f9cb1108..4da57130485 100644
--- a/tests/value/leaf2.i
+++ b/tests/value/leaf2.i
@@ -3,7 +3,7 @@ extern T f(char* p,int q, int i);
T G,H,I;
void main (void) {
- G = f(&H,(int)&I,17);
+ G = f((char*)&H,(int)&I,17);
if (G == -1) G++;
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 860d55a1eff..b2323316224 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -232,7 +232,7 @@ tests/value/gauges.i:200:[value] warning: non-finite float value.
[value] Done for function main10_aux
tests/value/gauges.i:209:[value] warning: overflow in conversion from floating-point to integer.
assert tmp < 2147483648;
- (tmp from main10_aux(& p, (float const *)(& A), (float const *)(& B), 10))
+ (tmp from main10_aux(& p, (float const *)(A), (float const *)(B), 10))
[value] Recording results for main10
[value] Done for function main10
[value] computing for function main11 <- main.
diff --git a/tests/value/reduce_formals.i b/tests/value/reduce_formals.i
index 6c0591e6cac..0085715fe88 100644
--- a/tests/value/reduce_formals.i
+++ b/tests/value/reduce_formals.i
@@ -16,7 +16,7 @@ void main3 (void) {
long x = 3;
long * p = &x;
//@ assert sizeof(long) == sizeof(int);
- f_main3 (p, x); // go through the casts on p and x
+ f_main3 ((int *)p, x); // go through the casts on p and x
Frama_C_show_each(x);
}
diff --git a/tests/value/strings_cond.i b/tests/value/strings_cond.i
index 20b0016d8c7..a6bc0c8d157 100644
--- a/tests/value/strings_cond.i
+++ b/tests/value/strings_cond.i
@@ -1,5 +1,5 @@
-void foo(char *s) {
+void foo(char const *s) {
Frama_C_dump_each();
while(*s) { Frama_C_show_each_s(s); s++; }
}
--
GitLab