diff --git a/tests/misc/Change_formals.ml b/tests/cil/Change_formals.ml
similarity index 100%
rename from tests/misc/Change_formals.ml
rename to tests/cil/Change_formals.ml
diff --git a/tests/cil/change_formals.c b/tests/cil/change_formals.c
new file mode 100644
index 0000000000000000000000000000000000000000..5ac6f89b75edfa8287197e7faefe404870c75820
--- /dev/null
+++ b/tests/cil/change_formals.c
@@ -0,0 +1,17 @@
+/* run.config
+EXECNOW: make -s tests/cil/Change_formals.cmxs
+OPT: -load-module tests/cil/Change_formals.cmxs -cpp-extra-args="-DNO_PROTO" -then-on test -print
+OPT: -load-module tests/cil/Change_formals.cmxs -cpp-extra-args="-DNO_IMPLEM" -then-on test -print
+OPT: -load-module tests/cil/Change_formals.cmxs -then-on test -print
+*/
+
+#ifndef NO_PROTO
+int f(int x);
+#endif
+
+#ifndef NO_IMPLEM
+int f(int x) { return x; }
+#endif
+
+// needed to prevent erasure of f in NO_IMPLEM case
+int g() { return f(0); }
diff --git a/tests/cil/insert_formal.i b/tests/cil/insert_formal.i
new file mode 100644
index 0000000000000000000000000000000000000000..5076f1f5c8931399845e12c95bb20a265355f9a9
--- /dev/null
+++ b/tests/cil/insert_formal.i
@@ -0,0 +1,103 @@
+/* run.config
+OPT: -load-script tests/cil/insert_formal.ml -print
+*/
+
+//                   v
+void void_circumflex( void ) {
+
+}
+
+//                            v
+void void_circumflex_g( void ) {
+
+}
+
+//                    v
+void void_dollar( void ) {
+
+}
+
+//                        v
+void void_dollar_g( void ) {
+
+}
+
+//                v
+void a_circumflex( int a ) {
+
+}
+
+//                  v
+void a_dollar( int a ) {
+
+}
+
+//                          v
+void a_circumflex_g( int a ) {
+
+}
+
+//                      v
+void a_dollar_g( int a ) {
+
+}
+
+//             v
+void a_a( int a ){
+
+}
+
+//                      v
+void ghost_a_circumflex( void ) /*@ ghost ( int a ) */ {
+
+}
+
+//                       v
+void ghost_a_dollar( void ) /*@ ghost ( int a ) */ {
+
+}
+
+//                                           v
+void ghost_a_circumflex_g( void ) /*@ ghost ( int a ) */ {
+
+}
+
+//                                             v
+void ghost_a_dollar_g( void ) /*@ ghost ( int a ) */ {
+
+}
+
+//                                      v
+void ghost_a_a( void ) /*@ ghost ( int a ) */ {
+
+}
+
+//                  v
+void a_b_c_a (int a, int b, int c) {
+
+}
+
+//                         v
+void b_a_c_a (int b, int a, int c) {
+
+}
+
+//                                              v
+void all_ghost_a_b_c_a ( void )/*@ ghost (int a, int b, int c) */ {
+
+}
+
+//                                                     v
+void all_ghost_b_a_c_a ( void )/*@ ghost (int b, int a, int c) */ {
+
+}
+
+//                        v
+void a_ghost_b_c_a ( int a )/*@ ghost (int b, int c) */ {
+
+}
+
+//                                           v
+void b_ghost_a_c_a ( int b )/*@ ghost (int a, int c) */ {
+
+}
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
new file mode 100644
index 0000000000000000000000000000000000000000..dd545df87cc28ee642b3c8472215901484580151
--- /dev/null
+++ b/tests/cil/insert_formal.ml
@@ -0,0 +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 ~where:"^g" "x" Cil.intType in
+    let insert_dollar_g f = Cil.makeFormalVar f ~where:"$g" "x" Cil.intType in
+    let insert_a f = Cil.makeFormalVar f ~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" ;
+      "ghost_a_a" ;
+      "a_b_c_a" ;
+      "b_a_c_a" ;
+      "all_ghost_a_b_c_a" ;
+      "all_ghost_b_a_c_a" ;
+      "a_ghost_b_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) ;
+    Cil.DoChildren
+end
+
+let run () =
+  Visitor.visitFramacFileSameGlobals (new visitor) (Ast.get ())
+
+let () = Db.Main.extend run
diff --git a/tests/misc/oracle/change_formals.0.res.oracle b/tests/cil/oracle/change_formals.0.res.oracle
similarity index 75%
rename from tests/misc/oracle/change_formals.0.res.oracle
rename to tests/cil/oracle/change_formals.0.res.oracle
index 22dc10f37e8a0e84a256544ee404ff1e529bcd10..794634cc91e1d6d84d9f983b9b9a68b9e869e1d5 100644
--- a/tests/misc/oracle/change_formals.0.res.oracle
+++ b/tests/cil/oracle/change_formals.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
 [test] current prj = project "test"
 [test] current prj = project "test"
 /* Generated by Frama-C */
