diff options
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterStatements.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index ffc47741..31c3aabb 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -919,16 +919,20 @@ 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 -> + (* Treat the global as a fresh symbolic value *) + (* 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 + (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : |