diff --git a/.gitignore b/.gitignore
index ab10834be6..0b63894459 100644
--- a/.gitignore
+++ b/.gitignore
@@ -62,6 +62,15 @@ compcert/doc/html/
 compcert/extraction/
 compcert/test/
 
+progs/alias
+progs/alias.compcert.c
+progs/alias.i
+progs/alias.parsed.c
+progs64/alias
+progs64/alias.compcert.c
+progs64/alias.i
+progs64/alias.parsed.c
+
 *.vo
 *.vos
 *.vok
diff --git a/Makefile b/Makefile
index e9fc375d3b..2cfd43c9b7 100644
--- a/Makefile
+++ b/Makefile
@@ -499,7 +499,8 @@ PROGS32_FILES= \
   libglob.v verif_libglob.v peel.v verif_peel.v \
   printf.v stackframe_demo.v verif_stackframe_demo.v \
 	rotate.v verif_rotate.v \
-  verif_objectSelf.v verif_objectSelfFancy.v verif_objectSelfFancyOverriding.v
+  verif_objectSelf.v verif_objectSelfFancy.v verif_objectSelfFancyOverriding.v \
+  alias.v verif_alias.v
 # verif_insertion_sort.v
 
 C64_ORDINARY = reverse.c revarray.c sumarray.c append.c bin_search.c \
@@ -513,7 +514,8 @@ V64_ORDINARY = verif_reverse2.v verif_revarray.v verif_sumarray.v \
     verif_bst.v verif_field_loadstore.v verif_float.v verif_object.v \
     verif_global.v verif_min.v verif_min64.v verif_nest2.v verif_nest3.v \
     verif_logical_compare.v \
-    verif_strlib.v verif_switch.v verif_union.v verif_message.v verif_incr.v
+    verif_strlib.v verif_switch.v verif_union.v verif_message.v verif_incr.v \
+    alias.v verif_alias.v
 
 SHA_FILES= \
   general_lemmas.v SHA256.v common_lemmas.v pure_lemmas.v sha_lemmas.v functional_prog.v \