diff --git a/tests/misc/oracle/change_formals.1.res.oracle b/tests/cil/oracle/change_formals.1.res.oracle
similarity index 69%
rename from tests/misc/oracle/change_formals.1.res.oracle
rename to tests/cil/oracle/change_formals.1.res.oracle
index 1f5fcdcd5e9190f8f8d30d8539dc1445a9034ed0..0269f038c67b179ed56aa983d0535dd43b6a6fc4 100644
--- a/tests/misc/oracle/change_formals.1.res.oracle
+++ b/tests/cil/oracle/change_formals.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
 [test] current prj = project "test"
 /* Generated by Frama-C */
 int f(int x, int ok);
diff --git a/tests/misc/oracle/change_formals.2.res.oracle b/tests/cil/oracle/change_formals.2.res.oracle
similarity index 77%
rename from tests/misc/oracle/change_formals.2.res.oracle
rename to tests/cil/oracle/change_formals.2.res.oracle
index 3f746d6b7f699a77b6f8d4fff112a9d72aa9ea18..9e91be519b33bd2915fe44dc2286eb5c28d291bc 100644
--- a/tests/misc/oracle/change_formals.2.res.oracle
+++ b/tests/cil/oracle/change_formals.2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
 [test] current prj = project "test"
 [test] current prj = project "test"
 /* Generated by Frama-C */
diff --git a/tests/cil/oracle/insert_formal.res.oracle b/tests/cil/oracle/insert_formal.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..935880bfc244d9cd8094c650bd014f02abaead45
--- /dev/null
+++ b/tests/cil/oracle/insert_formal.res.oracle
@@ -0,0 +1,103 @@
+[kernel] Parsing tests/cil/insert_formal.i (no preprocessing)
+/* Generated by Frama-C */
+void void_circumflex(int x)
+{
+  return;
+}
+
+void void_circumflex_g(void)/*@ ghost (int x) */
+{
+  return;
+}
+
+void void_dollar(int x)
+{
+  return;
+}
+
+void void_dollar_g(void)/*@ ghost (int x) */
+{
+  return;
+}
+
+void a_circumflex(int x, int a)
+{
+  return;
+}
+
+void a_dollar(int a, int x)
+{
+  return;
+}
+
+void a_circumflex_g(int a)/*@ ghost (int x) */
+{
+  return;
+}
+
+void a_dollar_g(int a)/*@ ghost (int x) */
+{
+  return;
+}
+
+void a_a(int a, int x)
+{
+  return;
+}
+
+void ghost_a_circumflex(int x)/*@ ghost (int a) */
+{
+  return;
+}
+
+void ghost_a_dollar(int x)/*@ ghost (int a) */
+{
+  return;
+}
+
+void ghost_a_circumflex_g(void)/*@ ghost (int x, int a) */
+{
+  return;
+}
+
+void ghost_a_dollar_g(void)/*@ ghost (int a, int x) */
+{
+  return;
+}
+
+void ghost_a_a(void)/*@ ghost (int a, int x) */
+{
+  return;
+}
+
+void a_b_c_a(int a, int x, int b, int c)
+{
+  return;
+}
+
+void b_a_c_a(int b, int a, int x, int c)
+{
+  return;
+}
+
+void all_ghost_a_b_c_a(void)/*@ ghost (int a, int x, int b, int c) */
+{
+  return;
+}
+
+void all_ghost_b_a_c_a(void)/*@ ghost (int b, int a, int x, int c) */
+{
+  return;
+}
+
+void a_ghost_b_c_a(int a, int x)/*@ ghost (int b, int c) */
+{
+  return;
+}
+
+void b_ghost_a_c_a(int b)/*@ ghost (int a, int x, int c) */
+{
+  return;
+}
+
+
diff --git a/tests/misc/change_formals.c b/tests/misc/change_formals.c
deleted file mode 100644
index c84ec7afadef6caf0fe82ca4d74cb4c1521062a2..0000000000000000000000000000000000000000
--- a/tests/misc/change_formals.c
+++ /dev/null
@@ -1,17 +0,0 @@
-/* run.config
-EXECNOW: make -s tests/misc/Change_formals.cmxs
-OPT: -load-module tests/misc/Change_formals.cmxs -cpp-extra-args="-DNO_PROTO" -then-on test -print
-OPT: -load-module tests/misc/Change_formals.cmxs -cpp-extra-args="-DNO_IMPLEM" -then-on test -print
-OPT: -load-module tests/misc/Change_formals.cmxs -then-on test -print
-*/
-
-#ifndef NO_PROTO
-int f(int x);
-#endif
-
-#ifndef NO_IMPLEM
-int f(int x) { return x; }
-#endif
-
-// needed to prevent erasure of f in NO_IMPLEM case
-int g() { return f(0); }