[tests] ghost builtins and vlas

tests/libc/fc_builtins_in_ghost.c

+#include "__fc_builtin.h"
+
+int main(void){
+  int i ;
+  //@ ghost Frama_C_show_each(i);
+  //@ ghost int p = Frama_C_int_interval(0, 10);
+}

tests/libc/oracle/fc_builtins_in_ghost.res.oracle

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

tests/syntax/ghost_vla.i

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

tests/syntax/oracle/ghost_vla.res.oracle

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