diff --git a/tests/libc/fc_builtins_in_ghost.c b/tests/libc/fc_builtins_in_ghost.c
new file mode 100644
index 0000000000000000000000000000000000000000..dee454a232e0ce38067c6fb0803d2e207ec8a788
--- /dev/null
+++ b/tests/libc/fc_builtins_in_ghost.c
@@ -0,0 +1,7 @@
+#include "__fc_builtin.h"
+
+int main(void){
+  int i ;
+  //@ ghost Frama_C_show_each(i);
+  //@ ghost int p = Frama_C_int_interval(0, 10);
+}
diff --git a/tests/libc/oracle/fc_builtins_in_ghost.res.oracle b/tests/libc/oracle/fc_builtins_in_ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0d46a02edf54ae25582fb34c1838da1810cdabd6
--- /dev/null
+++ b/tests/libc/oracle/fc_builtins_in_ghost.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing fc_builtins_in_ghost.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] fc_builtins_in_ghost.c:5: Frama_C_show_each: ⊥
+[eva] computing for function Frama_C_int_interval <- main.
+  Called from fc_builtins_in_ghost.c:6.
+[eva] using specification for function Frama_C_int_interval
+[eva] fc_builtins_in_ghost.c:6: 
+  function Frama_C_int_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_int_interval
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  Frama_C_entropy_source ∈ [--..--]
+  p ∈ [0..10]
+  __retres ∈ {0}
diff --git a/tests/syntax/ghost_vla.i b/tests/syntax/ghost_vla.i
new file mode 100644
index 0000000000000000000000000000000000000000..e2fbc9a738198c33b9f84bd47730a7d7d4dacfd1
--- /dev/null
+++ b/tests/syntax/ghost_vla.i
@@ -0,0 +1,9 @@
+int local_vla(int len){
+  //@ ghost int a[len];
+  //@ ghost a[4] = 32;
+  return 42;
+}
+
+void formal_vla(int len) /*@ ghost (int a[len]) */{
+  //@ ghost a[4] = 32;
+}
diff --git a/tests/syntax/oracle/ghost_vla.res.oracle b/tests/syntax/oracle/ghost_vla.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fba7be0da522d7865730b903feb102be92a63c80
--- /dev/null
+++ b/tests/syntax/oracle/ghost_vla.res.oracle
@@ -0,0 +1,34 @@
+[kernel] Parsing ghost_vla.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ assigns \nothing;
+    frees p; */
+ __attribute__((__FC_BUILTIN__)) void __fc_vla_free(void *p);
+
+/*@ assigns \result;
+    assigns \result \from \nothing;
+    allocates \result; */
+ __attribute__((__FC_BUILTIN__)) void *__fc_vla_alloc(unsigned int size);
+
+int local_vla(int len)
+{
+  int __retres;
+  /*@ ghost unsigned int __lengthof_a; */
+  /*@ ghost
+    /@ assert alloca_bounds: 0 < sizeof(int \ghost) * len ≤ 4294967295; @/
+    ;
+    __lengthof_a = (unsigned int)len;
+    int \ghost *a = __fc_vla_alloc(sizeof(int \ghost) * __lengthof_a);
+  */
+  /*@ ghost *(a + 4) = 32; */
+  __retres = 42;
+  __fc_vla_free((void *)a);
+  return __retres;
+}
+
+void formal_vla(int len) /*@ ghost (int \ghost a[len]) */
+{
+  /*@ ghost *(a + 4) = 32; */
+  return;
+}
+
+