From ba61ed50e7b2fdc78690de92d734a3747029f903 Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Wed, 8 Jun 2022 12:32:14 +0200
Subject: read globals from LLBC JSON into functions

---
 src/InterpreterStatements.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/InterpreterStatements.ml')

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 1083d643..c7308720 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -7,6 +7,7 @@ module A = LlbcAst
 module L = Logging
 open TypesUtils
 open ValuesUtils
+open FunIdentifier
 module Inv = Invariants
 module S = SynthesizeSymbolic
 open Errors
@@ -1001,7 +1002,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
         call.args call.dest
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
-and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
+and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id)
     (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
@@ -1079,7 +1080,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
   cc cf ctx
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
-and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
+and eval_local_function_call_symbolic (config : C.config) (fid : FunDeclId.id)
     (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
@@ -1300,7 +1301,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
 
 (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
     [eval_statement]) *)
-and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
+and eval_local_function_call (config : C.config) (fid : FunDeclId.id)
     (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
   match config.mode with
-- 
cgit v1.2.3