@@ -218,7 +218,7 @@ object (self)
218218 (mkNumerical fld.fld_offset) in
219219 let fldname = vname ^ " ->" ^ fld.fld_name in
220220 let fldtype = fld.fld_type in
221- let ifldvar = self#mk_initial_memory_value fldvar in
221+ let ifldvar = TR. tget_ok ( self#mk_initial_memory_value fldvar) in
222222 let ifldname = fldname ^ " _in" in
223223 let _ = chlog#add " set field var" (STR fldname) in
224224 begin
@@ -243,7 +243,7 @@ object (self)
243243 List. iter (fun (offset , name , _ty ) ->
244244 let memref = self#mk_local_stack_reference in
245245 let v = self#mk_memory_variable memref (mkNumerical offset) in
246- let initV = self#mk_initial_memory_value v in
246+ let initV = TR. tget_ok ( self#mk_initial_memory_value v) in
247247 begin
248248 self#set_variable_name initV name ;
249249 if offset = 4 then
@@ -253,7 +253,7 @@ object (self)
253253 let jniInterfacePtr =
254254 self#mk_memory_variable memref numerical_zero in
255255 let jniInterfacePtrIn =
256- self#mk_initial_memory_value jniInterfacePtr in
256+ TR. tget_ok ( self#mk_initial_memory_value jniInterfacePtr) in
257257 self#set_variable_name jniInterfacePtrIn " jni$Ifp" )
258258 ~error: (fun _ -> () )
259259 (self#mk_base_variable_reference initV)
@@ -264,7 +264,7 @@ object (self)
264264 List. iter (fun (offset , name , _ty ) ->
265265 let memref = self#mk_local_stack_reference in
266266 let v = self#mk_memory_variable memref (mkNumerical offset) in
267- let initV = self#mk_initial_memory_value v in
267+ let initV = TR. tget_ok ( self#mk_initial_memory_value v) in
268268 begin
269269 self#set_variable_name initV name ;
270270 if offset = 4 then
@@ -275,7 +275,7 @@ object (self)
275275 let jniInterfacePtr =
276276 self#mk_memory_variable memref numerical_zero in
277277 let jniInterfacePtrIn =
278- self#mk_initial_memory_value jniInterfacePtr in
278+ TR. tget_ok ( self#mk_initial_memory_value jniInterfacePtr) in
279279 self#set_variable_name jniInterfacePtrIn " jni$Ifp" )
280280 ~error: (fun _ -> () )
281281 (self#mk_base_variable_reference initV)
@@ -287,7 +287,7 @@ object (self)
287287 let memref = self#mk_local_stack_reference in
288288 let argvar =
289289 self#mk_memory_variable ~save_name: false memref (mkNumerical (4 * i)) in
290- let argvarin = self#mk_initial_memory_value argvar in
290+ let argvarin = TR. tget_ok ( self#mk_initial_memory_value argvar) in
291291 begin
292292 match sc with
293293 | FieldValues l ->
@@ -296,7 +296,7 @@ object (self)
296296 (log_error " set_argument_structconstant" " invalid memref" )
297297 ~ok: (fun mref ->
298298 let mvar = self#mk_memory_variable mref (mkNumerical offset) in
299- let mvarin = self#mk_initial_memory_value mvar in
299+ let mvarin = TR. tget_ok ( self#mk_initial_memory_value mvar) in
300300 match ssc with
301301 | FieldString s ->
302302 begin
@@ -337,7 +337,8 @@ object (self)
337337 let mvar =
338338 self#mk_memory_variable mref
339339 (mkNumerical offset) in
340- let mvarin = self#mk_initial_memory_value mvar in
340+ let mvarin =
341+ TR. tget_ok (self#mk_initial_memory_value mvar) in
341342 match ssc with
342343 | FieldCallTarget tgt ->
343344 begin
@@ -393,7 +394,7 @@ object (self)
393394 memref
394395 (mkNumerical
395396 (i * 4 )) in
396- let memInitVar = self#mk_initial_memory_value memvar in
397+ let memInitVar = TR. tget_ok ( self#mk_initial_memory_value memvar) in
397398 (name,memInitVar)) stackpardata in
398399 let regVars =
399400 List. map (fun (r ,name ) ->
@@ -439,7 +440,8 @@ object (self)
439440 ~save_name: false
440441 memref
441442 (mkNumerical dm.cppdm_offset) in
442- let memberInitVar = self#mk_initial_memory_value memberVar in
443+ let memberInitVar =
444+ TR. tget_ok (self#mk_initial_memory_value memberVar) in
443445 let mName = self#variable_name_to_string basevar in
444446 let name = mName ^ " ->" ^ dm.cppdm_name in
445447 self#set_variable_name memberInitVar name)
@@ -457,7 +459,7 @@ object (self)
457459 memref
458460 (mkNumerical vf.cppvf_offset) in
459461 let vfptrInitVar =
460- self#mk_initial_memory_value vfptrVar in
462+ TR. tget_ok ( self#mk_initial_memory_value vfptrVar) in
461463 let mName = self#variable_name_to_string basevar in
462464 let vfptrName = mName ^ " ->vtableptr" in
463465 let vfsummaries = get_vtable_summaries vf.cppvf_table in
@@ -474,7 +476,7 @@ object (self)
474476 vfmemref
475477 (mkNumerical vfOffset) in
476478 let vfInitVar =
477- self#mk_initial_memory_value vfVar in
479+ TR. tget_ok ( self#mk_initial_memory_value vfVar) in
478480 self#register_virtual_call vfInitVar summary)
479481 ~error: (fun _ -> () )
480482 (self#mk_base_variable_reference vfptrInitVar))
@@ -497,7 +499,8 @@ object (self)
497499 ~save_name: false
498500 memref
499501 (mkNumerical dm.cppdm_offset) in
500- let memberInitVar = self#mk_initial_memory_value memberVar in
502+ let memberInitVar =
503+ TR. tget_ok (self#mk_initial_memory_value memberVar) in
501504 let name = " this->" ^ dm.cppdm_name in
502505 begin
503506 self#set_variable_name memberInitVar name ;
@@ -516,7 +519,8 @@ object (self)
516519 ~save_name: false
517520 memref
518521 (mkNumerical vf.cppvf_offset) in
519- let vfptrInitVar = self#mk_initial_memory_value vfptrVar in
522+ let vfptrInitVar =
523+ TR. tget_ok (self#mk_initial_memory_value vfptrVar) in
520524 let vfptrVarName = " this->" ^ " vtableptr" in
521525 let vfsummaries = get_vtable_summaries vf.cppvf_table in
522526 begin
@@ -531,7 +535,8 @@ object (self)
531535 ~save_name: false
532536 vfmemref
533537 (mkNumerical vfOffset) in
534- let vfInitVar = self#mk_initial_memory_value vfVar in
538+ let vfInitVar =
539+ TR. tget_ok (self#mk_initial_memory_value vfVar) in
535540 self#register_virtual_call vfInitVar summary)
536541 ~error: (fun _ -> () )
537542 (self#mk_base_variable_reference vfptrInitVar))
@@ -556,34 +561,57 @@ object (self)
556561 let stackpardata =
557562 List. map (fun p ->
558563 let (name, ty) = get_parameter_signature p in
559- let offset = TR. tget_ok (get_stack_parameter_offset p) in
560- (offset, name, ty)) (get_stack_parameters fintf) in
564+ let offset = get_stack_parameter_offset p in
565+ (offset, name, ty))
566+ (get_stack_parameters fintf) in
561567 let regpardata =
562568 List. map (fun p ->
563569 let (name, ty) = get_parameter_signature p in
564- let reg = TR. tget_ok ( get_register_parameter_register p) in
570+ let reg = get_register_parameter_register p in
565571 (reg, name, ty)) (get_register_parameters fintf) in
566572 begin
567- List. iter (fun (offset , name , ty ) ->
568- let memref = self#mk_local_stack_reference in
569- let v =
570- self#mk_memory_variable
571- ~save_name: false memref (mkNumerical offset) in
572- let iv = self#mk_initial_memory_value v in
573- let vname = name ^ " $" ^ (string_of_int offset) in
574- begin
575- self#set_variable_name iv vname ;
576- if is_ptrto_known_struct ty then
577- self#set_pointedto_struct_field_names 1 iv vname ty
578- end ) stackpardata;
579- List. iter (fun (reg ,name ,ty ) ->
580- let v = self#mk_initial_register_value ~level: 0 reg in
581- let vname = name in
582- begin
583- self#set_variable_name v vname ;
584- if is_ptrto_known_struct ty then
585- self#set_pointedto_struct_field_names 1 v vname ty
586- end ) regpardata
573+ List. iter (fun (offset_r , name , ty ) ->
574+ let memref = self#mk_local_stack_reference in
575+ TR. tfold
576+ ~ok: (fun offset ->
577+ let v =
578+ self#mk_memory_variable
579+ ~save_name: false memref (mkNumerical offset) in
580+ TR. tfold
581+ ~ok: (fun iv ->
582+ let vname = name ^ " $" ^ (string_of_int offset) in
583+ begin
584+ self#set_variable_name iv vname;
585+ if is_ptrto_known_struct ty then
586+ self#set_pointedto_struct_field_names 1 iv vname ty
587+ end )
588+ ~error: (fun e ->
589+ ch_error_log#add
590+ (" set_argument_names:" ^ (string_of_int __LINE__))
591+ (STR (String. concat " ; " e)))
592+ (self#mk_initial_memory_value v))
593+ ~error: (fun e ->
594+ ch_error_log#add
595+ (" set_argument_names" ^ (string_of_int __LINE__))
596+ (STR (String. concat " ; " e)))
597+ offset_r
598+ ) stackpardata;
599+ List. iter (fun (reg_r , name , ty ) ->
600+ TR. tfold
601+ ~ok: (fun reg ->
602+ let v = self#mk_initial_register_value ~level: 0 reg in
603+ let vname = name in
604+ begin
605+ self#set_variable_name v vname;
606+ if is_ptrto_known_struct ty then
607+ self#set_pointedto_struct_field_names 1 v vname ty
608+ end )
609+ ~error: (fun e ->
610+ ch_error_log#add
611+ (" set_argument_names:" ^ (string_of_int __LINE__))
612+ (STR (String. concat " ; " e)))
613+ reg_r
614+ ) regpardata
587615 end
588616
589617
@@ -608,7 +636,7 @@ object (self)
608636 method mk_base_sym_reference
609637 (s : symbol_t ): memory_reference_int traceresult =
610638 tbind
611- ~msg: " env:mk_base_sym_reference "
639+ ~msg: (__FILE__ ^ " : " ^ (string_of_int __LINE__))
612640 self#mk_base_variable_reference
613641 (self#get_variable s#getSeqNumber)
614642
@@ -688,7 +716,8 @@ object (self)
688716 if H. mem chifvars index then
689717 Ok (H. find chifvars index)
690718 else
691- Error [" env#get_variable: index not found: " ^ (string_of_int index)]
719+ Error [__FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : "
720+ ^ " No variable found with index: " ^ (string_of_int index)]
692721
693722 method get_variable_type (var : variable_t ): btype_t option =
694723 varmgr#get_variable_type var
@@ -770,7 +799,7 @@ object (self)
770799 | BaseVar v when variable_names#has v#getName#getSeqNumber ->
771800 Some (variable_names#get v#getName#getSeqNumber)
772801 | _ -> None in
773- let offset = ConstantOffset (offset,NoOffset ) in
802+ let offset = ConstantOffset (offset, NoOffset ) in
774803 let avar = varmgr#make_memory_variable ~size memref offset in
775804 let v = self#mk_variable avar in
776805 let _ = match optName with
@@ -792,17 +821,19 @@ object (self)
792821 else
793822 Error [__FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : "
794823 ^ " variable " ^ (p2s v#toPretty) ^ " is not a memory variable" ]
795-
796- method mk_index_offset_memory_variable
824+ (*
825+ method mk_offset_memory_variable
797826 ?(size=4)
798827 (memref: memory_reference_int)
799- (offset : memory_offset_t ) =
828+ (offset: memory_offset_t): variable_t =
800829 if memref#is_unknown_reference then
801830 self#mk_num_temp
802831 else
803832 let avar = varmgr#make_memory_variable memref ~size offset in
804833 self#mk_variable avar
834+ *)
805835
836+ (*
806837 method mk_index_offset_global_memory_variable
807838 ?(elementsize=4)
808839 (base: numerical_t)
@@ -835,6 +866,7 @@ object (self)
835866 self#set_variable_name ivar (vname ^ "_in")
836867 end in
837868 Ok var
869+ *)
838870
839871 method mk_gloc_variable
840872 (gloc : global_location_int ) (offset : memory_offset_t ): variable_t =
@@ -1018,25 +1050,17 @@ object (self)
10181050 ~error: (fun _ -> () )
10191051 (varmgr#get_global_variable_address v)
10201052
1021- method mk_initial_memory_value (v :variable_t ): variable_t =
1053+ method mk_initial_memory_value (v :variable_t ): variable_t traceresult =
10221054 if (self#is_memory_variable v) && (self#has_constant_offset v) then
10231055 let iv = self#mk_variable (varmgr#make_initial_memory_value v) in
10241056 let _ =
10251057 if varmgr#is_global_variable v then
10261058 self#probe_global_var_field_values v iv in
1027- iv
1059+ Ok iv
10281060 else
1029- let msg =
1030- (LBLOCK [
1031- STR " variable is not suitable for initial memory variable: " ;
1032- v#toPretty;
1033- STR " (" ;
1034- faddr#toPretty;
1035- STR " )" ]) in
1036- begin
1037- ch_error_log#add " function environment" msg;
1038- raise (BCH_failure msg)
1039- end
1061+ Error [__FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : "
1062+ ^ " Variable is not suitable for initial memory value: "
1063+ ^ v#getName#getBaseName]
10401064
10411065 method mk_initial_register_value ?(level =0 ) (r :register_t ) =
10421066 self#mk_variable (varmgr#make_initial_register_value r level)
0 commit comments