Merge branch 'feature/kernel/syntactic-search' into 'master'

use Kernel functions for symbol lookup

See merge request frama-c/meta!78

meta_bindings.ml

@@ -172,7 +172,7 @@ let add_ghost_code flags =
       Ast.mark_as_changed ()
     end
 
-let search_global_var name = Globals.Vars.find_from_astinfo name VGlobal
+let search_global_var name = Globals.Vars.find_from_astinfo name Global
 
 (* Replace \binds by code adequately modifying _set and _size *)
 let make_static_modif_code name lvar =

meta_parse.ml

@@ -139,14 +139,11 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
       let label = FormalLabel l in
       Logic_const.tat (e_t, label)
     | PLapp ("\\formal", _, [{lexpr_node = PLvar param}]) ->
-      let formals = Kernel_function.get_formals kf in
-      begin try
-        let vi = List.find (fun vi -> vi.vname = param) formals in
-        let lv = Cil.cvar_to_lvar vi in
-        Logic_const.tvar lv
-      with Not_found -> meta_ctxt.error loc "%s is not a formal in %a"
-                          param Kernel_function.pretty kf
-      end
+      (match Globals.Syntactic_search.find_in_scope param (Formal kf) with
+        | Some vi -> vi |> Cil.cvar_to_lvar |> Logic_const.tvar
+        | None ->
+          meta_ctxt.error loc "%s is not a formal in %a"
+            param Kernel_function.pretty kf)
     | PLapp ("\\bound", _, [bound]) ->
       Meta_bindings.parse_bound meta_ctxt loc quantifiers bound
     | PLapp (app_name, _, [{lexpr_node = PLvar arg}])
@@ -256,7 +253,7 @@ let delay_prop tc name lexpr kf aslist =
     (* Tweak find_var so it can find things after link *)
     try tc.find_var var
     with Not_found -> try
-      let vi = Globals.Vars.find_from_astinfo var VGlobal in
+      let vi = Globals.Vars.find_from_astinfo var Global in
       Cil.cvar_to_lvar vi
     with Not_found ->
       let kf = Globals.Functions.find_by_name var in