From 8fba8a9e71cc9625d874f27a96af4edd88764b37 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 3 Oct 2019 18:50:00 +0200
Subject: [PATCH] [Kernel] Tests about ghost parameters use the right option

---
 tests/cil/insert_formal.i    |  4 +-
 tests/cil/insert_formal.ml   | 98 +++++++++++++++++-------------------
 tests/spec/assigns_from_kf.i |  4 +-
 3 files changed, 51 insertions(+), 55 deletions(-)

diff --git a/tests/cil/insert_formal.i b/tests/cil/insert_formal.i
index f995057760a..d6222ef953c 100644
--- a/tests/cil/insert_formal.i
+++ b/tests/cil/insert_formal.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -print
 */
 
 //                   v
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
index 18e26925e70..0a0a7e01395 100644
--- a/tests/cil/insert_formal.ml
+++ b/tests/cil/insert_formal.ml
@@ -1,57 +1,53 @@
 open Cil_types
 
-class visitor = object
-  inherit Visitor.frama_c_inplace
-
-  method! vfunc f =
-    let insert_circ f = Cil.makeFormalVar f ~where:"^" "x" Cil.intType in
-    let insert_dollar f = Cil.makeFormalVar f ~where:"$" "x" Cil.intType in
-    let insert_circ_g f = Cil.makeFormalVar f ~ghost:true ~where:"^" "x" Cil.intType in
-    let insert_dollar_g f = Cil.makeFormalVar f ~ghost:true ~where:"$" "x" Cil.intType in
-    let insert_a f = Cil.makeFormalVar f ~where:"a" "x" Cil.intType in
-    let insert_a_g f = Cil.makeFormalVar f ~ghost:true ~where:"a" "x" Cil.intType in
-    let circ_list = [
-      "void_circumflex" ;
-      "a_circumflex" ;
-      "ghost_a_circumflex"
-    ] in
-    let dollar_list = [
-      "void_dollar" ;
-      "a_dollar" ;
-      "ghost_a_dollar"
-    ] in
-    let circ_g_list = [
-      "void_circumflex_g" ;
-      "a_circumflex_g" ;
-      "ghost_a_circumflex_g"
-    ] in
-    let dollar_g_list = [
-      "void_dollar_g" ;
-      "a_dollar_g" ;
-      "ghost_a_dollar_g"
-    ] in
-    let a_list = [
-      "a_a" ;
-      "a_b_c_a" ;
-      "b_a_c_a" ;
-      "a_ghost_b_c_a" ;
-    ] in
-    let a_g_list = [
-      "ghost_a_a" ;
-      "all_ghost_a_b_c_a" ;
-      "all_ghost_b_a_c_a" ;
-      "b_ghost_a_c_a"
-    ] in
-    if List.mem f.svar.vname circ_list then ignore(insert_circ f) ;
-    if List.mem f.svar.vname dollar_list then ignore(insert_dollar f) ;
-    if List.mem f.svar.vname circ_g_list then ignore(insert_circ_g f) ;
-    if List.mem f.svar.vname dollar_g_list then ignore(insert_dollar_g f) ;
-    if List.mem f.svar.vname a_list then ignore(insert_a f) ;
-    if List.mem f.svar.vname a_g_list then ignore(insert_a_g f) ;
-    Cil.DoChildren
-end
+let update_func f =
+  let insert_circ f = Cil.makeFormalVar f ~where:"^" "x" Cil.intType in
+  let insert_dollar f = Cil.makeFormalVar f ~where:"$" "x" Cil.intType in
+  let insert_circ_g f = Cil.makeFormalVar f ~ghost:true ~where:"^" "x" Cil.intType in
+  let insert_dollar_g f = Cil.makeFormalVar f ~ghost:true ~where:"$" "x" Cil.intType in
+  let insert_a f = Cil.makeFormalVar f ~where:"a" "x" Cil.intType in
+  let insert_a_g f = Cil.makeFormalVar f ~ghost:true ~where:"a" "x" Cil.intType in
+  let circ_list = [
+    "void_circumflex" ;
+    "a_circumflex" ;
+    "ghost_a_circumflex"
+  ] in
+  let dollar_list = [
+    "void_dollar" ;
+    "a_dollar" ;
+    "ghost_a_dollar"
+  ] in
+  let circ_g_list = [
+    "void_circumflex_g" ;
+    "a_circumflex_g" ;
+    "ghost_a_circumflex_g"
+  ] in
+  let dollar_g_list = [
+    "void_dollar_g" ;
+    "a_dollar_g" ;
+    "ghost_a_dollar_g"
+  ] in
+  let a_list = [
+    "a_a" ;
+    "a_b_c_a" ;
+    "b_a_c_a" ;
+    "a_ghost_b_c_a" ;
+  ] in
+  let a_g_list = [
+    "ghost_a_a" ;
+    "all_ghost_a_b_c_a" ;
+    "all_ghost_b_a_c_a" ;
+    "b_ghost_a_c_a"
+  ] in
+  if List.mem f.svar.vname circ_list then ignore(insert_circ f) ;
+  if List.mem f.svar.vname dollar_list then ignore(insert_dollar f) ;
+  if List.mem f.svar.vname circ_g_list then ignore(insert_circ_g f) ;
+  if List.mem f.svar.vname dollar_g_list then ignore(insert_dollar_g f) ;
+  if List.mem f.svar.vname a_list then ignore(insert_a f) ;
+  if List.mem f.svar.vname a_g_list then ignore(insert_a_g f) ;
+  ()
 
 let run () =
-  Visitor.visitFramacFileSameGlobals (new visitor) (Ast.get ())
+  Globals.Functions.iter_on_fundecs update_func
 
 let () = Db.Main.extend run
diff --git a/tests/spec/assigns_from_kf.i b/tests/spec/assigns_from_kf.i
index 6d537e59f65..cf8f4228ed4 100644
--- a/tests/spec/assigns_from_kf.i
+++ b/tests/spec/assigns_from_kf.i
@@ -1,6 +1,6 @@
 /* run.config
-  EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-  OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+  MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+  OPT: -print
 */
 
 void nothing(void);
-- 
GitLab