From 295c7a787cb8921ef297edc031e7e00f6a1a7b33 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 30 Mar 2023 18:14:30 +0200
Subject: [PATCH] [parsing] use Kernel functions for symbol lookup
---
meta_bindings.ml | 2 +-
meta_parse.ml | 15 ++++++---------
2 files changed, 7 insertions(+), 10 deletions(-)
diff --git a/meta_bindings.ml b/meta_bindings.ml
index fbc697d..1317129 100644
--- a/meta_bindings.ml
+++ b/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 =
diff --git a/meta_parse.ml b/meta_parse.ml
index 30a47f3..d95011c 100644
--- a/meta_parse.ml
+++ b/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
--
GitLab