diff --git a/opam b/opam
index ca6dd2be800bbd63a8293969fa83286e14ba63db..816adfb521400171d3ce556ddb8324f88a607059 100644
--- a/opam
+++ b/opam
@@ -53,6 +53,7 @@ authors: [
   "Melody Méaulle"
   "Benjamin Monate"
   "Yannick Moy"
+  "Pierre Nigron"
   "Anne Pacalet"
   "Valentin Perrelle"
   "Guillaume Petiot"
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b6422e8030749d9da9814f232e4a68fa14bc868f..a2393c647bb38c8130bafe1cb5283debbb3de66a 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -818,20 +818,7 @@ let get_formals vi =
 let initGlobals () =
   theFile := [];
   theFileTypes := [];
-  Cil_datatype.Varinfo.Hashtbl.clear theFileVars;
-;;
-
-let cabsPushGlobal (g: global) =
-  pushGlobal g ~types:theFileTypes ~variables:theFile;
-  (match g with
-   | GVar (vi, _, _) | GVarDecl (vi, _)
-   | GFun ({svar = vi}, _) | GFunDecl (_, vi, _) ->
-     (* Do 'add' and not 'replace' here, as we may store both
-        declarations and definitions for the same varinfo *)
-     Cil_datatype.Varinfo.Hashtbl.add theFileVars vi g
-   | _ -> ()
-  );
-;;
+  Cil_datatype.Varinfo.Hashtbl.clear theFileVars
 
 
 (* Keep track of some variable ids that must be turned into definitions. We
@@ -845,6 +832,8 @@ let mustTurnIntoDef: bool IH.t = IH.create 117
 (* Globals that have already been defined. Indexed by the variable name. *)
 let alreadyDefined: (string, location) H.t = H.create 117
 
+let isDefined vi = H.mem alreadyDefined vi.vorig_name
+
 (* Globals that were created due to static local variables. We chose their
  * names to be distinct from any global encountered at the time. But we might
  * see a global with conflicting name later in the file. *)
@@ -876,6 +865,54 @@ let fileGlobals () =
   revonto (revonto [] !theFile) !theFileTypes
 
 
+class checkGlobal = object
+  inherit nopCilVisitor
+
+
+  method! vglob = function
+    | GVar _ -> DoChildren
+    | _ -> SkipChildren
+
+  method! vexpr exp =
+    begin
+      match exp.enode with
+      | SizeOfE _ ->
+        (* sizeOf doesn't depend on the definitions *)
+        ()
+      | _ ->
+        let problematic_var : string option ref = ref None in
+        let is_varinfo_cst vi =
+          let res = Cil.isConstType vi.vtype && isDefined vi in
+          if not res then problematic_var := Some vi.vorig_name;
+          res
+        in
+        if not(isConstant ~is_varinfo_cst exp)
+        then
+          match !problematic_var with
+          | Some name ->
+            Kernel.error ~once:true ~current:true
+              ("%s is not a compile-time constant") name
+          | None ->
+            Kernel.error ~once:true ~current:true
+              "Initializer element is not a compile-time constant";
+    end;
+    SkipChildren
+
+end
+
+let cabsPushGlobal (g: global) =
+  ignore (visitCilGlobal (new checkGlobal) g);
+  pushGlobal g ~types:theFileTypes ~variables:theFile;
+  (match g with
+   | GVar (vi, _, _) | GVarDecl (vi, _)
+   | GFun ({svar = vi}, _) | GFunDecl (_, vi, _) ->
+     (* Do 'add' and not 'replace' here, as we may store both
+        declarations and definitions for the same varinfo *)
+     Cil_datatype.Varinfo.Hashtbl.add theFileVars vi g
+   | _ -> ()
+  )
+
+
 (********* ENVIRONMENTS ***************)
 
 (* The environment is kept in two distinct data structures. A hash table maps
@@ -8899,9 +8936,9 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * C
         if vi.vstorage = Extern then
           vi.vstorage <- NoStorage;     (* equivalent and canonical *)
 
-        H.add alreadyDefined vi.vname (CurrentLoc.get ());
         IH.remove mustTurnIntoDef vi.vid;
         cabsPushGlobal (GVar(vi, {init = init}, CurrentLoc.get ()));
+        H.add alreadyDefined vi.vname (CurrentLoc.get ());
         vi
       end else begin
         if not (isFunctionType vi.vtype) &&
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d5a6b27c12b79ccb5cd9734b8c2f9e42164efc67..c3520bf16882dba358b2f0d1d0a857b41c3fa445 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -830,6 +830,7 @@ let id = Fun.id
 let alphabetabeta _ x = x
 let alphabetafalse _ _ = false
 let alphatrue _ = true
+let alphafalse _ = false
 
 module Extensions = struct
   let initialized = ref false
@@ -5802,32 +5803,53 @@ let isVariadicListType t = match unrollTypeSkel t with
   | TBuiltin_va_list _ -> true
   | _ -> false
 
-let rec isConstantGen f e = match e.enode with
+let rec isConstantGen lit_only is_varinfo_cst f e = match e.enode with
   | Const c -> f c
-  | UnOp (_, e, _) -> isConstantGen f e
-  | BinOp (_, e1, e2, _) -> isConstantGen f e1 && isConstantGen f e2
-  | Lval (Var vi, NoOffset) ->
-    (vi.vglob && isArrayType vi.vtype || isFunctionType vi.vtype)
+  | UnOp (_, e, _) -> isConstantGen lit_only is_varinfo_cst f e
+  | BinOp (_, e1, e2, _) ->
+    isConstantGen lit_only is_varinfo_cst f e1 &&
+    isConstantGen lit_only is_varinfo_cst f e2
+  | Lval (Var vi, _) ->
+    is_varinfo_cst vi ||
+    (vi.vglob && isArrayType vi.vtype) ||
+    isFunctionType vi.vtype
   | Lval _ -> false
   | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> true
   (* see ISO 6.6.6 *)
   | CastE(t,{ enode = Const(CReal _)}) when isIntegralType t -> true
-  | CastE (_, e) -> isConstantGen f e
-  | AddrOf (Var vi, off) | StartOf (Var vi, off)
-    -> vi.vglob && isConstantOffsetGen f off
-  | AddrOf (Mem e, off) | StartOf(Mem e, off)
-    -> isConstantGen f e && isConstantOffsetGen f off
-
-and isConstantOffsetGen f = function
+  | CastE(t, e) ->
+    begin
+      match t, typeOf e with
+      | TInt (i, _), TPtr _ ->
+        (* gcc/clang/ccomp consider a non-truncated pointer to be a constant.
+           If it is truncated, we check whether we already know its value. *)
+        bytesSizeOfInt theMachine.upointKind <= bytesSizeOfInt i ||
+        isConstantGen true is_varinfo_cst f e
+      | _ -> isConstantGen lit_only is_varinfo_cst f e
+    end
+  | AddrOf (Var vi, off) | StartOf (Var vi, off) ->
+    not lit_only &&
+    vi.vglob &&
+    isConstantOffsetGen lit_only is_varinfo_cst f off
+  | AddrOf (Mem e, off) | StartOf(Mem e, off) ->
+    isConstantGen lit_only is_varinfo_cst f e &&
+    isConstantOffsetGen lit_only is_varinfo_cst f off
+
+and isConstantOffsetGen lit_only is_varinfo_cst f = function
     NoOffset -> true
-  | Field(_fi, off) -> isConstantOffsetGen f off
-  | Index(e, off) -> isConstantGen f e && isConstantOffsetGen f off
-
-let isConstant e = isConstantGen alphatrue e
-let isConstantOffset o = isConstantOffsetGen alphatrue o
-
-let isIntegerConstant e =
-  isConstantGen
+  | Field(_fi, off) -> isConstantOffsetGen lit_only is_varinfo_cst f off
+  | Index(e, off) ->
+    isConstantGen lit_only is_varinfo_cst f e &&
+    isConstantOffsetGen lit_only is_varinfo_cst f off
+
+let isConstant ?(is_varinfo_cst = alphafalse) e =
+  isConstantGen false is_varinfo_cst alphatrue e
+let isConstantOffset ?(is_varinfo_cst = alphafalse) o =
+  isConstantOffsetGen false is_varinfo_cst alphatrue o
+
+let isIntegerConstant ?(is_varinfo_cst = alphafalse) e =
+  isConstantGen false
+    is_varinfo_cst
     (function
       | CInt64 _ | CChr _ | CEnum _ -> true
       | CStr _ | CWStr _ | CReal _ -> false)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 8b63fb51b24e9a757822fd9696bd9c9b00902fcc..92213780da74fc591c8a36209b7b0053ab2868b3 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -841,14 +841,26 @@ val kfloat: loc:location -> fkind -> float -> exp
     character or an integer constant *)
 val isInteger: exp -> Integer.t option
 
-(** True if the expression is a compile-time constant *)
-val isConstant: exp -> bool
+(** True if the expression is a compile-time constant.
+    [is_varinfo_cst] indicates whether a variable should
+    be considered as having a constant content. Defaults to
+    [false].
 
-(** True if the expression is a compile-time integer constant *)
-val isIntegerConstant: exp -> bool
+    @before Frama-C+dev [is_varinfo_cst] does not exist
+*)
+val isConstant: ?is_varinfo_cst:(varinfo -> bool) -> exp -> bool
+
+(** True if the expression is a compile-time integer constant
+
+    @before Frama-C+dev [is_varinfo_cst] does not exist
+*)
+val isIntegerConstant: ?is_varinfo_cst:(varinfo -> bool) -> exp -> bool
+
+(** True if the given offset contains only field names or constant indices.
 
-(** True if the given offset contains only field names or constant indices. *)
-val isConstantOffset: offset -> bool
+    @before Frama-C+dev [is_varinfo_cst] does not exist
+*)
+val isConstantOffset: ?is_varinfo_cst:(varinfo -> bool) -> offset -> bool
 
 (** True if the given expression is a (possibly cast'ed) integer or character
     constant with value zero *)
diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml
index d0e1fedf9ea17fd08e0c576e6348fef59e01418b..0ac0ab6798b22bfc04ea81c49090ad2190cd248a 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -56,6 +56,7 @@ let show main_ui =
     "Melody Méaulle";
     "Benjamin Monate";
     "Yannick Moy";
+    "Pierre Nigron";
     "Anne Pacalet";
     "Valentin Perrelle";
     "Guillaume Petiot";
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;