From be57ac44f2af8e5d9da63f6226785644e1ec425c Mon Sep 17 00:00:00 2001
From: Pierre Nigron <pierre.nigron@cea.fr>
Date: Tue, 18 Jul 2023 13:59:22 +0200
Subject: [PATCH] Tests + Oracles

---
 src/plugins/wp/tests/wp_usage/valinit.i       | 15 ++++---
 tests/cil/oracle/bts892.res.oracle            |  2 +
 tests/constant_propagation/bts-1787.i         |  6 +--
 .../oracle/bts-1787.0.res.oracle              |  2 +-
 .../oracle/bts-1787.1.res.oracle              |  2 +-
 tests/syntax/conflict.c                       | 18 ++++++++
 tests/syntax/ghost_cv_incompat.i              |  6 +--
 tests/syntax/ghost_cv_var_decl.c              |  2 +-
 tests/syntax/ko_global.c                      | 41 +++++++++++++++++++
 tests/syntax/merge_loc.i                      |  2 +-
 tests/syntax/ok_globals.c                     | 34 +++++++++++++++
 tests/syntax/oracle/conflict.res.oracle       | 15 +++++++
 tests/syntax/oracle/ko_global.res.oracle      | 11 +++++
 tests/syntax/oracle/merge_loc.res.oracle      |  2 +-
 tests/syntax/oracle/ok_globals.res.oracle     | 27 ++++++++++++
 tests/value/from_call.i                       |  6 +--
 tests/value/non_iso_initializer.i             |  4 +-
 tests/value/oracle/from_call.0.res.oracle     |  4 +-
 tests/value/oracle/from_call.1.res.oracle     |  4 +-
 tests/value/oracle/struct_array.res.oracle    | 12 +++---
 tests/value/struct_array.i                    |  6 +--
 21 files changed, 187 insertions(+), 34 deletions(-)
 create mode 100644 tests/syntax/conflict.c
 create mode 100644 tests/syntax/ko_global.c
 create mode 100644 tests/syntax/ok_globals.c
 create mode 100644 tests/syntax/oracle/conflict.res.oracle
 create mode 100644 tests/syntax/oracle/ko_global.res.oracle
 create mode 100644 tests/syntax/oracle/ok_globals.res.oracle

diff --git a/src/plugins/wp/tests/wp_usage/valinit.i b/src/plugins/wp/tests/wp_usage/valinit.i
index 55ceb6bffe6..35a4884a6e6 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 9ec093e1f49..f9a9a310578 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 6b534ca4bbd..5fa026433e9 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 e9f8f0700a6..c48284fa8e0 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 e9f8f0700a6..c48284fa8e0 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 00000000000..dc85f0d78bd
--- /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 e75186e231c..89ede27d8fe 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 c407d427b9c..b8193afe7da 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 00000000000..2c61e443df6
--- /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 2a93071ea4d..ed787d3174c 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 00000000000..712226b32ad
--- /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 00000000000..c6efc60b067
--- /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 00000000000..204f067a98c
--- /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 9bf94a39b94..c80e91140f9 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 00000000000..f614876f4d1
--- /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 7e979f0b83d..ff5f6045e01 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 c7059e95a9a..27bf94c012b 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 101005bed38..e8e374f9be8 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 14097263afd..60886fe4c87 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 5d52686c112..e3c8fe1473c 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 cfe0e9ab488..898aa91752d 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;
-- 
GitLab