diff --git a/progs/alias.c b/progs/alias.c
new file mode 100644
index 0000000000..5748b7de52
--- /dev/null
+++ b/progs/alias.c
@@ -0,0 +1,77 @@
+long foo(long *p, void **q) {
+  *p = 1;
+  *q = 0;
+  return *p;
+}
+int main() {
+  long x;
+  return foo(&x, &x);
+}
+
+/*
+The usage in this canonical example is essential to systems programming but has
+undefined behavior according to ISO C due to the strict aliasing restriction.
+
+From the perspective that pointers are addresses and memory maps addresses to
+bytes, we have two writes and one read of the same 4-byte memory region, and
+main returns 0. Yet ISO C17 § 6.5.7 limits the lvalue types through which the
+value of a declared object can be accessed to a fixed list of variations on the
+declared type plus char. Here the declared type is long, so the modification
+through *p is consistent with these rules, but the modification through *q (of
+type void*) is not, even though long and void* have the same size and alignment.
+The ubiquitous compiler flag -fno-strict-aliasing lifts these restrictions.
+
+VST is proved sound only for CompCert, which always uses -fno-strict-aliasing.
+While VST also enforces many other additional requirements of the C standard,
+it is not sound for use with other compilers without -fno-strict-aliasing.
+
+To show that this complication is relevant in practice, the example was tested
+using clang 14.0.6, gcc 12.2.0, and CompCert a1f01c84 (3.11++).
+
+It returns 0 in the following invocations:
+
+clang -m32 -O0 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -O0 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -O1 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O1 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O2 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O3 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -fno-strict-aliasing -O2 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -fno-strict-aliasing -O3 -w alias.c -o alias && ./alias; echo $?
+
+It also returns 0 with CompCert:
+
+../../CompCert/ccomp alias.c -c alias.o && gcc -m32 alias.o -o alias && ./alias; echo $?
+../../CompCert/ccomp -interp alias.c
+
+It returns 1 in the following invocations:
+
+clang -m32 -O1 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -O2 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -O3 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -O2 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -O3 -w alias.c -o alias && ./alias; echo $?
+
+alias.v was generated using the following invocation:
+
+../../CompCert/clightgen -dclight -normalize -nostdinc -P -std=c11 alias.c
+
+The corresponding clight file returns 0 in all invocations where the input file returned 0:
+
+clang -m32 -O0 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -O0 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O2 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O3 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -fno-strict-aliasing -O2 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -fno-strict-aliasing -O3 -w alias.light.c -o alias && ./alias; echo $?
+
+... and returns 1 in all invocations where the input file returned 1:
+
+clang -m32 -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -O2 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -O3 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -O2 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -O3 -w alias.light.c -o alias && ./alias; echo $?
+*/
diff --git a/progs/alias.light.c b/progs/alias.light.c
new file mode 100644
index 0000000000..2b87ed581f
--- /dev/null
+++ b/progs/alias.light.c
@@ -0,0 +1,41 @@
+extern unsigned int __compcert_va_int32(void *);
+extern unsigned long long __compcert_va_int64(void *);
+extern double __compcert_va_float64(void *);
+extern void *__compcert_va_composite(void *, unsigned int);
+extern long long __compcert_i64_dtos(double);
+extern unsigned long long __compcert_i64_dtou(double);
+extern double __compcert_i64_stod(long long);
+extern double __compcert_i64_utod(unsigned long long);
+extern float __compcert_i64_stof(long long);
+extern float __compcert_i64_utof(unsigned long long);
+extern long long __compcert_i64_sdiv(long long, long long);
+extern unsigned long long __compcert_i64_udiv(unsigned long long, unsigned long long);
+extern long long __compcert_i64_smod(long long, long long);
+extern unsigned long long __compcert_i64_umod(unsigned long long, unsigned long long);
+extern long long __compcert_i64_shl(long long, int);
+extern unsigned long long __compcert_i64_shr(unsigned long long, int);
+extern long long __compcert_i64_sar(long long, int);
+extern long long __compcert_i64_smulh(long long, long long);
+extern unsigned long long __compcert_i64_umulh(unsigned long long, unsigned long long);
+extern void __builtin_debug(int, ...);
+int foo(int *, void **);
+int main(void);
+int foo(int *$p, void **$q)
+{
+  register int $128;
+  *$p = 1;
+  *$q = 0;
+  $128 = *$p;
+  return $128;
+}
+
+int main(void)
+{
+  int x;
+  register int $128;
+  $128 = foo(&x, &x);
+  return $128;
+  return 0;
+}
+
+
diff --git a/progs/alias.v b/progs/alias.v
new file mode 100644
index 0000000000..ec5b54ac71
--- /dev/null
+++ b/progs/alias.v
@@ -0,0 +1,420 @@
+From Coq Require Import String List ZArith.
+From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.
+Import Clightdefs.ClightNotations.
+Local Open Scope Z_scope.
+Local Open Scope string_scope.
+Local Open Scope clight_scope.
+
+Module Info.
+  Definition version := "3.11".
+  Definition build_number := "".
+  Definition build_tag := "".
+  Definition build_branch := "".
+  Definition arch := "x86".
+  Definition model := "32sse2".
+  Definition abi := "standard".
+  Definition bitsize := 32.
+  Definition big_endian := false.
+  Definition source_file := "alias.c".
+  Definition normalized := true.
+End Info.
+
+Definition ___builtin_ais_annot : ident := $"__builtin_ais_annot".
+Definition ___builtin_annot : ident := $"__builtin_annot".
+Definition ___builtin_annot_intval : ident := $"__builtin_annot_intval".
+Definition ___builtin_bswap : ident := $"__builtin_bswap".
+Definition ___builtin_bswap16 : ident := $"__builtin_bswap16".
+Definition ___builtin_bswap32 : ident := $"__builtin_bswap32".
+Definition ___builtin_bswap64 : ident := $"__builtin_bswap64".
+Definition ___builtin_clz : ident := $"__builtin_clz".
+Definition ___builtin_clzl : ident := $"__builtin_clzl".
+Definition ___builtin_clzll : ident := $"__builtin_clzll".
+Definition ___builtin_ctz : ident := $"__builtin_ctz".
+Definition ___builtin_ctzl : ident := $"__builtin_ctzl".
+Definition ___builtin_ctzll : ident := $"__builtin_ctzll".
+Definition ___builtin_debug : ident := $"__builtin_debug".
+Definition ___builtin_expect : ident := $"__builtin_expect".
+Definition ___builtin_fabs : ident := $"__builtin_fabs".
+Definition ___builtin_fabsf : ident := $"__builtin_fabsf".
+Definition ___builtin_fmadd : ident := $"__builtin_fmadd".
+Definition ___builtin_fmax : ident := $"__builtin_fmax".
+Definition ___builtin_fmin : ident := $"__builtin_fmin".
+Definition ___builtin_fmsub : ident := $"__builtin_fmsub".
+Definition ___builtin_fnmadd : ident := $"__builtin_fnmadd".
+Definition ___builtin_fnmsub : ident := $"__builtin_fnmsub".
+Definition ___builtin_fsqrt : ident := $"__builtin_fsqrt".
+Definition ___builtin_membar : ident := $"__builtin_membar".
+Definition ___builtin_memcpy_aligned : ident := $"__builtin_memcpy_aligned".
+Definition ___builtin_read16_reversed : ident := $"__builtin_read16_reversed".
+Definition ___builtin_read32_reversed : ident := $"__builtin_read32_reversed".
+Definition ___builtin_sel : ident := $"__builtin_sel".
+Definition ___builtin_sqrt : ident := $"__builtin_sqrt".
+Definition ___builtin_unreachable : ident := $"__builtin_unreachable".
+Definition ___builtin_va_arg : ident := $"__builtin_va_arg".
+Definition ___builtin_va_copy : ident := $"__builtin_va_copy".
+Definition ___builtin_va_end : ident := $"__builtin_va_end".
+Definition ___builtin_va_start : ident := $"__builtin_va_start".
+Definition ___builtin_write16_reversed : ident := $"__builtin_write16_reversed".
+Definition ___builtin_write32_reversed : ident := $"__builtin_write32_reversed".
+Definition ___compcert_i64_dtos : ident := $"__compcert_i64_dtos".
+Definition ___compcert_i64_dtou : ident := $"__compcert_i64_dtou".
+Definition ___compcert_i64_sar : ident := $"__compcert_i64_sar".
+Definition ___compcert_i64_sdiv : ident := $"__compcert_i64_sdiv".
+Definition ___compcert_i64_shl : ident := $"__compcert_i64_shl".
+Definition ___compcert_i64_shr : ident := $"__compcert_i64_shr".
+Definition ___compcert_i64_smod : ident := $"__compcert_i64_smod".
+Definition ___compcert_i64_smulh : ident := $"__compcert_i64_smulh".
+Definition ___compcert_i64_stod : ident := $"__compcert_i64_stod".
+Definition ___compcert_i64_stof : ident := $"__compcert_i64_stof".
+Definition ___compcert_i64_udiv : ident := $"__compcert_i64_udiv".
+Definition ___compcert_i64_umod : ident := $"__compcert_i64_umod".
+Definition ___compcert_i64_umulh : ident := $"__compcert_i64_umulh".
+Definition ___compcert_i64_utod : ident := $"__compcert_i64_utod".
+Definition ___compcert_i64_utof : ident := $"__compcert_i64_utof".
+Definition ___compcert_va_composite : ident := $"__compcert_va_composite".
+Definition ___compcert_va_float64 : ident := $"__compcert_va_float64".
+Definition ___compcert_va_int32 : ident := $"__compcert_va_int32".
+Definition ___compcert_va_int64 : ident := $"__compcert_va_int64".
+Definition _foo : ident := $"foo".
+Definition _main : ident := $"main".
+Definition _p : ident := $"p".
+Definition _q : ident := $"q".
+Definition _x : ident := $"x".
+Definition _t'1 : ident := 128%positive.
+
+Definition f_foo := {|
+  fn_return := tint;
+  fn_callconv := cc_default;
+  fn_params := ((_p, (tptr tint)) :: (_q, (tptr (tptr tvoid))) :: nil);
+  fn_vars := nil;
+  fn_temps := ((_t'1, tint) :: nil);
+  fn_body :=
+(Ssequence
+  (Sassign (Ederef (Etempvar _p (tptr tint)) tint)
+    (Econst_int (Int.repr 1) tint))
+  (Ssequence
+    (Sassign (Ederef (Etempvar _q (tptr (tptr tvoid))) (tptr tvoid))
+      (Econst_int (Int.repr 0) tint))
+    (Ssequence
+      (Sset _t'1 (Ederef (Etempvar _p (tptr tint)) tint))
+      (Sreturn (Some (Etempvar _t'1 tint))))))
+|}.
+
+Definition f_main := {|
+  fn_return := tint;
+  fn_callconv := cc_default;
+  fn_params := nil;
+  fn_vars := ((_x, tint) :: nil);
+  fn_temps := ((_t'1, tint) :: nil);
+  fn_body :=
+(Ssequence
+  (Ssequence
+    (Scall (Some _t'1)
+      (Evar _foo (Tfunction
+                   (Tcons (tptr tint) (Tcons (tptr (tptr tvoid)) Tnil)) tint
+                   cc_default))
+      ((Eaddrof (Evar _x tint) (tptr tint)) ::
+       (Eaddrof (Evar _x tint) (tptr tint)) :: nil))
+    (Sreturn (Some (Etempvar _t'1 tint))))
+  (Sreturn (Some (Econst_int (Int.repr 0) tint))))
+|}.
+
+Definition composites : list composite_definition :=
+nil.
+
+Definition global_definitions : list (ident * globdef fundef type) :=
+((___compcert_va_int32,
+   Gfun(External (EF_runtime "__compcert_va_int32"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons (tptr tvoid) Tnil) tuint cc_default)) ::
+ (___compcert_va_int64,
+   Gfun(External (EF_runtime "__compcert_va_int64"
+                   (mksignature (AST.Tint :: nil) AST.Tlong cc_default))
+     (Tcons (tptr tvoid) Tnil) tulong cc_default)) ::
+ (___compcert_va_float64,
+   Gfun(External (EF_runtime "__compcert_va_float64"
+                   (mksignature (AST.Tint :: nil) AST.Tfloat cc_default))
+     (Tcons (tptr tvoid) Tnil) tdouble cc_default)) ::
+ (___compcert_va_composite,
+   Gfun(External (EF_runtime "__compcert_va_composite"
+                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint
+                     cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
+     (tptr tvoid) cc_default)) ::
+ (___compcert_i64_dtos,
+   Gfun(External (EF_runtime "__compcert_i64_dtos"
+                   (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default))
+     (Tcons tdouble Tnil) tlong cc_default)) ::
+ (___compcert_i64_dtou,
+   Gfun(External (EF_runtime "__compcert_i64_dtou"
+                   (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default))
+     (Tcons tdouble Tnil) tulong cc_default)) ::
+ (___compcert_i64_stod,
+   Gfun(External (EF_runtime "__compcert_i64_stod"
+                   (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default))
+     (Tcons tlong Tnil) tdouble cc_default)) ::
+ (___compcert_i64_utod,
+   Gfun(External (EF_runtime "__compcert_i64_utod"
+                   (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default))
+     (Tcons tulong Tnil) tdouble cc_default)) ::
+ (___compcert_i64_stof,
+   Gfun(External (EF_runtime "__compcert_i64_stof"
+                   (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default))
+     (Tcons tlong Tnil) tfloat cc_default)) ::
+ (___compcert_i64_utof,
+   Gfun(External (EF_runtime "__compcert_i64_utof"
+                   (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default))
+     (Tcons tulong Tnil) tfloat cc_default)) ::
+ (___compcert_i64_sdiv,
+   Gfun(External (EF_runtime "__compcert_i64_sdiv"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_udiv,
+   Gfun(External (EF_runtime "__compcert_i64_udiv"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
+     cc_default)) ::
+ (___compcert_i64_smod,
+   Gfun(External (EF_runtime "__compcert_i64_smod"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_umod,
+   Gfun(External (EF_runtime "__compcert_i64_umod"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
+     cc_default)) ::
+ (___compcert_i64_shl,
+   Gfun(External (EF_runtime "__compcert_i64_shl"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_shr,
+   Gfun(External (EF_runtime "__compcert_i64_shr"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
+                     cc_default)) (Tcons tulong (Tcons tint Tnil)) tulong
+     cc_default)) ::
+ (___compcert_i64_sar,
+   Gfun(External (EF_runtime "__compcert_i64_sar"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_smulh,
+   Gfun(External (EF_runtime "__compcert_i64_smulh"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_umulh,
+   Gfun(External (EF_runtime "__compcert_i64_umulh"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
+     cc_default)) ::
+ (___builtin_ais_annot,
+   Gfun(External (EF_builtin "__builtin_ais_annot"
+                   (mksignature (AST.Tint :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons (tptr tschar) Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
+ (___builtin_bswap64,
+   Gfun(External (EF_builtin "__builtin_bswap64"
+                   (mksignature (AST.Tlong :: nil) AST.Tlong cc_default))
+     (Tcons tulong Tnil) tulong cc_default)) ::
+ (___builtin_bswap,
+   Gfun(External (EF_builtin "__builtin_bswap"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tuint cc_default)) ::
+ (___builtin_bswap32,
+   Gfun(External (EF_builtin "__builtin_bswap32"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tuint cc_default)) ::
+ (___builtin_bswap16,
+   Gfun(External (EF_builtin "__builtin_bswap16"
+                   (mksignature (AST.Tint :: nil) AST.Tint16unsigned
+                     cc_default)) (Tcons tushort Tnil) tushort cc_default)) ::
+ (___builtin_clz,
+   Gfun(External (EF_builtin "__builtin_clz"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tint cc_default)) ::
+ (___builtin_clzl,
+   Gfun(External (EF_builtin "__builtin_clzl"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tint cc_default)) ::
+ (___builtin_clzll,
+   Gfun(External (EF_builtin "__builtin_clzll"
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons tulong Tnil) tint cc_default)) ::
+ (___builtin_ctz,
+   Gfun(External (EF_builtin "__builtin_ctz"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tint cc_default)) ::
+ (___builtin_ctzl,
+   Gfun(External (EF_builtin "__builtin_ctzl"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tint cc_default)) ::
+ (___builtin_ctzll,
+   Gfun(External (EF_builtin "__builtin_ctzll"
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons tulong Tnil) tint cc_default)) ::
+ (___builtin_fabs,
+   Gfun(External (EF_builtin "__builtin_fabs"
+                   (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default))
+     (Tcons tdouble Tnil) tdouble cc_default)) ::
+ (___builtin_fabsf,
+   Gfun(External (EF_builtin "__builtin_fabsf"
+                   (mksignature (AST.Tsingle :: nil) AST.Tsingle cc_default))
+     (Tcons tfloat Tnil) tfloat cc_default)) ::
+ (___builtin_fsqrt,
+   Gfun(External (EF_builtin "__builtin_fsqrt"
+                   (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default))
+     (Tcons tdouble Tnil) tdouble cc_default)) ::
+ (___builtin_sqrt,
+   Gfun(External (EF_builtin "__builtin_sqrt"
+                   (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default))
+     (Tcons tdouble Tnil) tdouble cc_default)) ::
+ (___builtin_memcpy_aligned,
+   Gfun(External (EF_builtin "__builtin_memcpy_aligned"
+                   (mksignature
+                     (AST.Tint :: AST.Tint :: AST.Tint :: AST.Tint :: nil)
+                     AST.Tvoid cc_default))
+     (Tcons (tptr tvoid)
+       (Tcons (tptr tvoid) (Tcons tuint (Tcons tuint Tnil)))) tvoid
+     cc_default)) ::
+ (___builtin_sel,
+   Gfun(External (EF_builtin "__builtin_sel"
+                   (mksignature (AST.Tint :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons tbool Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
+ (___builtin_annot,
+   Gfun(External (EF_builtin "__builtin_annot"
+                   (mksignature (AST.Tint :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons (tptr tschar) Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
+ (___builtin_annot_intval,
+   Gfun(External (EF_builtin "__builtin_annot_intval"
+                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint
+                     cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil))
+     tint cc_default)) ::
+ (___builtin_membar,
+   Gfun(External (EF_builtin "__builtin_membar"
+                   (mksignature nil AST.Tvoid cc_default)) Tnil tvoid
+     cc_default)) ::
+ (___builtin_va_start,
+   Gfun(External (EF_builtin "__builtin_va_start"
+                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
+     (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
+ (___builtin_va_arg,
+   Gfun(External (EF_builtin "__builtin_va_arg"
+                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                     cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
+     tvoid cc_default)) ::
+ (___builtin_va_copy,
+   Gfun(External (EF_builtin "__builtin_va_copy"
+                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                     cc_default))
+     (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) ::
+ (___builtin_va_end,
+   Gfun(External (EF_builtin "__builtin_va_end"
+                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
+     (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
+ (___builtin_unreachable,
+   Gfun(External (EF_builtin "__builtin_unreachable"
+                   (mksignature nil AST.Tvoid cc_default)) Tnil tvoid
+     cc_default)) ::
+ (___builtin_expect,
+   Gfun(External (EF_builtin "__builtin_expect"
+                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint
+                     cc_default)) (Tcons tint (Tcons tint Tnil)) tint
+     cc_default)) ::
+ (___builtin_fmax,
+   Gfun(External (EF_builtin "__builtin_fmax"
+                   (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat
+                     cc_default)) (Tcons tdouble (Tcons tdouble Tnil))
+     tdouble cc_default)) ::
+ (___builtin_fmin,
+   Gfun(External (EF_builtin "__builtin_fmin"
+                   (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat
+                     cc_default)) (Tcons tdouble (Tcons tdouble Tnil))
+     tdouble cc_default)) ::
+ (___builtin_fmadd,
+   Gfun(External (EF_builtin "__builtin_fmadd"
+                   (mksignature
+                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
+                     AST.Tfloat cc_default))
+     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
+     cc_default)) ::
+ (___builtin_fmsub,
+   Gfun(External (EF_builtin "__builtin_fmsub"
+                   (mksignature
+                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
+                     AST.Tfloat cc_default))
+     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
+     cc_default)) ::
+ (___builtin_fnmadd,
+   Gfun(External (EF_builtin "__builtin_fnmadd"
+                   (mksignature
+                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
+                     AST.Tfloat cc_default))
+     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
+     cc_default)) ::
+ (___builtin_fnmsub,
+   Gfun(External (EF_builtin "__builtin_fnmsub"
+                   (mksignature
+                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
+                     AST.Tfloat cc_default))
+     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
+     cc_default)) ::
+ (___builtin_read16_reversed,
+   Gfun(External (EF_builtin "__builtin_read16_reversed"
+                   (mksignature (AST.Tint :: nil) AST.Tint16unsigned
+                     cc_default)) (Tcons (tptr tushort) Tnil) tushort
+     cc_default)) ::
+ (___builtin_read32_reversed,
+   Gfun(External (EF_builtin "__builtin_read32_reversed"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons (tptr tuint) Tnil) tuint cc_default)) ::
+ (___builtin_write16_reversed,
+   Gfun(External (EF_builtin "__builtin_write16_reversed"
+                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                     cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil))
+     tvoid cc_default)) ::
+ (___builtin_write32_reversed,
+   Gfun(External (EF_builtin "__builtin_write32_reversed"
+                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                     cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil))
+     tvoid cc_default)) ::
+ (___builtin_debug,
+   Gfun(External (EF_external "__builtin_debug"
+                   (mksignature (AST.Tint :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons tint Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
+ (_foo, Gfun(Internal f_foo)) :: (_main, Gfun(Internal f_main)) :: nil).
+
+Definition public_idents : list ident :=
+(_main :: _foo :: ___builtin_debug :: ___builtin_write32_reversed ::
+ ___builtin_write16_reversed :: ___builtin_read32_reversed ::
+ ___builtin_read16_reversed :: ___builtin_fnmsub :: ___builtin_fnmadd ::
+ ___builtin_fmsub :: ___builtin_fmadd :: ___builtin_fmin ::
+ ___builtin_fmax :: ___builtin_expect :: ___builtin_unreachable ::
+ ___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg ::
+ ___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval ::
+ ___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned ::
+ ___builtin_sqrt :: ___builtin_fsqrt :: ___builtin_fabsf ::
+ ___builtin_fabs :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz ::
+ ___builtin_clzll :: ___builtin_clzl :: ___builtin_clz ::
+ ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap ::
+ ___builtin_bswap64 :: ___builtin_ais_annot :: ___compcert_i64_umulh ::
+ ___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr ::
+ ___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod ::
+ ___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof ::
+ ___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod ::
+ ___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite ::
+ ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 ::
+ nil).
+
+Definition prog : Clight.program := 
+  mkprogram composites global_definitions public_idents _main Logic.I.
+
+
diff --git a/progs/verif_alias.v b/progs/verif_alias.v
new file mode 100644
index 0000000000..5e56a8f079
--- /dev/null
+++ b/progs/verif_alias.v
@@ -0,0 +1,64 @@
+Require Import VST.floyd.proofauto.
+Require Import VST.progs.alias.
+
+Lemma field_compatible_void_int cs p : @field_compatible cs (tptr Tvoid) [] p = @field_compatible cs tint [] p.
+Proof.
+  eapply PropExtensionality.propositional_extensionality.
+  destruct p;
+  cbv [field_compatible align_compatible size_compatible];
+  intuition idtac;
+  repeat match goal with
+         | H : align_compatible_rec _ _ _ |- _ => inversion H; clear H; subst end.
+  all : econstructor; eauto.
+Qed.
+
+Lemma data_at__void_int cs sh p : @data_at_ cs sh (tptr Tvoid) p = @data_at_ cs sh tint p.
+Proof. rewrite 2data_at__memory_block, field_compatible_void_int; trivial. Qed.
+
+Lemma data_at_void_int_null cs sh p : @data_at cs sh (tptr Tvoid) (Vint Int.zero) p = @data_at cs sh tint (Vint Int.zero) p.
+Proof.
+  cbv [data_at field_at at_offset nested_field_type tptr].
+  simpl data_at_rec.
+  unfold data_at_rec.
+  simpl rank_type.
+  simpl type_induction.type_func.
+  rewrite field_compatible_void_int; f_equal.
+  change (Tint I32 Signed noattr) with tint.
+  erewrite mapsto_null_mapsto_pointer; reflexivity.
+Qed.
+
+
+#[export] Instance CompSpecs : compspecs.
+Proof. make_compspecs prog. Defined.
+Definition Vprog : varspecs. mk_varspecs prog. Defined.
+
+Definition foo_spec := DECLARE _foo WITH p : val
+  PRE [ tptr tint, tptr (tptr Tvoid) ] PROP() PARAMS(p; p) SEP(data_at_ Tsh tint p)
+  POST [ tint ] PROP() RETURN(Vint Int.zero) SEP(data_at_ Tsh tint p).
+
+Definition main_spec := DECLARE _main WITH gv : globals
+  PRE  [] main_pre prog tt gv
+  POST [ tint ] PROP() RETURN (Vint Int.zero) SEP(has_ext tt).
+
+Definition Gprog : funspecs := ltac:(with_library prog [foo_spec; main_spec]).
+
+Lemma body_main : semax_body Vprog Gprog f_main main_spec.
+Proof. start_function. forward_call. forward. entailer!. Qed.
+
+Lemma body_foo : semax_body Vprog Gprog f_foo foo_spec.
+Proof.
+  start_function.
+  forward.
+  match goal with | |- context[data_at ?sh ?t ?Vs ?op] => sep_apply (data_at_data_at_ sh t Vs op) end.
+  erewrite <-data_at__void_int.
+  forward.
+  rewrite data_at_void_int_null.
+  forward.
+  forward.
+  entailer!.
+Qed.
+
+Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog prog) Gprog.
+#[export] Existing Instance Espec.
+Lemma prog_correct: semax_prog prog tt Vprog Gprog.
+Proof. prove_semax_prog. semax_func_cons body_foo. semax_func_cons body_main. Qed.
diff --git a/progs64/alias.c b/progs64/alias.c
new file mode 100644
index 0000000000..a99f9f0c7e
--- /dev/null
+++ b/progs64/alias.c
@@ -0,0 +1,77 @@
+long foo(long *p, void **q) {
+  *p = 1;
+  *q = 0;
+  return *p;
+}
+int main() {
+  long x;
+  return foo(&x, &x);
+}
+
+/*
+The usage in this canonical example is essential to systems programming but has
+undefined behavior according to ISO C due to the strict aliasing restriction.
+
+From the perspective that pointers are addresses and memory maps addresses to
+bytes, we have two writes and one read of the same 8-byte memory region, and
+main returns 0. Yet ISO C17 § 6.5.7 limits the lvalue types through which the
+value of a declared object can be accessed to a fixed list of variations on the
+declared type plus char. Here the declared type is long, so the modification
+through *p is consistent with these rules, but the modification through *q (of
+type void*) is not, even though long and void* have the same size and alignment.
+The ubiquitous compiler flag -fno-strict-aliasing lifts these restrictions.
+
+VST is proved sound only for CompCert, which always uses -fno-strict-aliasing.
+While VST also enforces many other additional requirements of the C standard,
+it is not sound for use with other compilers without -fno-strict-aliasing.
+
+To show that this complication is relevant in practice, the example was tested
+using clang 14.0.6, gcc 12.2.0, and CompCert a1f01c84 (3.11++).
+
+It returns 0 in the following invocations:
+
+clang -O0 -w alias.c -o alias && ./alias; echo $?
+gcc   -O0 -w alias.c -o alias && ./alias; echo $?
+gcc   -O1 -w alias.c -o alias && ./alias; echo $?
+clang -fno-strict-aliasing -O1 -w alias.c -o alias && ./alias; echo $?
+clang -fno-strict-aliasing -O2 -w alias.c -o alias && ./alias; echo $?
+clang -fno-strict-aliasing -O3 -w alias.c -o alias && ./alias; echo $?
+gcc   -fno-strict-aliasing -O2 -w alias.c -o alias && ./alias; echo $?
+gcc   -fno-strict-aliasing -O3 -w alias.c -o alias && ./alias; echo $?
+
+It also returns 0 with CompCert:
+
+../../CompCert/ccomp alias.c -c alias.o && gcc alias.o -o alias && ./alias; echo $?
+../../CompCert/ccomp -interp alias.c
+
+It returns 1 in the following invocations:
+
+clang -O1 -w alias.c -o alias && ./alias; echo $?
+clang -O2 -w alias.c -o alias && ./alias; echo $?
+clang -O3 -w alias.c -o alias && ./alias; echo $?
+gcc   -O2 -w alias.c -o alias && ./alias; echo $?
+gcc   -O3 -w alias.c -o alias && ./alias; echo $?
+
+alias.v was generated using the following invocation:
+
+../../CompCert/clightgen -dclight -normalize -nostdinc -P -std=c11 alias.c
+
+The corresponding clight file returns 0 in all invocations where the input file returned 0:
+
+clang -O0 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -O0 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -fno-strict-aliasing -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -fno-strict-aliasing -O2 -w alias.light.c -o alias && ./alias; echo $?
+clang -fno-strict-aliasing -O3 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -fno-strict-aliasing -O2 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -fno-strict-aliasing -O3 -w alias.light.c -o alias && ./alias; echo $?
+
+... and returns 1 in all invocations where the input file returned 1:
+
+clang -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -O2 -w alias.light.c -o alias && ./alias; echo $?
+clang -O3 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -O2 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -O3 -w alias.light.c -o alias && ./alias; echo $?
+*/
diff --git a/progs64/alias.light.c b/progs64/alias.light.c
new file mode 100644
index 0000000000..c536a4bc9a
--- /dev/null
+++ b/progs64/alias.light.c
@@ -0,0 +1,41 @@
+extern unsigned int __compcert_va_int32(void *);
+extern unsigned long long __compcert_va_int64(void *);
+extern double __compcert_va_float64(void *);
+extern void *__compcert_va_composite(void *, unsigned long long);
+extern long long __compcert_i64_dtos(double);
+extern unsigned long long __compcert_i64_dtou(double);
+extern double __compcert_i64_stod(long long);
+extern double __compcert_i64_utod(unsigned long long);
+extern float __compcert_i64_stof(long long);
+extern float __compcert_i64_utof(unsigned long long);
+extern long long __compcert_i64_sdiv(long long, long long);
+extern unsigned long long __compcert_i64_udiv(unsigned long long, unsigned long long);
+extern long long __compcert_i64_smod(long long, long long);
+extern unsigned long long __compcert_i64_umod(unsigned long long, unsigned long long);
+extern long long __compcert_i64_shl(long long, int);
+extern unsigned long long __compcert_i64_shr(unsigned long long, int);
+extern long long __compcert_i64_sar(long long, int);
+extern long long __compcert_i64_smulh(long long, long long);
+extern unsigned long long __compcert_i64_umulh(unsigned long long, unsigned long long);
+extern void __builtin_debug(int, ...);
+long long foo(long long *, void **);
+int main(void);
+long long foo(long long *$p, void **$q)
+{
+  register long long $128;
+  *$p = 1;
+  *$q = 0;
+  $128 = *$p;
+  return $128;
+}
+
+int main(void)
+{
+  long long x;
+  register long long $128;
+  $128 = foo(&x, &x);
+  return $128;
+  return 0;
+}
+
+
diff --git a/progs64/alias.v b/progs64/alias.v
new file mode 100644
index 0000000000..942f95c4f4
--- /dev/null
+++ b/progs64/alias.v
@@ -0,0 +1,420 @@
+From Coq Require Import String List ZArith.
+From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.
+Import Clightdefs.ClightNotations.
+Local Open Scope Z_scope.
+Local Open Scope string_scope.
+Local Open Scope clight_scope.
+
+Module Info.
+  Definition version := "3.11".
+  Definition build_number := "".
+  Definition build_tag := "".
+  Definition build_branch := "".
+  Definition arch := "x86".
+  Definition model := "64".
+  Definition abi := "standard".
+  Definition bitsize := 64.
+  Definition big_endian := false.
+  Definition source_file := "alias.c".
+  Definition normalized := true.
+End Info.
+
+Definition ___builtin_ais_annot : ident := $"__builtin_ais_annot".
+Definition ___builtin_annot : ident := $"__builtin_annot".
+Definition ___builtin_annot_intval : ident := $"__builtin_annot_intval".
+Definition ___builtin_bswap : ident := $"__builtin_bswap".
+Definition ___builtin_bswap16 : ident := $"__builtin_bswap16".
+Definition ___builtin_bswap32 : ident := $"__builtin_bswap32".
+Definition ___builtin_bswap64 : ident := $"__builtin_bswap64".
+Definition ___builtin_clz : ident := $"__builtin_clz".
+Definition ___builtin_clzl : ident := $"__builtin_clzl".
+Definition ___builtin_clzll : ident := $"__builtin_clzll".
+Definition ___builtin_ctz : ident := $"__builtin_ctz".
+Definition ___builtin_ctzl : ident := $"__builtin_ctzl".
+Definition ___builtin_ctzll : ident := $"__builtin_ctzll".
+Definition ___builtin_debug : ident := $"__builtin_debug".
+Definition ___builtin_expect : ident := $"__builtin_expect".
+Definition ___builtin_fabs : ident := $"__builtin_fabs".
+Definition ___builtin_fabsf : ident := $"__builtin_fabsf".
+Definition ___builtin_fmadd : ident := $"__builtin_fmadd".
+Definition ___builtin_fmax : ident := $"__builtin_fmax".
+Definition ___builtin_fmin : ident := $"__builtin_fmin".
+Definition ___builtin_fmsub : ident := $"__builtin_fmsub".
+Definition ___builtin_fnmadd : ident := $"__builtin_fnmadd".
+Definition ___builtin_fnmsub : ident := $"__builtin_fnmsub".
+Definition ___builtin_fsqrt : ident := $"__builtin_fsqrt".
+Definition ___builtin_membar : ident := $"__builtin_membar".
+Definition ___builtin_memcpy_aligned : ident := $"__builtin_memcpy_aligned".
+Definition ___builtin_read16_reversed : ident := $"__builtin_read16_reversed".
+Definition ___builtin_read32_reversed : ident := $"__builtin_read32_reversed".
+Definition ___builtin_sel : ident := $"__builtin_sel".
+Definition ___builtin_sqrt : ident := $"__builtin_sqrt".
+Definition ___builtin_unreachable : ident := $"__builtin_unreachable".
+Definition ___builtin_va_arg : ident := $"__builtin_va_arg".
+Definition ___builtin_va_copy : ident := $"__builtin_va_copy".
+Definition ___builtin_va_end : ident := $"__builtin_va_end".
+Definition ___builtin_va_start : ident := $"__builtin_va_start".
+Definition ___builtin_write16_reversed : ident := $"__builtin_write16_reversed".
+Definition ___builtin_write32_reversed : ident := $"__builtin_write32_reversed".
+Definition ___compcert_i64_dtos : ident := $"__compcert_i64_dtos".
+Definition ___compcert_i64_dtou : ident := $"__compcert_i64_dtou".
+Definition ___compcert_i64_sar : ident := $"__compcert_i64_sar".
+Definition ___compcert_i64_sdiv : ident := $"__compcert_i64_sdiv".
+Definition ___compcert_i64_shl : ident := $"__compcert_i64_shl".
+Definition ___compcert_i64_shr : ident := $"__compcert_i64_shr".
+Definition ___compcert_i64_smod : ident := $"__compcert_i64_smod".
+Definition ___compcert_i64_smulh : ident := $"__compcert_i64_smulh".
+Definition ___compcert_i64_stod : ident := $"__compcert_i64_stod".
+Definition ___compcert_i64_stof : ident := $"__compcert_i64_stof".
+Definition ___compcert_i64_udiv : ident := $"__compcert_i64_udiv".
+Definition ___compcert_i64_umod : ident := $"__compcert_i64_umod".
+Definition ___compcert_i64_umulh : ident := $"__compcert_i64_umulh".
+Definition ___compcert_i64_utod : ident := $"__compcert_i64_utod".
+Definition ___compcert_i64_utof : ident := $"__compcert_i64_utof".
+Definition ___compcert_va_composite : ident := $"__compcert_va_composite".
+Definition ___compcert_va_float64 : ident := $"__compcert_va_float64".
+Definition ___compcert_va_int32 : ident := $"__compcert_va_int32".
+Definition ___compcert_va_int64 : ident := $"__compcert_va_int64".
+Definition _foo : ident := $"foo".
+Definition _main : ident := $"main".
+Definition _p : ident := $"p".
+Definition _q : ident := $"q".
+Definition _x : ident := $"x".
+Definition _t'1 : ident := 128%positive.
+
+Definition f_foo := {|
+  fn_return := tlong;
+  fn_callconv := cc_default;
+  fn_params := ((_p, (tptr tlong)) :: (_q, (tptr (tptr tvoid))) :: nil);
+  fn_vars := nil;
+  fn_temps := ((_t'1, tlong) :: nil);
+  fn_body :=
+(Ssequence
+  (Sassign (Ederef (Etempvar _p (tptr tlong)) tlong)
+    (Econst_int (Int.repr 1) tint))
+  (Ssequence
+    (Sassign (Ederef (Etempvar _q (tptr (tptr tvoid))) (tptr tvoid))
+      (Econst_int (Int.repr 0) tint))
+    (Ssequence
+      (Sset _t'1 (Ederef (Etempvar _p (tptr tlong)) tlong))
+      (Sreturn (Some (Etempvar _t'1 tlong))))))
+|}.
+
+Definition f_main := {|
+  fn_return := tint;
+  fn_callconv := cc_default;
+  fn_params := nil;
+  fn_vars := ((_x, tlong) :: nil);
+  fn_temps := ((_t'1, tlong) :: nil);
+  fn_body :=
+(Ssequence
+  (Ssequence
+    (Scall (Some _t'1)
+      (Evar _foo (Tfunction
+                   (Tcons (tptr tlong) (Tcons (tptr (tptr tvoid)) Tnil))
+                   tlong cc_default))
+      ((Eaddrof (Evar _x tlong) (tptr tlong)) ::
+       (Eaddrof (Evar _x tlong) (tptr tlong)) :: nil))
+    (Sreturn (Some (Etempvar _t'1 tlong))))
+  (Sreturn (Some (Econst_int (Int.repr 0) tint))))
+|}.
+
+Definition composites : list composite_definition :=
+nil.
+
+Definition global_definitions : list (ident * globdef fundef type) :=
+((___compcert_va_int32,
+   Gfun(External (EF_runtime "__compcert_va_int32"
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons (tptr tvoid) Tnil) tuint cc_default)) ::
+ (___compcert_va_int64,
+   Gfun(External (EF_runtime "__compcert_va_int64"
+                   (mksignature (AST.Tlong :: nil) AST.Tlong cc_default))
+     (Tcons (tptr tvoid) Tnil) tulong cc_default)) ::
+ (___compcert_va_float64,
+   Gfun(External (EF_runtime "__compcert_va_float64"
+                   (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default))
+     (Tcons (tptr tvoid) Tnil) tdouble cc_default)) ::
+ (___compcert_va_composite,
+   Gfun(External (EF_runtime "__compcert_va_composite"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons (tptr tvoid) (Tcons tulong Tnil))
+     (tptr tvoid) cc_default)) ::
+ (___compcert_i64_dtos,
+   Gfun(External (EF_runtime "__compcert_i64_dtos"
+                   (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default))
+     (Tcons tdouble Tnil) tlong cc_default)) ::
+ (___compcert_i64_dtou,
+   Gfun(External (EF_runtime "__compcert_i64_dtou"
+                   (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default))
+     (Tcons tdouble Tnil) tulong cc_default)) ::
+ (___compcert_i64_stod,
+   Gfun(External (EF_runtime "__compcert_i64_stod"
+                   (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default))
+     (Tcons tlong Tnil) tdouble cc_default)) ::
+ (___compcert_i64_utod,
+   Gfun(External (EF_runtime "__compcert_i64_utod"
+                   (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default))
+     (Tcons tulong Tnil) tdouble cc_default)) ::
+ (___compcert_i64_stof,
+   Gfun(External (EF_runtime "__compcert_i64_stof"
+                   (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default))
+     (Tcons tlong Tnil) tfloat cc_default)) ::
+ (___compcert_i64_utof,
+   Gfun(External (EF_runtime "__compcert_i64_utof"
+                   (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default))
+     (Tcons tulong Tnil) tfloat cc_default)) ::
+ (___compcert_i64_sdiv,
+   Gfun(External (EF_runtime "__compcert_i64_sdiv"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_udiv,
+   Gfun(External (EF_runtime "__compcert_i64_udiv"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
+     cc_default)) ::
+ (___compcert_i64_smod,
+   Gfun(External (EF_runtime "__compcert_i64_smod"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_umod,
+   Gfun(External (EF_runtime "__compcert_i64_umod"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
+     cc_default)) ::
+ (___compcert_i64_shl,
+   Gfun(External (EF_runtime "__compcert_i64_shl"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_shr,
+   Gfun(External (EF_runtime "__compcert_i64_shr"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
+                     cc_default)) (Tcons tulong (Tcons tint Tnil)) tulong
+     cc_default)) ::
+ (___compcert_i64_sar,
+   Gfun(External (EF_runtime "__compcert_i64_sar"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_smulh,
+   Gfun(External (EF_runtime "__compcert_i64_smulh"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
+     cc_default)) ::
+ (___compcert_i64_umulh,
+   Gfun(External (EF_runtime "__compcert_i64_umulh"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
+     cc_default)) ::
+ (___builtin_ais_annot,
+   Gfun(External (EF_builtin "__builtin_ais_annot"
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons (tptr tschar) Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
+ (___builtin_bswap64,
+   Gfun(External (EF_builtin "__builtin_bswap64"
+                   (mksignature (AST.Tlong :: nil) AST.Tlong cc_default))
+     (Tcons tulong Tnil) tulong cc_default)) ::
+ (___builtin_bswap,
+   Gfun(External (EF_builtin "__builtin_bswap"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tuint cc_default)) ::
+ (___builtin_bswap32,
+   Gfun(External (EF_builtin "__builtin_bswap32"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tuint cc_default)) ::
+ (___builtin_bswap16,
+   Gfun(External (EF_builtin "__builtin_bswap16"
+                   (mksignature (AST.Tint :: nil) AST.Tint16unsigned
+                     cc_default)) (Tcons tushort Tnil) tushort cc_default)) ::
+ (___builtin_clz,
+   Gfun(External (EF_builtin "__builtin_clz"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tint cc_default)) ::
+ (___builtin_clzl,
+   Gfun(External (EF_builtin "__builtin_clzl"
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons tulong Tnil) tint cc_default)) ::
+ (___builtin_clzll,
+   Gfun(External (EF_builtin "__builtin_clzll"
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons tulong Tnil) tint cc_default)) ::
+ (___builtin_ctz,
+   Gfun(External (EF_builtin "__builtin_ctz"
+                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+     (Tcons tuint Tnil) tint cc_default)) ::
+ (___builtin_ctzl,
+   Gfun(External (EF_builtin "__builtin_ctzl"
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons tulong Tnil) tint cc_default)) ::
+ (___builtin_ctzll,
+   Gfun(External (EF_builtin "__builtin_ctzll"
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons tulong Tnil) tint cc_default)) ::
+ (___builtin_fabs,
+   Gfun(External (EF_builtin "__builtin_fabs"
+                   (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default))
+     (Tcons tdouble Tnil) tdouble cc_default)) ::
+ (___builtin_fabsf,
+   Gfun(External (EF_builtin "__builtin_fabsf"
+                   (mksignature (AST.Tsingle :: nil) AST.Tsingle cc_default))
+     (Tcons tfloat Tnil) tfloat cc_default)) ::
+ (___builtin_fsqrt,
+   Gfun(External (EF_builtin "__builtin_fsqrt"
+                   (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default))
+     (Tcons tdouble Tnil) tdouble cc_default)) ::
+ (___builtin_sqrt,
+   Gfun(External (EF_builtin "__builtin_sqrt"
+                   (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default))
+     (Tcons tdouble Tnil) tdouble cc_default)) ::
+ (___builtin_memcpy_aligned,
+   Gfun(External (EF_builtin "__builtin_memcpy_aligned"
+                   (mksignature
+                     (AST.Tlong :: AST.Tlong :: AST.Tlong :: AST.Tlong ::
+                      nil) AST.Tvoid cc_default))
+     (Tcons (tptr tvoid)
+       (Tcons (tptr tvoid) (Tcons tulong (Tcons tulong Tnil)))) tvoid
+     cc_default)) ::
+ (___builtin_sel,
+   Gfun(External (EF_builtin "__builtin_sel"
+                   (mksignature (AST.Tint :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons tbool Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
+ (___builtin_annot,
+   Gfun(External (EF_builtin "__builtin_annot"
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons (tptr tschar) Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
+ (___builtin_annot_intval,
+   Gfun(External (EF_builtin "__builtin_annot_intval"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tint
+                     cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil))
+     tint cc_default)) ::
+ (___builtin_membar,
+   Gfun(External (EF_builtin "__builtin_membar"
+                   (mksignature nil AST.Tvoid cc_default)) Tnil tvoid
+     cc_default)) ::
+ (___builtin_va_start,
+   Gfun(External (EF_builtin "__builtin_va_start"
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
+     (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
+ (___builtin_va_arg,
+   Gfun(External (EF_builtin "__builtin_va_arg"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid
+                     cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
+     tvoid cc_default)) ::
+ (___builtin_va_copy,
+   Gfun(External (EF_builtin "__builtin_va_copy"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tvoid
+                     cc_default))
+     (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) ::
+ (___builtin_va_end,
+   Gfun(External (EF_builtin "__builtin_va_end"
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
+     (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
+ (___builtin_unreachable,
+   Gfun(External (EF_builtin "__builtin_unreachable"
+                   (mksignature nil AST.Tvoid cc_default)) Tnil tvoid
+     cc_default)) ::
+ (___builtin_expect,
+   Gfun(External (EF_builtin "__builtin_expect"
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
+     cc_default)) ::
+ (___builtin_fmax,
+   Gfun(External (EF_builtin "__builtin_fmax"
+                   (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat
+                     cc_default)) (Tcons tdouble (Tcons tdouble Tnil))
+     tdouble cc_default)) ::
+ (___builtin_fmin,
+   Gfun(External (EF_builtin "__builtin_fmin"
+                   (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat
+                     cc_default)) (Tcons tdouble (Tcons tdouble Tnil))
+     tdouble cc_default)) ::
+ (___builtin_fmadd,
+   Gfun(External (EF_builtin "__builtin_fmadd"
+                   (mksignature
+                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
+                     AST.Tfloat cc_default))
+     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
+     cc_default)) ::
+ (___builtin_fmsub,
+   Gfun(External (EF_builtin "__builtin_fmsub"
+                   (mksignature
+                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
+                     AST.Tfloat cc_default))
+     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
+     cc_default)) ::
+ (___builtin_fnmadd,
+   Gfun(External (EF_builtin "__builtin_fnmadd"
+                   (mksignature
+                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
+                     AST.Tfloat cc_default))
+     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
+     cc_default)) ::
+ (___builtin_fnmsub,
+   Gfun(External (EF_builtin "__builtin_fnmsub"
+                   (mksignature
+                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
+                     AST.Tfloat cc_default))
+     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
+     cc_default)) ::
+ (___builtin_read16_reversed,
+   Gfun(External (EF_builtin "__builtin_read16_reversed"
+                   (mksignature (AST.Tlong :: nil) AST.Tint16unsigned
+                     cc_default)) (Tcons (tptr tushort) Tnil) tushort
+     cc_default)) ::
+ (___builtin_read32_reversed,
+   Gfun(External (EF_builtin "__builtin_read32_reversed"
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons (tptr tuint) Tnil) tuint cc_default)) ::
+ (___builtin_write16_reversed,
+   Gfun(External (EF_builtin "__builtin_write16_reversed"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid
+                     cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil))
+     tvoid cc_default)) ::
+ (___builtin_write32_reversed,
+   Gfun(External (EF_builtin "__builtin_write32_reversed"
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid
+                     cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil))
+     tvoid cc_default)) ::
+ (___builtin_debug,
+   Gfun(External (EF_external "__builtin_debug"
+                   (mksignature (AST.Tint :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons tint Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
+ (_foo, Gfun(Internal f_foo)) :: (_main, Gfun(Internal f_main)) :: nil).
+
+Definition public_idents : list ident :=
+(_main :: _foo :: ___builtin_debug :: ___builtin_write32_reversed ::
+ ___builtin_write16_reversed :: ___builtin_read32_reversed ::
+ ___builtin_read16_reversed :: ___builtin_fnmsub :: ___builtin_fnmadd ::
+ ___builtin_fmsub :: ___builtin_fmadd :: ___builtin_fmin ::
+ ___builtin_fmax :: ___builtin_expect :: ___builtin_unreachable ::
+ ___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg ::
+ ___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval ::
+ ___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned ::
+ ___builtin_sqrt :: ___builtin_fsqrt :: ___builtin_fabsf ::
+ ___builtin_fabs :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz ::
+ ___builtin_clzll :: ___builtin_clzl :: ___builtin_clz ::
+ ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap ::
+ ___builtin_bswap64 :: ___builtin_ais_annot :: ___compcert_i64_umulh ::
+ ___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr ::
+ ___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod ::
+ ___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof ::
+ ___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod ::
+ ___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite ::
+ ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 ::
+ nil).
+
+Definition prog : Clight.program := 
+  mkprogram composites global_definitions public_idents _main Logic.I.
+
+
diff --git a/progs64/verif_alias.v b/progs64/verif_alias.v
new file mode 100644
index 0000000000..bf4e89906b
--- /dev/null
+++ b/progs64/verif_alias.v
@@ -0,0 +1,65 @@
+Require Import VST.floyd.proofauto.
+Require Import VST.progs64.alias.
+
+Lemma field_compatible_void_long cs p : @field_compatible cs (tptr Tvoid) [] p = @field_compatible cs tlong [] p.
+Proof.
+  eapply PropExtensionality.propositional_extensionality.
+  destruct p;
+  cbv [field_compatible align_compatible size_compatible];
+  intuition idtac;
+  repeat match goal with
+         | H : align_compatible_rec _ _ _ |- _ => inversion H; clear H; subst end.
+  all : econstructor; eauto.
+Qed.
+
+Lemma data_at__void_long cs sh p : @data_at_ cs sh (tptr Tvoid) p = @data_at_ cs sh tlong p.
+Proof. rewrite 2data_at__memory_block, field_compatible_void_long; trivial. Qed.
+
+Lemma data_at_void_long_null cs sh p : @data_at cs sh (tptr Tvoid) (Vlong Int64.zero) p = @data_at cs sh tlong (Vlong Int64.zero) p.
+Proof.
+  cbv [data_at field_at at_offset nested_field_type tptr].
+  simpl data_at_rec.
+  unfold data_at_rec.
+  simpl rank_type.
+  simpl type_induction.type_func.
+  rewrite field_compatible_void_long; f_equal.
+  change (Tlong Signed noattr) with tlong.
+  rewrite mapsto_tuint_tptr_nullval.
+  reflexivity.
+Qed.
+
+
+#[export] Instance CompSpecs : compspecs.
+Proof. make_compspecs prog. Defined.
+Definition Vprog : varspecs. mk_varspecs prog. Defined.
+
+Definition foo_spec := DECLARE _foo WITH p : val
+  PRE [ tptr tlong, tptr (tptr Tvoid) ] PROP() PARAMS(p; p) SEP(data_at_ Tsh tlong p)
+  POST [ tlong ] PROP() RETURN(Vlong Int64.zero) SEP(data_at_ Tsh tlong p).
+
+Definition main_spec := DECLARE _main WITH gv : globals
+  PRE  [] main_pre prog tt gv
+  POST [ tint ] PROP() RETURN (Vint Int.zero) SEP(has_ext tt).
+
+Definition Gprog : funspecs := ltac:(with_library prog [foo_spec; main_spec]).
+
+Lemma body_main : semax_body Vprog Gprog f_main main_spec.
+Proof. start_function. forward_call. forward. entailer!. Qed.
+
+Lemma body_foo : semax_body Vprog Gprog f_foo foo_spec.
+Proof.
+  start_function.
+  forward.
+  match goal with | |- context[data_at ?sh ?t ?Vs ?op] => sep_apply (data_at_data_at_ sh t Vs op) end.
+  erewrite <-data_at__void_long.
+  forward.
+  rewrite data_at_void_long_null.
+  forward.
+  forward.
+  entailer!.
+Qed.
+
+Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog prog) Gprog.
+#[export] Existing Instance Espec.
+Lemma prog_correct: semax_prog prog tt Vprog Gprog.
+Proof. prove_semax_prog. semax_func_cons body_foo. semax_func_cons body_main. Qed.