diff --git a/tests/cil/insert_formal.i b/tests/cil/insert_formal.i
index d6222ef953c9ff024b70b15790c0599661a69875..5b30c58d98030efe6ba865ee764fc5e8b7140d86 100644
--- a/tests/cil/insert_formal.i
+++ b/tests/cil/insert_formal.i
@@ -102,3 +102,40 @@ void a_ghost_b_c_a ( int a )/*@ ghost (int b, int c) */ {
 void b_ghost_a_c_a ( int b )/*@ ghost (int a, int c) */ {
 
 }
+
+/*@ ghost
+  //                     v
+  void g_void_circumflex( void ) {
+
+  }
+
+  //                      v
+  void g_void_dollar( void ) {
+
+  }
+
+  //                  v
+  void g_a_circumflex( int a ) {
+
+  }
+
+  //                    v
+  void g_a_dollar( int a ) {
+
+  }
+
+  //               v
+  void g_a_a( int a ){
+
+  }
+
+  //                    v
+  void g_a_b_c_a (int a, int b, int c) {
+
+  }
+
+  //                           v
+  void g_b_a_c_a (int b, int a, int c) {
+
+  }
+*/
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
index 0a0a7e013955303b51259055161c3e30a9526836..a4796d9b33bb2fdf068980b0230a25f860cba669 100644
--- a/tests/cil/insert_formal.ml
+++ b/tests/cil/insert_formal.ml
@@ -20,12 +20,16 @@ let update_func f =
   let circ_g_list = [
     "void_circumflex_g" ;
     "a_circumflex_g" ;
-    "ghost_a_circumflex_g"
+    "ghost_a_circumflex_g" ;
+    "g_void_circumflex" ;
+    "g_a_circumflex"
   ] in
   let dollar_g_list = [
     "void_dollar_g" ;
     "a_dollar_g" ;
-    "ghost_a_dollar_g"
+    "ghost_a_dollar_g" ;
+    "g_void_dollar" ;
+    "g_a_dollar"
   ] in
   let a_list = [
     "a_a" ;
@@ -37,7 +41,10 @@ let update_func f =
     "ghost_a_a" ;
     "all_ghost_a_b_c_a" ;
     "all_ghost_b_a_c_a" ;
-    "b_ghost_a_c_a"
+    "b_ghost_a_c_a" ;
+    "g_a_a" ;
+    "g_a_b_c_a" ;
+    "g_b_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) ;
diff --git a/tests/cil/oracle/insert_formal.res.oracle b/tests/cil/oracle/insert_formal.res.oracle
index faefb89b04774d031958731f2df0f3da1dc8176c..06fe54925388a880fa643e2d843b97244abc567e 100644
--- a/tests/cil/oracle/insert_formal.res.oracle
+++ b/tests/cil/oracle/insert_formal.res.oracle
@@ -100,4 +100,53 @@ void b_ghost_a_c_a(int b) /*@ ghost (int a, int x, int c) */
   return;
 }
 
+/*@ ghost void g_void_circumflex(int x)
+          {
+            return;
+          }
+
+*/
+
+/*@ ghost void g_void_dollar(int x)
+          {
+            return;
+          }
+
+*/
+
+/*@ ghost void g_a_circumflex(int x, int a)
+          {
+            return;
+          }
+
+*/
+
+/*@ ghost void g_a_dollar(int a, int x)
+          {
+            return;
+          }
+
+*/
+
+/*@ ghost void g_a_a(int a, int x)
+          {
+            return;
+          }
+
+*/
+
+/*@ ghost void g_a_b_c_a(int a, int x, int b, int c)
+          {
+            return;
+          }
+
+*/
+
+/*@ ghost void g_b_a_c_a(int b, int a, int x, int c)
+          {
+            return;
+          }
+
+*/
+