From a0e48f90dbb0e81b76aa10b5c87d1e4c1f17fb00 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 20 Sep 2024 09:27:56 +0200
Subject: [PATCH] [tests] Add specifier of implicit ints in tests
---
src/plugins/dive/tests/dive/const.i | 2 +-
.../tests/loop_analysis/non_natural_loop.i | 2 +-
src/plugins/report/tests/report/csv.c | 2 +-
src/plugins/variadic/tests/known/fcntl.c | 2 +-
.../tests/known/printf_wrong_pointers.c | 2 +-
tests/builtins/alloc_weak.c | 2 +-
tests/builtins/free.c | 2 +-
tests/builtins/malloc-optimistic.c | 2 +-
tests/builtins/malloc-size-zero.c | 2 +-
tests/builtins/malloc_memexec.c | 2 +-
tests/builtins/memcpy.c | 2 +-
tests/builtins/precise_memset.c | 2 +-
tests/builtins/realloc.c | 2 +-
tests/float/alarms.i | 2 +-
tests/float/builtins.c | 2 +-
tests/float/cond_cast_int_to_float.c | 2 +-
tests/float/conv.i | 2 +-
tests/float/div.i | 2 +-
tests/float/dr_infinity.i | 2 +-
tests/float/logic.i | 2 +-
tests/float/parse.i | 2 +-
tests/impact/loop2.i | 2 +-
tests/misc/oracle/audit-out.json | 2 +-
tests/pdg/bts1194.c | 2 +-
tests/scope/bts971.c | 2 +-
tests/syntax/built.i | 2 +-
tests/syntax/exit.c | 2 +-
tests/syntax/implicit-int.i | 14 ++++++++++
tests/syntax/inline_def_1.i | 2 +-
tests/syntax/inline_def_2.i | 4 +--
tests/syntax/inline_def_bad_1.i | 2 +-
tests/syntax/inline_def_bad_2.i | 2 +-
tests/syntax/merge_inline_1.c | 2 +-
tests/syntax/oracle/implicit-int.res.oracle | 27 +++++++++++++++++++
tests/syntax/static_formals.h | 2 +-
tests/syntax/unroll_labels.i | 2 +-
tests/value/alias.i | 2 +-
tests/value/bitfield.i | 2 +-
tests/value/bitwise_reduction.i | 2 +-
tests/value/builtins_split.c | 2 +-
tests/value/const.i | 2 +-
tests/value/constarraystructlibentry.i | 4 +--
tests/value/conversion.i | 2 +-
tests/value/dataflow_order.i | 2 +-
tests/value/degeneration2.i | 2 +-
tests/value/deps_unitialized_locals.i | 2 +-
tests/value/downcast.i | 2 +-
tests/value/gauges.c | 2 +-
tests/value/if2.i | 2 +-
tests/value/init_const_guard.i | 2 +-
tests/value/initialized.c | 2 +-
tests/value/library.i | 2 +-
tests/value/local_slevel.i | 2 +-
tests/value/logic.c | 2 +-
tests/value/modulo.i | 2 +-
tests/value/non_natural.i | 6 ++---
tests/value/overflow_cast_float_int.i | 2 +-
tests/value/partitioning-annots.c | 2 +-
tests/value/reduce_by_valid.i | 2 +-
tests/value/shift.i | 2 +-
tests/value/split_return.i | 4 +--
tests/value/struct_array.i | 2 +-
tests/value/subset.c | 2 +-
tests/value/symbolic_locs.i | 4 +--
tests/value/unop.c | 2 +-
65 files changed, 110 insertions(+), 69 deletions(-)
create mode 100644 tests/syntax/implicit-int.i
create mode 100644 tests/syntax/oracle/implicit-int.res.oracle
diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i
index 622693ee684..76239a315c3 100644
--- a/src/plugins/dive/tests/dive/const.i
+++ b/src/plugins/dive/tests/dive/const.i
@@ -4,7 +4,7 @@ STDOPT: +"-dive-from-variables main::res -dive-depth-limit 5"
int f(int x, int y)
{
- const c = x + 1;
+ const int c = x + 1;
int w = y + 1;
return c + w;
}
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/non_natural_loop.i b/src/plugins/loop_analysis/tests/loop_analysis/non_natural_loop.i
index ad1d08d2555..ff29ee9cc8d 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/non_natural_loop.i
+++ b/src/plugins/loop_analysis/tests/loop_analysis/non_natural_loop.i
@@ -1,5 +1,5 @@
void duff(int *to, int *from, int count) {
- register n = (count + 7) / 8;
+ register int n = (count + 7) / 8;
switch(count % 8) {
case 0: do {
Frama_C_show_each(to);
diff --git a/src/plugins/report/tests/report/csv.c b/src/plugins/report/tests/report/csv.c
index c9e27daea85..79b12fd184b 100644
--- a/src/plugins/report/tests/report/csv.c
+++ b/src/plugins/report/tests/report/csv.c
@@ -4,7 +4,7 @@ PLUGIN: report from,inout,scope,eva
OPT: -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
COMMENT: first, do an analysis without any message, but check that the .csv is complete. Then, redo the analysis with value warnings. slevel 1 is just there to force Value to restart
*/
-volatile v;
+volatile int v;
void main1(int x) {
int t[10];
int u[15];
diff --git a/src/plugins/variadic/tests/known/fcntl.c b/src/plugins/variadic/tests/known/fcntl.c
index bb291039664..f8d3c7d095b 100644
--- a/src/plugins/variadic/tests/known/fcntl.c
+++ b/src/plugins/variadic/tests/known/fcntl.c
@@ -2,7 +2,7 @@
int main(){
struct flock fl;
- volatile choice = 0;
+ volatile int choice = 0;
// Normal usage
int flags = fcntl(0, F_GETFD);
diff --git a/src/plugins/variadic/tests/known/printf_wrong_pointers.c b/src/plugins/variadic/tests/known/printf_wrong_pointers.c
index 6f70884be9c..9a7fbf0c122 100644
--- a/src/plugins/variadic/tests/known/printf_wrong_pointers.c
+++ b/src/plugins/variadic/tests/known/printf_wrong_pointers.c
@@ -6,7 +6,7 @@ int main(){
char *string = "foo";
wchar_t *wstring = L"bar";
- volatile nondet = 0;
+ volatile int nondet = 0;
// Wrong pointers are passed to printf and this must be detected by value
switch (nondet)
diff --git a/tests/builtins/alloc_weak.c b/tests/builtins/alloc_weak.c
index 020c7e0458d..3a78f843a09 100644
--- a/tests/builtins/alloc_weak.c
+++ b/tests/builtins/alloc_weak.c
@@ -5,7 +5,7 @@
#include <stdlib.h>
#include <string.h>
-volatile v;
+volatile int v;
static void copy(void *dst_, void *src_, size_t off, size_t len)
{
diff --git a/tests/builtins/free.c b/tests/builtins/free.c
index a16798e5ff9..7bd178b9111 100644
--- a/tests/builtins/free.c
+++ b/tests/builtins/free.c
@@ -2,7 +2,7 @@
STDOPT: #" -eva-alloc-builtin fresh"
*/
#include "stdlib.h"
-volatile v;
+volatile int v;
void main1() {
int *p = malloc(40);
diff --git a/tests/builtins/malloc-optimistic.c b/tests/builtins/malloc-optimistic.c
index 8b2a9551ec0..cbd3bd8589c 100644
--- a/tests/builtins/malloc-optimistic.c
+++ b/tests/builtins/malloc-optimistic.c
@@ -8,7 +8,7 @@ void *malloc(size_t size);
//@ assigns \nothing; frees p;
void free(void *p);
-volatile v;
+volatile int v;
void* main1() {
int i, *p;
diff --git a/tests/builtins/malloc-size-zero.c b/tests/builtins/malloc-size-zero.c
index 0ff4c5e749f..7b717dfc354 100644
--- a/tests/builtins/malloc-size-zero.c
+++ b/tests/builtins/malloc-size-zero.c
@@ -10,7 +10,7 @@ void* my_calloc (int s, int n) {
return malloc (s*n);
}
-volatile foo;
+volatile int foo;
void main () {
char *p1 = my_calloc (0, 0);
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index cac60b4be31..f32b9f6ac27 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -7,7 +7,7 @@ void f(int *p, int i) {
*p = i;
}
-volatile v;
+volatile int v;
void main() {
/*@ eva_allocate fresh; */
diff --git a/tests/builtins/memcpy.c b/tests/builtins/memcpy.c
index 1eee41ee76b..2fedf2a766e 100644
--- a/tests/builtins/memcpy.c
+++ b/tests/builtins/memcpy.c
@@ -24,7 +24,7 @@ void init () {
for (j=0;j<100;j++) dst5[j] = -1;
}
-volatile maybe;
+volatile int maybe;
void buggy () {
char c;
diff --git a/tests/builtins/precise_memset.c b/tests/builtins/precise_memset.c
index a0ef943db02..c0e73b872f2 100644
--- a/tests/builtins/precise_memset.c
+++ b/tests/builtins/precise_memset.c
@@ -5,7 +5,7 @@
#include "string.h"
-volatile v;
+volatile int v;
int x;
diff --git a/tests/builtins/realloc.c b/tests/builtins/realloc.c
index b67d078b18d..75c1003690a 100644
--- a/tests/builtins/realloc.c
+++ b/tests/builtins/realloc.c
@@ -137,7 +137,7 @@ void main9() {
free (q);
}
-volatile v;
+volatile int v;
void f(int x) {
Frama_C_show_each(x);
diff --git a/tests/float/alarms.i b/tests/float/alarms.i
index 8d60a075054..a989d92374e 100644
--- a/tests/float/alarms.i
+++ b/tests/float/alarms.i
@@ -9,7 +9,7 @@ float f;
double d, big;
unsigned long long ull;
double fd(void);
-volatile rand;
+volatile int rand;
void main1 (long long l){
u1.l = l;
diff --git a/tests/float/builtins.c b/tests/float/builtins.c
index 614f78d751b..6d90c77d675 100644
--- a/tests/float/builtins.c
+++ b/tests/float/builtins.c
@@ -41,7 +41,7 @@ void main(int c, char **v)
-volatile v;
+volatile int v;
void main_log_exp(double d) {
double l1, l2, l3, l4, l5, l6, l7, l8;
diff --git a/tests/float/cond_cast_int_to_float.c b/tests/float/cond_cast_int_to_float.c
index 83491cc202a..d053970a3e5 100644
--- a/tests/float/cond_cast_int_to_float.c
+++ b/tests/float/cond_cast_int_to_float.c
@@ -1,4 +1,4 @@
-volatile v;
+volatile int v;
//@ requires c; assigns \nothing;
void __assert(int c);
diff --git a/tests/float/conv.i b/tests/float/conv.i
index ef357137277..5d3f1421a6f 100644
--- a/tests/float/conv.i
+++ b/tests/float/conv.i
@@ -5,7 +5,7 @@
float f;
double d;
-volatile v;
+volatile int v;
// Conversion from binary integer representation to float
void main1() {
diff --git a/tests/float/div.i b/tests/float/div.i
index bbd3b589429..4d1337f0183 100644
--- a/tests/float/div.i
+++ b/tests/float/div.i
@@ -1,4 +1,4 @@
-volatile v;
+volatile int v;
void main() {
double d1, d2;
diff --git a/tests/float/dr_infinity.i b/tests/float/dr_infinity.i
index 9ed72782982..2c7f8798b5a 100644
--- a/tests/float/dr_infinity.i
+++ b/tests/float/dr_infinity.i
@@ -1,7 +1,7 @@
/* run.config*
STDOPT: #"-kernel-warn-key parser:decimal-float=active -float-hex"
*/
-volatile v;
+volatile int v;
void main(void)
{
float x; double d;
diff --git a/tests/float/logic.i b/tests/float/logic.i
index 52402c55205..f9bc3941bcc 100644
--- a/tests/float/logic.i
+++ b/tests/float/logic.i
@@ -3,7 +3,7 @@
STDOPT: #"-kernel-warn-key parser:decimal-float=active -float-hex -warn-special-float none"
*/
-volatile v;
+volatile int v;
volatile float any_float;
volatile double any_double;
diff --git a/tests/float/parse.i b/tests/float/parse.i
index d4fab9c06ab..deba35670bc 100644
--- a/tests/float/parse.i
+++ b/tests/float/parse.i
@@ -2,7 +2,7 @@
STDOPT: #"-kernel-warn-key parser:decimal-float=active -float-hex"
*/
-volatile v;
+volatile int v;
int main() {
if (v) {
diff --git a/tests/impact/loop2.i b/tests/impact/loop2.i
index efe9f7fac61..a492a59d96d 100644
--- a/tests/impact/loop2.i
+++ b/tests/impact/loop2.i
@@ -3,7 +3,7 @@
*/
-volatile v;
+volatile int v;
int t[10], u[10], w[10];
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index f078d477d54..42f5dbd8c9e 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -65,7 +65,7 @@
"parser:unsupported:pragma", "plugin-not-loaded", "pp",
"pp:compilation-db", "pp:line-directive", "project",
"too-large-array", "typing", "typing:implicit-conv-void-ptr",
- "typing:implicit-function-declaration",
+ "typing:implicit-function-declaration", "typing:implicit-int",
"typing:incompatible-pointer-types",
"typing:incompatible-types-call", "typing:inconsistent-specifier",
"typing:int-conversion", "typing:merge-conversion", "typing:no-proto"
diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c
index 37d50ee5443..5c3935b20fc 100644
--- a/tests/pdg/bts1194.c
+++ b/tests/pdg/bts1194.c
@@ -3,7 +3,7 @@ PLUGIN: @EVA_PLUGINS@ pdg slicing
STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print @EVA_OPTIONS@"
*/
int Y, X;
-volatile v;
+volatile int v;
//@ assigns \result \from \nothing;
int input(void);
diff --git a/tests/scope/bts971.c b/tests/scope/bts971.c
index 968ca119f33..641649849e6 100644
--- a/tests/scope/bts971.c
+++ b/tests/scope/bts971.c
@@ -4,7 +4,7 @@
OPT: -then -main main2
*/
/* bug 971: */
-volatile foo;
+volatile int foo;
int v;
void f1 () {
v += 1;
diff --git a/tests/syntax/built.i b/tests/syntax/built.i
index 25023c3bbc6..4de1013d3e7 100644
--- a/tests/syntax/built.i
+++ b/tests/syntax/built.i
@@ -4,7 +4,7 @@ STDOPT: +"-machdep gcc_x86_32"
extern __attribute__((const, noreturn))
int ____ilog2_NaN(void);
-_Noreturn inline dummy_f(void) { while(1); }
+_Noreturn inline int dummy_f(void) { while(1); }
static inline __attribute__((no_instrument_function)) __attribute__((const))
int __ilog2_u32(int n);
diff --git a/tests/syntax/exit.c b/tests/syntax/exit.c
index ba3cc9bfe79..9f782b6d95a 100644
--- a/tests/syntax/exit.c
+++ b/tests/syntax/exit.c
@@ -1,6 +1,6 @@
#include <stdlib.h>
-volatile c;
+volatile int c;
int f() {
if (c) {
diff --git a/tests/syntax/implicit-int.i b/tests/syntax/implicit-int.i
new file mode 100644
index 00000000000..ee4a6ad421a
--- /dev/null
+++ b/tests/syntax/implicit-int.i
@@ -0,0 +1,14 @@
+/* run.config
+ STDOPT: +"-kernel-warn-key typing:implicit-int=feedback"
+*/
+
+/* It is not allowed by ISO C11 6.7.2.2 to omit type specifier in a decaration,
+ but gcc and clang allow it with -Wimplicit-int. */
+
+const c;
+
+volatile v;
+
+extern f() { return c + v; }
+
+_Noreturn g(void) { while(1); }
diff --git a/tests/syntax/inline_def_1.i b/tests/syntax/inline_def_1.i
index 17dce1c7966..82d5dbad588 100644
--- a/tests/syntax/inline_def_1.i
+++ b/tests/syntax/inline_def_1.i
@@ -9,6 +9,6 @@ inline int f(int x) { return x; }
inline int f1() { return 1; }
// this time, f2 is a normal external definition.
-extern inline f2() { return 3; }
+extern inline int f2() { return 3; }
int g(int x) { return f(x) + f1() + f2 (); }
diff --git a/tests/syntax/inline_def_2.i b/tests/syntax/inline_def_2.i
index e58e9865cca..83a68daa5d5 100644
--- a/tests/syntax/inline_def_2.i
+++ b/tests/syntax/inline_def_2.i
@@ -4,8 +4,8 @@ DONTRUN: main test is in inline_def_1.i
int f(int x) { return x + 1; }
-inline f1 () { return 2; }
+inline int f1 () { return 2; }
-extern f2(void);
+extern int f2(void);
int h(int x) { return f(x) + f1() + f2(); }
diff --git a/tests/syntax/inline_def_bad_1.i b/tests/syntax/inline_def_bad_1.i
index 0a80ad46d0f..6f280b50b73 100644
--- a/tests/syntax/inline_def_bad_1.i
+++ b/tests/syntax/inline_def_bad_1.i
@@ -2,6 +2,6 @@
STDOPT: +"%{dep:./inline_def_bad_2.i}"
*/
-extern inline f() { return 1; }
+extern inline int f() { return 1; }
int g() { return f(); }
diff --git a/tests/syntax/inline_def_bad_2.i b/tests/syntax/inline_def_bad_2.i
index 984694238f2..ac6f318267a 100644
--- a/tests/syntax/inline_def_bad_2.i
+++ b/tests/syntax/inline_def_bad_2.i
@@ -3,6 +3,6 @@ DONTRUN: main test is inline_def_bad_1.i
*/
// should be an error: we have two definitions for the same function
-extern inline f() { return 42; }
+extern inline int f() { return 42; }
int h() { return f(); }
diff --git a/tests/syntax/merge_inline_1.c b/tests/syntax/merge_inline_1.c
index d1856bd086d..ce29cc149a2 100644
--- a/tests/syntax/merge_inline_1.c
+++ b/tests/syntax/merge_inline_1.c
@@ -8,7 +8,7 @@ int foo(int x); /* Declare it here. */
inline int foo(int x) { return x; }
-extern getfoo2(void);
+extern int getfoo2(void);
int main() {
if(getfoo2() != (int)foo) {
diff --git a/tests/syntax/oracle/implicit-int.res.oracle b/tests/syntax/oracle/implicit-int.res.oracle
new file mode 100644
index 00000000000..9264d716236
--- /dev/null
+++ b/tests/syntax/oracle/implicit-int.res.oracle
@@ -0,0 +1,27 @@
+[kernel] Parsing implicit-int.i (no preprocessing)
+[kernel:typing:implicit-int] implicit-int.i:8:
+ type specifier missing, defaults to 'int'; ISO C99 and later do not support implicit int
+[kernel:typing:implicit-int] implicit-int.i:10:
+ type specifier missing, defaults to 'int'; ISO C99 and later do not support implicit int
+[kernel:typing:implicit-int] implicit-int.i:12:
+ type specifier missing, defaults to 'int'; ISO C99 and later do not support implicit int
+[kernel:typing:implicit-int] implicit-int.i:14:
+ type specifier missing, defaults to 'int'; ISO C99 and later do not support implicit int
+/* Generated by Frama-C */
+int const c;
+int volatile v;
+extern int f(void)
+{
+ int __retres;
+ __retres = c + v;
+ return __retres;
+}
+
+ __attribute__((__noreturn__)) int g(void)
+{
+ int __retres;
+ while (1) ;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/static_formals.h b/tests/syntax/static_formals.h
index b3926492082..095ea458b94 100644
--- a/tests/syntax/static_formals.h
+++ b/tests/syntax/static_formals.h
@@ -1,2 +1,2 @@
//@ requires x < 10;
-static f(int x);
+static int f(int x);
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index cc85b245b77..00b16d23ea4 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -4,7 +4,7 @@ PLUGIN: eva,inout,scope
STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3"
*/
enum { SIX = 6 } ;
-volatile foo;
+volatile int foo;
void main () {
int j = 0;
/*@ loop unfold "completely", 4; */
diff --git a/tests/value/alias.i b/tests/value/alias.i
index 4b91cf96a5b..6ed23d01c9b 100644
--- a/tests/value/alias.i
+++ b/tests/value/alias.i
@@ -37,7 +37,7 @@ int t,u,v,w,x,y,z,t2,v2,*PTR1,*PTR2,*PTR3,*PTR4,*PTR5, *PTR6;
volatile int c,c1,c2,c3,c4;
void main (void) {
- volatile vol=0;
+ volatile int vol=0;
/* SECTION 1 */
A=1;
diff --git a/tests/value/bitfield.i b/tests/value/bitfield.i
index 595e5713872..e656ce91dc8 100644
--- a/tests/value/bitfield.i
+++ b/tests/value/bitfield.i
@@ -60,7 +60,7 @@ struct A {
void leaf (struct A *p1);
-volatile foo;
+volatile int foo;
void imprecise_bts_1671 ()
{
diff --git a/tests/value/bitwise_reduction.i b/tests/value/bitwise_reduction.i
index f2c89bf951a..e9ea293de46 100644
--- a/tests/value/bitwise_reduction.i
+++ b/tests/value/bitwise_reduction.i
@@ -3,7 +3,7 @@
STDOPT: +"-big-ints-hex 255 -machdep ppc_32"
*/
-volatile v;
+volatile int v;
void main1() {
int t[2];
diff --git a/tests/value/builtins_split.c b/tests/value/builtins_split.c
index cc38f28c313..215d879378d 100644
--- a/tests/value/builtins_split.c
+++ b/tests/value/builtins_split.c
@@ -5,7 +5,7 @@
int *p;
int x, y, t[10];
-volatile v;
+volatile int v;
//@ assigns \result \from i;
long long Frama_C_abstract_cardinal(long long i);
diff --git a/tests/value/const.i b/tests/value/const.i
index 644d6f04ac0..98be8097097 100644
--- a/tests/value/const.i
+++ b/tests/value/const.i
@@ -5,7 +5,7 @@ extern const int G;
extern const int I=2;
int J = 8;
-volatile v;
+volatile int v;
int X;
const struct {
diff --git a/tests/value/constarraystructlibentry.i b/tests/value/constarraystructlibentry.i
index 6d0f14ef293..01c21564c5b 100644
--- a/tests/value/constarraystructlibentry.i
+++ b/tests/value/constarraystructlibentry.i
@@ -24,8 +24,8 @@ const int t4[12] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
ss t5[7] = {{1, 2}, {3}, 5, 6, 7, 8, 9, 10};
ss2 t6[6] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
-extern const t7[5]; // Do not initialize to 0
-extern const t8[5] = {1, 2}; // Ignore extern (done by Cil)
+extern const int t7[5]; // Do not initialize to 0
+extern const int t8[5] = {1, 2}; // Ignore extern (done by Cil)
struct ts1 {int b; char c;};
struct ts2 {struct ts1 a; char c;};
diff --git a/tests/value/conversion.i b/tests/value/conversion.i
index a429feccfb7..c44c6420a69 100644
--- a/tests/value/conversion.i
+++ b/tests/value/conversion.i
@@ -4,7 +4,7 @@
// Comments are given for cases where -eva-warn-copy-indeterminate is not set
-volatile v;
+volatile int v;
void main() {
int x;
diff --git a/tests/value/dataflow_order.i b/tests/value/dataflow_order.i
index 9e7a25f5e77..bc704d9aff8 100644
--- a/tests/value/dataflow_order.i
+++ b/tests/value/dataflow_order.i
@@ -1,4 +1,4 @@
-volatile c;
+volatile int c;
unsigned int j, k;
diff --git a/tests/value/degeneration2.i b/tests/value/degeneration2.i
index 1fced460015..f5fcf7a06c6 100644
--- a/tests/value/degeneration2.i
+++ b/tests/value/degeneration2.i
@@ -1,7 +1,7 @@
/* The name of this file is probably historical, as Value no longer degenerates
on anything in it */
-volatile v;
+volatile int v;
void main (int c,int d) {
void *A,*B,*C,*D, *E;
diff --git a/tests/value/deps_unitialized_locals.i b/tests/value/deps_unitialized_locals.i
index c6c4aea9024..1c9eaded0c8 100644
--- a/tests/value/deps_unitialized_locals.i
+++ b/tests/value/deps_unitialized_locals.i
@@ -1,7 +1,7 @@
/* run.config*
STDOPT: #"-calldeps"
*/
-volatile maybe;
+volatile int maybe;
typedef struct {
short ts;
diff --git a/tests/value/downcast.i b/tests/value/downcast.i
index 6c01c21fd74..70d4eae7bdb 100644
--- a/tests/value/downcast.i
+++ b/tests/value/downcast.i
@@ -17,7 +17,7 @@ struct s {
unsigned j: 5;
};
-volatile v;
+volatile int v;
void main1(void) {
sz = sx + sy;
diff --git a/tests/value/gauges.c b/tests/value/gauges.c
index 8acfac2c411..571b69385c5 100644
--- a/tests/value/gauges.c
+++ b/tests/value/gauges.c
@@ -4,7 +4,7 @@
#include <stdlib.h>
-volatile v;
+volatile int v;
void main0() {
int i = 1;
diff --git a/tests/value/if2.i b/tests/value/if2.i
index d5fbe3ceb34..bd65e4f84b9 100644
--- a/tests/value/if2.i
+++ b/tests/value/if2.i
@@ -19,7 +19,7 @@ int G3 = 75, G4;
int R;
-volatile v;
+volatile int v;
enum Bool {
FALSE = 0,
diff --git a/tests/value/init_const_guard.i b/tests/value/init_const_guard.i
index 517c8278b61..6aa07fb3db5 100644
--- a/tests/value/init_const_guard.i
+++ b/tests/value/init_const_guard.i
@@ -21,7 +21,7 @@ int f(void)
return 0;
}
-volatile v;
+volatile int v;
/*@
ensures P_not_Const: \valid(&p);
diff --git a/tests/value/initialized.c b/tests/value/initialized.c
index 3e04b3cc716..16ce5f8cd32 100644
--- a/tests/value/initialized.c
+++ b/tests/value/initialized.c
@@ -12,7 +12,7 @@ void f(int m, int* t, int n) {
t[i]=i;
}
-volatile rand;
+volatile int rand;
void g1 (){
int t1[20], t2[20], t3[20], t4[20], t5[20], t6[20], i, j;
diff --git a/tests/value/library.i b/tests/value/library.i
index a7de6191a45..1eaaad8e96f 100644
--- a/tests/value/library.i
+++ b/tests/value/library.i
@@ -8,7 +8,7 @@ int *gpi;
/*@ assigns \result \from indirect:x, gpi; */
int *f_star_int(int x);
-int ****G; volatile v;
+int ****G; volatile int v;
int G0,*G1;
typedef int (*pfun)(int *p1, const int *p2);
diff --git a/tests/value/local_slevel.i b/tests/value/local_slevel.i
index 7c127424f77..e5b9dd94840 100644
--- a/tests/value/local_slevel.i
+++ b/tests/value/local_slevel.i
@@ -30,7 +30,7 @@ void g() {// Do not crash when loop unrolling clears the dependencies of the AST
}
int t[100];
-volatile vol;
+volatile int vol;
void main2() {
for (int i = 0; i < 100; i++) {
diff --git a/tests/value/logic.c b/tests/value/logic.c
index d8de93ab774..45dbca15496 100644
--- a/tests/value/logic.c
+++ b/tests/value/logic.c
@@ -1,7 +1,7 @@
#include "__fc_builtin.h"
int t[10], u[11];
struct ts { int f1; int f2; } s1, s2, s3[10];
-unsigned int x; volatile v;
+unsigned int x; volatile int v;
struct s1{
int x;
diff --git a/tests/value/modulo.i b/tests/value/modulo.i
index fbb77dc8f38..e802427c601 100644
--- a/tests/value/modulo.i
+++ b/tests/value/modulo.i
@@ -2,7 +2,7 @@
STDOPT: #"-eva-slevel-function pgcd1:100,pgcd2:100,pgcd3:100"
*/
int A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R;
-volatile v;
+volatile int v;
void main2 ()
{ int i = v;
diff --git a/tests/value/non_natural.i b/tests/value/non_natural.i
index 4ebeee5d6fd..b5634288f23 100644
--- a/tests/value/non_natural.i
+++ b/tests/value/non_natural.i
@@ -1,4 +1,4 @@
-volatile v;
+volatile int v;
void main1() {
int c = 0;
@@ -16,7 +16,7 @@ void main1() {
void duff1(int *to, int *from, int count) {
- register n = (count + 7) / 8;
+ register int n = (count + 7) / 8;
switch(count % 8) {
case 0: do {
Frama_C_show_each(to);
@@ -33,7 +33,7 @@ void duff1(int *to, int *from, int count) {
}
void duff2(int *to, int *from, int count) {
- register n = (count + 7) / 8;
+ register int n = (count + 7) / 8;
switch(count % 8) {
case 0: L: { Frama_C_show_each(to);
*to++ = *from++;
diff --git a/tests/value/overflow_cast_float_int.i b/tests/value/overflow_cast_float_int.i
index deac525af17..4ea0b53bd50 100644
--- a/tests/value/overflow_cast_float_int.i
+++ b/tests/value/overflow_cast_float_int.i
@@ -2,7 +2,7 @@
*/
-volatile v;
+volatile int v;
int main()
{
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index 393b1fe4bbd..6323f1df659 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -11,7 +11,7 @@
#define N 10
-volatile nondet;
+volatile int nondet;
void test_unroll()
{
diff --git a/tests/value/reduce_by_valid.i b/tests/value/reduce_by_valid.i
index 077c491e09d..0ed07fbc0a0 100644
--- a/tests/value/reduce_by_valid.i
+++ b/tests/value/reduce_by_valid.i
@@ -266,7 +266,7 @@ int* reduced_garbled_mix (int *p);
/* Tests reduction of garbled mix values by \valid and \valid_read. */
void main12(void) {
int x;
- const y = 16;
+ const int y = 16;
int a[5];
int *p = v ? &x : &a[0];
p = garbled_mix(p);
diff --git a/tests/value/shift.i b/tests/value/shift.i
index dc77652fe8a..e5f7444b98f 100644
--- a/tests/value/shift.i
+++ b/tests/value/shift.i
@@ -9,7 +9,7 @@ unsigned int ua,ub,uc,ud,ue,uf;
char t[10];
-volatile v;
+volatile int v;
int main(int c, int z, int zz) {
a=5024;
diff --git a/tests/value/split_return.i b/tests/value/split_return.i
index 08b7e3e2ea7..16161c9cb1c 100644
--- a/tests/value/split_return.i
+++ b/tests/value/split_return.i
@@ -128,7 +128,7 @@ void main5() {
}
}
-volatile v;
+volatile int v;
int f6() {
int i = v;
@@ -141,7 +141,7 @@ void main6() {
}
}
-volatile v;
+volatile int v;
int v7;
int* f7() {
diff --git a/tests/value/struct_array.i b/tests/value/struct_array.i
index 898aa91752d..03c07ce530d 100644
--- a/tests/value/struct_array.i
+++ b/tests/value/struct_array.i
@@ -2,7 +2,7 @@
STDOPT: +" -then -unsafe-arrays"
*/
-volatile v;
+volatile int v;
struct st1 {
long a;
diff --git a/tests/value/subset.c b/tests/value/subset.c
index 1bf34b0323b..42566220d5d 100644
--- a/tests/value/subset.c
+++ b/tests/value/subset.c
@@ -35,7 +35,7 @@ void main1(int i, int j) {
//@ assert p == \null || \valid(p);
}
-volatile v;
+volatile int v;
void main2() {
int x = 1;
diff --git a/tests/value/symbolic_locs.i b/tests/value/symbolic_locs.i
index 88d16de1dee..88195506235 100644
--- a/tests/value/symbolic_locs.i
+++ b/tests/value/symbolic_locs.i
@@ -2,8 +2,8 @@
STDOPT: +"-eva-domains symbolic-locations -eva-msg-key d-symblocs"
*/
-volatile v;
-int t[10]; extern u[10];
+volatile int v;
+int t[10]; extern int u[10];
void main1() {
unsigned int i = v;
diff --git a/tests/value/unop.c b/tests/value/unop.c
index 29b62f4e98e..102849ee97e 100644
--- a/tests/value/unop.c
+++ b/tests/value/unop.c
@@ -16,7 +16,7 @@ void main2(int i) {
}
}
-volatile v;
+volatile int v;
void main() {
main1((float)v);
--
GitLab