@@ -128,36 +128,6 @@ let po_anchor_to_pretty a =
128128 | IndirectAccess n -> LBLOCK [ STR " indirect ( " ; bterm_to_pretty n ; STR " )" ]
129129
130130
131- class type saved_register_int =
132- object ('a)
133-
134- method compare : 'a -> int
135-
136- method set_save_address : ctxt_iaddress_t -> unit
137- method add_restore_address : ctxt_iaddress_t -> unit
138-
139- method get_register : register_t
140- method get_save_address : ctxt_iaddress_t
141- method get_restore_addresses: ctxt_iaddress_t list
142-
143- method has_save_address : bool
144- method has_restore_addresses: bool
145-
146- method is_save_or_restore_address: ctxt_iaddress_t -> bool
147-
148- method write_xml: xml_element_int -> unit
149- method toPretty: pretty_t
150- end
151-
152-
153- module SavedRegistersCollections = CHCollections. Make
154- (struct
155- type t = saved_register_int
156- let compare r1 r2 = r1#compare r2
157- let toPretty r = r#toPretty
158- end )
159-
160-
161131let pr_expr = xpr_formatter#pr_expr
162132
163133
@@ -907,6 +877,29 @@ object (self)
907877 let _ = memmap#add_location ~size: (Some size) ~btype dw in
908878 Ok (self#mk_variable (self#varmgr#make_global_variable dw#to_numerical))
909879
880+ method mk_stack_variable
881+ (stackframe : stackframe_int )
882+ (offset : numerical_t ): variable_t traceresult =
883+ match stackframe#containing_stackslot offset#toInt with
884+ | Some stackslot ->
885+ tmap
886+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : memref:stack" )
887+ (fun memoffset ->
888+ let svar =
889+ self#mk_variable
890+ (self#varmgr#make_local_stack_variable
891+ ~offset: memoffset (mkNumerical stackslot#offset)) in
892+ let name = stackslot#name ^ (memory_offset_to_string memoffset) in
893+ begin
894+ self#set_variable_name svar name;
895+ svar
896+ end )
897+ (stackslot#frame_offset_memory_offset (num_constant_expr offset))
898+ | _ ->
899+ Error [
900+ __FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : "
901+ ^ " No stack slot found at offset " ^ offset#toString]
902+
910903 method mk_register_variable (register :register_t ) =
911904 self#mk_variable (varmgr#make_register_variable register)
912905
0 commit comments