diff --git a/src/plugins/wp/tests/wp_usage/valinit.i b/src/plugins/wp/tests/wp_usage/valinit.i index 55ceb6bffe652ad1494c3a27867601e2ad97d3d4..35a4884a6e6ef220c0078c1dd7e96937d3a8c7b5 100644 --- a/src/plugins/wp/tests/wp_usage/valinit.i +++ b/src/plugins/wp/tests/wp_usage/valinit.i @@ -6,19 +6,24 @@ DONTRUN: */ -int x0, y0, z0, *p0; +int x0, y0; +const int z0 = 0; +int *p0; int x1=1, y1=1, z1=z0, *q0=(int*)0, *q1=&y0, *p1=&y1; struct s { int c; int* cp; } ; -int a0, a1; -struct s s0, v0, w0; -struct s s1=s0; +int a0; +const int a1 = 1; +struct s s0={0,(int*)0}; +struct s v0; +struct s w0={0,(int*)0}; +struct s s1={0,(int*)0}; struct s s2={1,(int*)0}; struct s s3={1,&a0}; struct s s4={a1,(int*)0}; struct s s5={1,&v0.c}; -struct s s6={w0.c,(int*)0}; +struct s s6={0,(int*)0}; void f(void) { diff --git a/tests/cil/oracle/bts892.res.oracle b/tests/cil/oracle/bts892.res.oracle index 9ec093e1f4930ae0df5e869fc9dc0a8572e98326..f9a9a310578a588b9be8231ceed0d87a1146977b 100644 --- a/tests/cil/oracle/bts892.res.oracle +++ b/tests/cil/oracle/bts892.res.oracle @@ -1,5 +1,7 @@ [kernel] Parsing bts892.i (no preprocessing) [kernel] bts892.i:17: User Error: Forbidden access to local variable i in static initializer +[kernel] bts892.i:17: User Error: + Initializer element is not a compile-time constant [kernel] User Error: stopping on file "bts892.i" that has errors. [kernel] Frama-C aborted: invalid user input. diff --git a/tests/constant_propagation/bts-1787.i b/tests/constant_propagation/bts-1787.i index 6b534ca4bbdf3057ce5a0049bf682f69faff46eb..5fa026433e9ac44636ade94d789481fcdb9c7f2b 100644 --- a/tests/constant_propagation/bts-1787.i +++ b/tests/constant_propagation/bts-1787.i @@ -7,7 +7,7 @@ typedef struct { int s; } S1_t; -typedef struct { +typedef struct { const S1_t* p1; S1_t* p2; S1_t* p3; @@ -27,7 +27,7 @@ static S2_t const G2 = { void g(S2_t const* q) { S1_t *s1 = (S1_t *)(q->p1); /* incorrect to inline because of const qualifier */ (*(q->p3)).s = (*(q->p1)).s + (*(q->p2)).s ; - // (*(q->p1)).s += (*(q->p1)).s; /* statement to be rejected by the C typechecker */ + // (*(q->p1)).s += (*(q->p1)).s; /* statement to be rejected by the C typechecker */ s1->s = 3; } @@ -39,5 +39,5 @@ int main(int c) { g(&G2); return G1.c3.s; } -int a = 0; +const int a = 0; int b = a; diff --git a/tests/constant_propagation/oracle/bts-1787.0.res.oracle b/tests/constant_propagation/oracle/bts-1787.0.res.oracle index e9f8f0700a6dca77f6113a9584d3a2ceddfbfcb2..c48284fa8e0e5f97ba9f882064a548c764497fc4 100644 --- a/tests/constant_propagation/oracle/bts-1787.0.res.oracle +++ b/tests/constant_propagation/oracle/bts-1787.0.res.oracle @@ -53,7 +53,7 @@ int main(int c) return __retres; } -int a = 0; +int const a = 0; int b = a; [scf] constant propagation done diff --git a/tests/constant_propagation/oracle/bts-1787.1.res.oracle b/tests/constant_propagation/oracle/bts-1787.1.res.oracle index e9f8f0700a6dca77f6113a9584d3a2ceddfbfcb2..c48284fa8e0e5f97ba9f882064a548c764497fc4 100644 --- a/tests/constant_propagation/oracle/bts-1787.1.res.oracle +++ b/tests/constant_propagation/oracle/bts-1787.1.res.oracle @@ -53,7 +53,7 @@ int main(int c) return __retres; } -int a = 0; +int const a = 0; int b = a; [scf] constant propagation done diff --git a/tests/syntax/conflict.c b/tests/syntax/conflict.c new file mode 100644 index 0000000000000000000000000000000000000000..dc85f0d78bd1efdb13bc1438f43fc44569db9b1e --- /dev/null +++ b/tests/syntax/conflict.c @@ -0,0 +1,18 @@ +const int a[1] = { 0 }; +int b = a[0]; + +struct stru { + const int c; +}; + +const struct stru d = { 0 }; + +int e = d.c; + +struct stru2 { + int f; +}; + +const struct stru2 g = { 0 }; + +int h = g.f; diff --git a/tests/syntax/ghost_cv_incompat.i b/tests/syntax/ghost_cv_incompat.i index e75186e231c116379b922093101c28ba321fbdfa..89ede27d8fe60412eb3ca078e5af2b7e4a47f699 100644 --- a/tests/syntax/ghost_cv_incompat.i +++ b/tests/syntax/ghost_cv_incompat.i @@ -23,12 +23,12 @@ void def_not_ghost(void) /*@ ghost (int * p) */ {} // int ng ; -//@ ghost int * gl_gp ; +//@ ghost int * const gl_gp = 0; //@ ghost int \ghost * gl_gpg_1 = &ng ; // error: address of non-ghost integer into pointer to ghost //@ ghost int \ghost * gl_gpg_2 = gl_gp ; // error: pointer to a non-ghost location into pointer to ghost -int *gl_p00, *gl_p01 ; +int * const gl_p00 = 0; int * const gl_p01 = 0 ; // error: we transform pointer to non-ghost into pointer to ghosts //@ ghost int \ghost * gl_array[3] = { gl_p00, gl_p00, gl_p01 }; @@ -100,7 +100,7 @@ void call_ng_to_g(void){ // //@ ghost int g ; -//@ ghost int \ghost * gl_gpg ; +//@ ghost int \ghost * const gl_gpg = 0; //@ ghost int * gl_gp_1 = &g ; // error: address of ghost integer into pointer to non-ghost //@ ghost int * gl_gp_2 = gl_gpg ; // error: pointer to a ghost location into pointer to non-ghost diff --git a/tests/syntax/ghost_cv_var_decl.c b/tests/syntax/ghost_cv_var_decl.c index c407d427b9c4feaaa9c790338a47b8aa8f7da522..b8193afe7da955d98d0ead50c9146d690df4b988 100644 --- a/tests/syntax/ghost_cv_var_decl.c +++ b/tests/syntax/ghost_cv_var_decl.c @@ -240,7 +240,7 @@ void reference_functions(){ //@ ghost int x ; int i ; -int * p ; +int * const p = &i; //@ ghost int * gp1 = &i ; //@ ghost int * gp2 = p ; diff --git a/tests/syntax/ko_global.c b/tests/syntax/ko_global.c new file mode 100644 index 0000000000000000000000000000000000000000..2c61e443df6b3d5166f35a10186bc786e8626a20 --- /dev/null +++ b/tests/syntax/ko_global.c @@ -0,0 +1,41 @@ +/* run.config + EXIT: 1 + STDOPT: +*/ + +int * const a; +int * b = a; + +struct stru { + const int c; +}; + +struct stru d = { 0 }; + +int e = d.c; + +const int f = f; + +int g = g; + +int h = (int) &h; + +const int i; +int j = i; + +int k = 1; +int l = k; + +struct stru2 { + int m; +}; + +int n = 1; +struct stru2 o = { n }; + +union unio2 { + int p; +}; + +int q = 1; +union unio2 r = {q}; diff --git a/tests/syntax/merge_loc.i b/tests/syntax/merge_loc.i index 2a93071ea4d794e47a457e2eb32bbca80ddade3f..ed787d3174c9f76065795e4ac716b99774a4dcd8 100644 --- a/tests/syntax/merge_loc.i +++ b/tests/syntax/merge_loc.i @@ -20,4 +20,4 @@ extern int baz; extern int baz; -int z = (int) &baz; +long z = (long) &baz; diff --git a/tests/syntax/ok_globals.c b/tests/syntax/ok_globals.c new file mode 100644 index 0000000000000000000000000000000000000000..712226b32adb9549dd0f17437d0a146f1c911bdd --- /dev/null +++ b/tests/syntax/ok_globals.c @@ -0,0 +1,34 @@ +const int a = 0; +const int b = 1; +int c = a + b; + +int d = (int) ((int*)3+5); + +const int e = 42; +int f = (int) ((int*)e); + +union uty { + int g; + float h; +}; + +const int i = 1; +union uty j = {i}; + +int k; +int l = sizeof(k); + +int m; +int n = sizeof((int) &m); + +struct sty { + int o; +}; + +const int o = 1; +struct sty p = { o }; + +int q; +unsigned long r = (unsigned long) &q; + +long s = (long) &s; diff --git a/tests/syntax/oracle/conflict.res.oracle b/tests/syntax/oracle/conflict.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..c6efc60b067cd8c106f9281e4ad7b573f739e0b5 --- /dev/null +++ b/tests/syntax/oracle/conflict.res.oracle @@ -0,0 +1,15 @@ +[kernel] Parsing conflict.c (with preprocessing) +/* Generated by Frama-C */ +struct stru { + int const c ; +}; +struct stru2 { + int f ; +}; +int const a[1] = {0}; +int b = a[0]; +struct stru const d = {.c = 0}; +int e = d.c; +struct stru2 const g = {.f = 0}; +int h = g.f; + diff --git a/tests/syntax/oracle/ko_global.res.oracle b/tests/syntax/oracle/ko_global.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..204f067a98c9e43a28e94eeca8b36ecd7581e598 --- /dev/null +++ b/tests/syntax/oracle/ko_global.res.oracle @@ -0,0 +1,11 @@ +[kernel] Parsing ko_global.c (with preprocessing) +[kernel] ko_global.c:7: User Error: a is not a compile-time constant +[kernel] ko_global.c:17: User Error: f is not a compile-time constant +[kernel] ko_global.c:19: User Error: g is not a compile-time constant +[kernel] ko_global.c:24: User Error: i is not a compile-time constant +[kernel] ko_global.c:27: User Error: k is not a compile-time constant +[kernel] ko_global.c:34: User Error: n is not a compile-time constant +[kernel] ko_global.c:41: User Error: q is not a compile-time constant +[kernel] User Error: stopping on file "ko_global.c" that has errors. Add '-kernel-msg-key pp' + for preprocessing command. +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/merge_loc.res.oracle b/tests/syntax/oracle/merge_loc.res.oracle index 9bf94a39b9416e64ec39f835a1d4d7476f809a5b..c80e91140f9ed8e5041a02c0feed29e406670d65 100644 --- a/tests/syntax/oracle/merge_loc.res.oracle +++ b/tests/syntax/oracle/merge_loc.res.oracle @@ -12,5 +12,5 @@ extern int baz; //#line 23 "merge_loc.i" -int z = (int)(& baz); +long z = (long)(& baz); diff --git a/tests/syntax/oracle/ok_globals.res.oracle b/tests/syntax/oracle/ok_globals.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..f614876f4d1b8db31029adcdde09b697f72cbe5a --- /dev/null +++ b/tests/syntax/oracle/ok_globals.res.oracle @@ -0,0 +1,27 @@ +[kernel] Parsing ok_globals.c (with preprocessing) +/* Generated by Frama-C */ +union uty { + int g ; + float h ; +}; +struct sty { + int o ; +}; +int const a = 0; +int const b = 1; +int c = a + b; +int d = (int)((int *)3 + 5); +int const e = 42; +int f = (int)((int *)e); +int const i = 1; +union uty j = {.g = i}; +int k; +int l = (int)sizeof(k); +int m; +int n = (int)sizeof((int)(& m)); +int const o = 1; +struct sty p = {.o = o}; +int q; +unsigned long r = (unsigned long)(& q); +long s = (long)(& s); + diff --git a/tests/value/from_call.i b/tests/value/from_call.i index 7e979f0b83d058231cb0c433e14b7f9528d06077..ff5f6045e01a6e21c252c47bb95e2e928698434e 100644 --- a/tests/value/from_call.i +++ b/tests/value/from_call.i @@ -67,9 +67,9 @@ int access_tab(int ind) } int AA,AR,AS; -int At[2]={(int)&AA}; -int Ar[2]={(int)&AA}; -int *Ap=At; +long At[2]={(long)&AA}; +long Ar[2]={(long)&AA}; +long *Ap=At; /*@ assigns AR \from Ap[..] ; assigns AS \from Ar[..] ; diff --git a/tests/value/non_iso_initializer.i b/tests/value/non_iso_initializer.i index c7059e95a9abaae748580c553986cba5b9db09cd..27bf94c012b7369459bcea9c91efbba78d7fc117 100644 --- a/tests/value/non_iso_initializer.i +++ b/tests/value/non_iso_initializer.i @@ -1,5 +1,5 @@ -int G0 = 42; -int G1 = G0>>1; +const int G0 = 42; +const int G1 = G0>>1; int G2 = G0 ^ G1 ; int G3 = -1; void main (void) { diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle index 101005bed38dbefde5ee3959f528076e5d542172..e8e374f9be8208104d40d0e6b79b78640bde6635 100644 --- a/tests/value/oracle/from_call.0.res.oracle +++ b/tests/value/oracle/from_call.0.res.oracle @@ -36,9 +36,9 @@ AA ∈ {0} AR ∈ {0} AS ∈ {0} - At[0] ∈ {{ (int)&AA }} + At[0] ∈ {{ (long)&AA }} [1] ∈ {0} - Ar[0] ∈ {{ (int)&AA }} + Ar[0] ∈ {{ (long)&AA }} [1] ∈ {0} Ap ∈ {{ &At[0] }} f_previous ∈ {{ &a }} diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle index 14097263afd44b7dd97bc7fa346a82925f1cd965..60886fe4c870b421d9f775f05ff32df1fb96e7a1 100644 --- a/tests/value/oracle/from_call.1.res.oracle +++ b/tests/value/oracle/from_call.1.res.oracle @@ -36,9 +36,9 @@ AA ∈ {0} AR ∈ {0} AS ∈ {0} - At[0] ∈ {{ (int)&AA }} + At[0] ∈ {{ (long)&AA }} [1] ∈ {0} - Ar[0] ∈ {{ (int)&AA }} + Ar[0] ∈ {{ (long)&AA }} [1] ∈ {0} Ap ∈ {{ &At[0] }} f_previous ∈ {{ &a }} diff --git a/tests/value/oracle/struct_array.res.oracle b/tests/value/oracle/struct_array.res.oracle index 5d52686c112607372e4c0fc385c3550a1d6e73cf..e3c8fe1473c06e3b5a1878987aa6244889eb08d6 100644 --- a/tests/value/oracle/struct_array.res.oracle +++ b/tests/value/oracle/struct_array.res.oracle @@ -21,11 +21,11 @@ [0].b ∈ {2} [0].pp ∈ {0} [0].p ∈ {{ &x }} - [1].a ∈ {{ (int)&z1 }} - [1].b ∈ {{ (int)&z2 }} + [1].a ∈ {{ (long)&z1 }} + [1].b ∈ {{ (long)&z2 }} [1].pp ∈ {{ &z3 }} [1].p ∈ {{ &y }} - [2].a ∈ {{ (int)&z4 }} + [2].a ∈ {{ (long)&z4 }} [2].b ∈ {2} [2].pp ∈ {0} [2].p ∈ {{ &x }} @@ -260,11 +260,11 @@ [0].b ∈ {2} [0].pp ∈ {0} [0].p ∈ {{ &x }} - [1].a ∈ {{ (int)&z1 }} - [1].b ∈ {{ (int)&z2 }} + [1].a ∈ {{ (long)&z1 }} + [1].b ∈ {{ (long)&z2 }} [1].pp ∈ {{ &z3 }} [1].p ∈ {{ &y }} - [2].a ∈ {{ (int)&z4 }} + [2].a ∈ {{ (long)&z4 }} [2].b ∈ {2} [2].pp ∈ {0} [2].p ∈ {{ &x }} diff --git a/tests/value/struct_array.i b/tests/value/struct_array.i index cfe0e9ab48851779b00a9a9d50ac6d8f47cab6b8..898aa91752d5add3109cfbdf907146ed35899e2b 100644 --- a/tests/value/struct_array.i +++ b/tests/value/struct_array.i @@ -5,14 +5,14 @@ volatile v; struct st1 { - int a; - int b; + long a; + long b; int *pp; int *p; }; int *outp; int x,y,z1,z2,z3,z4; -struct st1 T[22] = { {1,2,0,&x}, {(int)&z1,(int)&z2,&z3,&y},{(int)&z4,2,0,&x},{1,2,0,&x} }; +struct st1 T[22] = { {1,2,0,&x}, {(long)&z1,(long)&z2,&z3,&y},{(long)&z4,2,0,&x},{1,2,0,&x} }; struct S { int a;