diff options
| author | Sidney Congard | 2022-06-21 11:41:09 +0200 |
|---|---|---|
| committer | Sidney Congard | 2022-06-21 11:41:09 +0200 |
| commit | 7703c4ca86a390303d0a120f8811c8fd704c5168 (patch) | |
| tree | 399145f7c842d9f59216e17b6e43964b2c4dfaa6 /src/Contexts.ml | |
| parent | 414769e0c9a1d370d3ab906b710e2e8adfe25e5e (diff) | |
concrete & symbolic evaluation work with new LLBC format
Diffstat (limited to 'src/Contexts.ml')
| -rw-r--r-- | src/Contexts.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index bbf5b8f3..1fbc916b 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -1,7 +1,6 @@ open Types open Values open LlbcAst -open FunIdentifier module V = Values open ValuesUtils module M = Modules @@ -218,7 +217,11 @@ type type_context = { } [@@deriving show] -type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show] +type fun_context = { + fun_decls : fun_decl FunDeclId.Map.t; + gid_conv : global_id_converter; +} +[@@deriving show] type eval_ctx = { type_context : type_context; @@ -256,6 +259,10 @@ let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl = let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl = FunDeclId.Map.find fid ctx.fun_context.fun_decls +(** TODO: make this more efficient with maps *) +let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : fun_decl = + ctx_lookup_fun_decl ctx (global_to_fun_id ctx.fun_context.gid_conv gid) + (** Retrieve a variable's value in an environment *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = (* We take care to stop at the end of current frame: different variables |