[Test] Adds some tests related to insertion of formals in ghost functions

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) {
+
+  }
+*/

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) ;

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