diff options
author | Sidney Congard | 2022-08-08 15:16:14 +0200 |
---|---|---|
committer | Sidney Congard | 2022-08-08 15:16:14 +0200 |
commit | 3c5fb260012ee8bb8b9fd90bc4624d893ac7678a (patch) | |
tree | 6702e5d4b3b01aa1a96da150dd17ca6f4dfce326 /src/InterpreterStatements.ml | |
parent | f9015d1e956ace6c875eb6a631caeac49cfb8148 (diff) |
Register global names, one error remaining
Diffstat (limited to 'src/InterpreterStatements.ml')
-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) : |