Tests + Oracles

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) {

tests/cil/oracle/bts892.res.oracle

 [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.

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;

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

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

tests/syntax/conflict.c

+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;

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
 

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 ;

tests/syntax/ko_global.c

+/* 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};

tests/syntax/merge_loc.i

@@ -20,4 +20,4 @@ extern int baz;
 
 extern int baz;
 
-int z = (int) &baz;
+long z = (long) &baz;

tests/syntax/ok_globals.c

+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;

tests/syntax/oracle/conflict.res.oracle

+[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;
+

tests/syntax/oracle/ko_global.res.oracle

+[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.

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);
 

tests/syntax/oracle/ok_globals.res.oracle

+[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);
+

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[..] ;

tests/value/non_iso_initializer.i

-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) {

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 }}

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 }}

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 }}