summaryrefslogtreecommitdiff
path: root/src/InterpreterStatements.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterStatements.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 3f6470b9..ffc47741 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -919,11 +919,16 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i
(* Treat the global as a function without arguments to call *)
(eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx
| SymbolicMode ->
+ (*
+ let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in
+ (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx
+ *)
+ failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value";
(* Treat the global as a fresh symbolic value *)
let rty = ety_no_regions_to_rty global.ty in
let sval = mk_fresh_symbolic_value V.FunCallRet rty in
let sval = mk_typed_value_from_symbolic_value sval in
- assign_to_place config sval place (cf Unit) ctx
+ (assign_to_place config sval place) (cf Unit) ctx
(** Evaluate a switch *)
and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :