From 082ac819b7f2ed9a3e177ec32476340a30a0eaf6 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 28 Sep 2022 10:23:07 +0200
Subject: [PATCH] [tests] ghost builtins and vlas

---
 tests/libc/fc_builtins_in_ghost.c             |  7 ++++
 .../oracle/fc_builtins_in_ghost.res.oracle    | 20 +++++++++++
 tests/syntax/ghost_vla.i                      |  9 +++++
 tests/syntax/oracle/ghost_vla.res.oracle      | 34 +++++++++++++++++++
 4 files changed, 70 insertions(+)
 create mode 100644 tests/libc/fc_builtins_in_ghost.c
 create mode 100644 tests/libc/oracle/fc_builtins_in_ghost.res.oracle
 create mode 100644 tests/syntax/ghost_vla.i
 create mode 100644 tests/syntax/oracle/ghost_vla.res.oracle

diff --git a/tests/libc/fc_builtins_in_ghost.c b/tests/libc/fc_builtins_in_ghost.c
new file mode 100644
index 00000000000..dee454a232e
--- /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 00000000000..0d46a02edf5
--- /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 00000000000..e2fbc9a7381
--- /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 00000000000..fba7be0da52
--- /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;
+}
+
+
-- 
GitLab