diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i index 622693ee684b1587bd5092c255096d84527beee3..76239a315c3380cca5977a625d8906b204ff2462 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 ad1d08d2555950389e5d57514eadae487ed7b3f2..ff29ee9cc8ddfd422944bf7393c99263552f1a30 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 c9e27daea85800e65c791ee988974205ca027585..79b12fd184b8e94931e6b389ab9e7019e09ef131 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 bb291039664b03f3c636a0bfc00026e31d20db0a..f8d3c7d095b61c5d5a85874491e40a17f26d3514 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 6f70884be9c9f57bcf36b7ffea57b52a203b8211..9a7fbf0c122ecc7d5071b1d9cdee112990980043 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 020c7e0458ddb3f3eba51190bd22c29db0e296ba..3a78f843a093a924ffec20946ff3c385e16aa80e 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 a16798e5ff968dd534fa977323c62e9eb59112fb..7bd178b9111939eedc2dcb0803a4fbd8f53c0285 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 8b2a9551ec09b64cec7500533acb4043d6d4df68..cbd3bd8589cb6b4af7da4a729c71ea4dbcbf33cc 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 0ff4c5e749f9ed70eb450993db8dcad2226ca561..7b717dfc35424c099d80aeebe84abbe4b226d554 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 cac60b4be3121fe0fe79ea701fee95860d0420a3..f32b9f6ac2718516ddcbcd7c57f82275f3d63833 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 1eee41ee76b0945dee477cf8f5602de8761e015a..2fedf2a766e0b960265061cddf6f3d21ed424690 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 a0ef943db027bddce81923cdad2bc8e362f90f39..c0e73b872f22ab9eb9fc5c2f681c967c86fa45dc 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 b67d078b18d1fdb6d51dfd9d95ca0cd7a1c68753..75c1003690a01a65caf759ec52c3859655c13832 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 8d60a075054d3ed035311ea24ecb62b5f24405c9..a989d92374ed9182aa58a03222c828a01e8e3b8a 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 614f78d751bfd7f5f816de33a7bd6146acd742b4..6d90c77d675c415bc851c29a971ade52f351ce8f 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 83491cc202ae8cb212d193588f0d184206ca1f45..d053970a3e56383773b744155447ea0a62c4a4b4 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 ef35713727730a5524ffa4fcf51fed76d6b416ae..5d3f1421a6f2f14bab90b749ec62c73f60021e82 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 bbd3b58942926b8dc94403a56ae10115faba86af..4d1337f0183f5218daa651379a7db55fd025c038 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 9ed727829827a3fb01cf0807fc4f37b54bd5edc5..2c7f8798b5a75ffa3808400bf42ef33d3ef1aad1 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 52402c55205cb4e7b577cadbac371de3a6687a1c..f9bc3941bcccc1a2ee2a289b3725061fe7dfc347 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 d4fab9c06ab6cb3394fa86071557cec9e0ebbdc3..deba35670bc9adb4d7675777bb70ea9cd484c970 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 efe9f7fac61cc78c35b173d9431de16b46dc890e..a492a59d96db6f456e7d8233e214fb562f0e37d2 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 f078d477d54e3ec8c44cda9d46117251acba0e6e..42f5dbd8c9e577b60e0897201d64343d212072e5 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 37d50ee5443a96ae718e5d645d5540edaea18da3..5c3935b20fcdecbcc7bd98f67be225b603539d6a 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 968ca119f331972615296755979e780362adc72f..641649849e6b901f127a7604dde5af91705d6908 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 25023c3bbc6788a0bfbde988e1a507d7458c7840..4de1013d3e7a5b3c37772a5cfbcae05d1a448b89 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 ba3cc9bfe79e4b6d93f1fc80d52552f9cb321b35..9f782b6d95a643e35cfd9e6e36914d42c4e96dcc 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 0000000000000000000000000000000000000000..ee4a6ad421a23fa429c2ee3d4f62920e8484b0f2 --- /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 17dce1c79660087b8632c54059ffb1b5a219065c..82d5dbad588ac549fb44defb4f6ef715751f1e9e 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 e58e9865cca6bacc169b12d45704977abd6e173a..83a68daa5d56b6b07429e0d99d7698eeda1774f8 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 0a80ad46d0f89ecdfc3852b9d8d3f645b2fe89d0..6f280b50b7327c37e67f23ab9131e2f27ea92361 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 984694238f2bf2754a3e3a8d673d02f60840a831..ac6f318267a9eb180b2f1fef1e65386afc5f1e64 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 d1856bd086d364e418d4a23f0dec9d46d844bbbe..ce29cc149a2149238254f77c73b030d21861dc99 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 0000000000000000000000000000000000000000..9264d7162361912c9012151fc3d1d82bf698da09 --- /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 b39264920822d1fddac4e0ae29e3088907466525..095ea458b94ae564d00cad4118221f18e8f34de0 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 cc85b245b77bb2e776294faefd15b949b7905117..00b16d23ea451518723b4a377a37376a86e38e47 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 4b91cf96a5b9397faf75c5a65279b01cff0312ba..6ed23d01c9bb04680c2f977894b071b959f37099 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 595e57138722f50050cc50b5bc27dcdaa4533292..e656ce91dc8c8c429ba846f816d931f2d8bbfd30 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 f2c89bf951a49f5b6c9c4c83ef1b2c39c87c1559..e9ea293de463980ab28f865c54396701fab9141f 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 cc38f28c313dbd9e2c022b8eabe768de8f2a38c8..215d879378d3d508cc48c24031559e0847fe6a2a 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 644d6f04ac0c7b3d7096ebe9fdc73d376b17fafe..98be80970975de49230eddfc590bf70d8acdab15 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 6d0f14ef2932f0caf465b4536d66985eaac15254..01c21564c5ba0306f09a94d01990d853aebbbdd8 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 a429feccfb7e509528b795e5f7ad1c70971c09c0..c44c6420a69741886815cb11b9918db7c5d6d91b 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 9e7a25f5e77e24560205568ba1c135fcd2ca91ff..bc704d9aff85a465a8487f8a017f99d7aa27d89c 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 1fced4600159098dfae9a3c922e04b149660707f..f5fcf7a06c63718a0b6579890329c93aa8bd3cbc 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 c6c4aea9024c27fcc1c5ee313ca22765afee76c4..1c9eaded0c8c030d453c9fd38a4190d11c3af7bc 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 6c01c21fd74573af61c929d6257ffaa1f1526bfc..70d4eae7bdbe44e557bec3f12d9ce4d77039242d 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 8acfac2c4118ae76f68f363d01f00159e02e04f9..571b69385c5639fe5bb38d577d60008eaa3d2a57 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 d5fbe3ceb34e50ae49066ec615102ccff27b3431..bd65e4f84b953491adada0d6221678af38717da8 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 517c8278b6173200f7c93d86dbd098e0451cde83..6aa07fb3db50375242c6ac5aa15059e4da519e70 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 3e04b3cc71674441815e291dae3d6f580cf4586b..16ce5f8cd32e61edf8cef1729c30a7edf29bb071 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 a7de6191a45e32d95a96bfde962081c2891b47a3..1eaaad8e96fc4bbf1bc7e815c5b4d46cf972dda1 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 7c127424f77fc006e54230fd5e7abc64082dea8c..e5b9dd948406dda7d7afcce2265d5e44cd141000 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 d8de93ab774f70888507f918447b42ee953ef630..45dbca154969f3bac5effe926ab303310ca23b84 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 fbb77dc8f382e5a240869aa2077f18f8ae189a4c..e802427c601e40b1b4eeb7ef6856a121ecb1a95c 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 4ebeee5d6fd5b6dd95f5cfae3566d546f6309d49..b5634288f233739fedc9be6bd5dec3559e9baeeb 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 deac525af17167369ab275ee795379f594063fb7..4ea0b53bd503ca343f00b7c6f9689cf370169bf5 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 393b1fe4bbd3e01a353013158fd7fa781ec5b43c..6323f1df659d5f8bdc4864ea3df9fd88baaf82b2 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 077c491e09d49f168473218fe708ada72019603c..0ed07fbc0a0a8afe4b639d1362cc5b105abc03fa 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 dc77652fe8aca5987123df298c40b60bbce751f3..e5f7444b98fb8a0837da940ca1c21336b408a49d 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 08b7e3e2ea7e4d22cfa1b736084949d33a47ce4e..16161c9cb1c6158c791a9b46cc5172a0ea7408a0 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 898aa91752d5add3109cfbdf907146ed35899e2b..03c07ce530de8a48580272ac3c2155469cbcfe55 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 1bf34b0323bf8baac99ab562ccc3513a382e48d0..42566220d5d69d264641db8d1bf62dd0646e98ee 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 88d16de1deeba5df7c136dcfafbd11488634c85f..881955062350cf37604281d06a9a254ccc404f1d 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 29b62f4e98e2f9b65ebece8b0f1fd727a9e897e3..102849ee97ee354ea52df363fefce0d6aae4350b 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);