Index: ma_memory_change_mediator.e
===================================================================
--- ma_memory_change_mediator.e	(revision 95541)
+++ ma_memory_change_mediator.e	(working copy)
@@ -120,6 +120,7 @@
 		local
 			l_state_1, l_state_2: MA_MEMORY_STATE
 			l_info_dlg: EV_INFORMATION_DIALOG
+			l_increased: attached like grid_data_increased
 		do
 			if grid_from_state.has_selected_row then
 				if grid_to_state.has_selected_row then
@@ -126,8 +127,9 @@
 					l_state_2 := states.i_th (grid_to_state.selected_rows.first.index)
 					l_state_1 := states.i_th (grid_from_state.selected_rows.first.index)
 					grid_util.grid_remove_and_clear_all_rows (grid_changed)
-					grid_data_increased := l_state_1.compare (l_state_2)
-					update_grid_increased_content
+					l_increased := l_state_1.compare (l_state_2)
+					grid_data_increased := l_increased
+					update_grid_increased_content (l_increased)
 				else
 					create l_info_dlg.make_with_text ("Please select a To State from the right grid.")
 					l_info_dlg.show_relative_to_window (main_window)
@@ -181,29 +183,24 @@
 
 feature {NONE} -- Implemention
 
-	update_grid_increased_content
+	update_grid_increased_content( a_grid_data_increased : attached like grid_data_increased)
 			-- Show the increased objects in the bottom result grid.
-		require
-			set: attached grid_data_increased
 		local
 			l_int: INTEGER
 			l_item: EV_GRID_LABEL_ITEM
 			l_i: INTEGER
-			l_grid_data_increased: like grid_data_increased
 		do
 			from
-				l_grid_data_increased := grid_data_increased
-				check attached l_grid_data_increased end -- Implied by precondition `set'
-				l_grid_data_increased.start
+				a_grid_data_increased.start
 			until
-				l_grid_data_increased.after
+				a_grid_data_increased.after
 			loop
-				if not filter.filter_class (l_grid_data_increased.item_for_iteration.text) then
+				if not filter.filter_class (a_grid_data_increased.item_for_iteration.text) then
 					l_i := l_i + 1
-					create l_item.make_with_text (l_grid_data_increased.item_for_iteration.text)
+					create l_item.make_with_text (a_grid_data_increased.item_for_iteration.text)
 					l_item.set_pixmap (icons.object_grid_class_icon)
 					grid_changed.set_item (1, l_i, l_item)
-					l_int := l_grid_data_increased.item_for_iteration.nb
+					l_int := a_grid_data_increased.item_for_iteration.nb
 					create l_item.make_with_text (l_int.out)
 					if l_int > 0 then
 						l_item.set_foreground_color (increased_color)
@@ -212,7 +209,7 @@
 					end
 					grid_changed.set_item (2, l_i, l_item)
 				end
-				l_grid_data_increased.forth
+				a_grid_data_increased.forth
 			end
 		end
 
@@ -273,33 +270,27 @@
 					sorted_column := a_column_index
 					sorting_order := False
 				end
-				if grid_data_increased /= Void then
-					sort_data
-					update_grid_increased_content
+				if attached grid_data_increased as l_grid_data_increased then
+					sort_data( l_grid_data_increased)
+					update_grid_increased_content (l_grid_data_increased)
 				end
 			end
 		end
 
-	handle_pick_item (a_item: EV_GRID_LABEL_ITEM): MA_CLASS_STONE
-			-- User pick a item from grid to filter.
-		local
-			l_result: detachable like handle_pick_item
+
+	handle_pick_item (a_item: detachable EV_GRID_ITEM): detachable MA_CLASS_STONE
+			-- User pick an item from grid to filter.
 		do
-			if a_item /= Void and a_item.column.index = 1 then
-				l_result := create {MA_CLASS_STONE}.make (a_item.text)
+			if attached {EV_GRID_LABEL_ITEM} a_item as l_label and then l_label.column.index = 1 then
+			   create {MA_CLASS_STONE} Result.make (l_label.text)
 			end
-			check attached l_result end -- FIXME: Implied by ...?
-			Result := l_result
 		end
 
-	sort_data
+	sort_data (a_grid_data_increased : attached like grid_data_increased)
 			-- Sort `grid_data' according to `sorted_column' and `sorting_order'.
-		require
-			set: attached grid_data_increased
 		local
 			l_sorter: QUICK_SORTER [like grid_data_increased_row]
 			l_agent_sorter: AGENT_EQUALITY_TESTER [like grid_data_increased_row]
-			l_grid_data_increased: like grid_data_increased
 		do
 			inspect
 				sorted_column
@@ -307,9 +298,7 @@
 			when 2 then create l_agent_sorter.make (agent sort_on_count)
 			end
 			create l_sorter.make (l_agent_sorter)
-			l_grid_data_increased := grid_data_increased
-			check attached l_grid_data_increased end -- Implied by precondition
-			l_sorter.sort (l_grid_data_increased)
+			l_sorter.sort (a_grid_data_increased)
 		end
 
 	sorting_order: BOOLEAN
@@ -348,13 +337,11 @@
 			-- Anchor type should not called.
 			-- first INTEGER is increased object count, second INTEGER is the increased objects type id
 		require
-			False
-		local
-			l_result: detachable like grid_data_increased_row
+			not_callable : False
 		do
-			check False end -- Anchor type only
-			check attached l_result end -- Satisfy void-safe compiler
-			Result := l_result
+			check False then end
+		ensure
+			for_typing_only : False
 		end
 
 	grid_data_increased: detachable ARRAYED_LIST [like grid_data_increased_row]
@@ -367,13 +354,11 @@
 			-- Type for the data inserted in grid
 			-- It is [Object Type Name, Eiffel Memory Used, C Memory Used, TypeId].
 		require
-			False
-		local
-			l_result: detachable like row_data
+			not_callable : False
 		do
-			check False end -- Anchor type only
-			check attached l_result end -- Satisfy void-safe compiler
-			Result := l_result
+			check False then end
+		ensure
+			for_typing_only : False
 		end
 
 	grid_from_state, grid_to_state: EV_GRID -- Two grid show states.
@@ -393,7 +378,7 @@
 	grid_increased_not_void: grid_changed /= Void
 	grid_data_not_void: grid_data /= Void
 note
-	copyright:	"Copyright (c) 1984-2013, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software
Index: ma_memory_state.e
===================================================================
--- ma_memory_state.e	(revision 95541)
+++ ma_memory_state.e	(working copy)
@@ -47,14 +47,12 @@
 
 	item_found_count: INTEGER
 			-- after routine found_type, return the count of founded item
-		require
-			founded_type_not_void: founded_type /= Void
-		local
-			l_item_founded: like item_founded
 		do
-			l_item_founded := item_founded
-			check l_item_founded /= Void end -- Implied by precondition
-			Result := l_item_founded.count_in_system
+			if attached item_founded as l_item_founded then
+				Result := l_item_founded.count_in_system
+			end
+		ensure
+			 item_found_count_non_negative: Result >= 0
 		end
 
 	memory_used_eiffel: INTEGER
@@ -163,12 +161,12 @@
 
 	state: TUPLE [type_name: STRING; count_in_system: INTEGER]
 			-- [type_name_of_type, number of instances of type_name_of_type present in system]
-		local
-			l_result: detachable like state
+		require
+			not_callable : False
 		do
-			check False end -- Anchor type only
-			check l_result /= void end -- Satisfy void-safe compiler
-			Result := l_result
+			check False then end
+		ensure
+			for_typing_only : False
 		end
 
 	objects_states: ARRAYED_LIST [like state];
@@ -175,14 +173,14 @@
 			-- the count the objects, first argument is type name, second argument is the object instances count
 
 note
-	copyright:	"Copyright (c) 1984-2006, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
-			 Eiffel Software
-			 356 Storke Road, Goleta, CA 93117 USA
-			 Telephone 805-685-1006, Fax 805-685-6869
-			 Website http://www.eiffel.com
-			 Customer support http://support.eiffel.com
+			Eiffel Software
+			5949 Hollister Ave., Goleta, CA 93117 USA
+			Telephone 805-685-1006, Fax 805-685-6869
+			Website http://www.eiffel.com
+			Customer support http://support.eiffel.com
 		]"
 
 
Index: ma_object_snapshot_mediator.e
===================================================================
--- ma_object_snapshot_mediator.e	(revision 95541)
+++ ma_object_snapshot_mediator.e	(working copy)
@@ -114,8 +114,7 @@
 
 				l_count := l_new_table.item_for_iteration
 
-				if finding_route_to_once then
-					check attached l_map end -- Implied by `finding_route_to_once'
+				if l_map /= Void then
 					add_to_reference_table (l_new_table.key_for_iteration, l_map)
 				end
 
@@ -151,7 +150,7 @@
 				end
 			end
 
-			if finding_route_to_once then
+			if l_map /= Void then
 				memory.collection_on
 				last_selected_object := Void
 			end
@@ -158,8 +157,9 @@
 
 			last_table := l_new_table
 			grid_data := l_data
-
-			update_grid_content
+			if attached grid_data as l_grid_data then
+				update_grid_content (l_grid_data)
+			end
 		end
 
 	set_finding_route_to_once (a_b: BOOLEAN)
@@ -212,21 +212,18 @@
 					sorted_column := a_column_index
 					sorting_order := False
 				end
-				if grid_data /= Void then
-					sort_data
-					update_grid_content
+				if attached grid_data as l_grid_data then
+					sort_data (l_grid_data)
+					update_grid_content (l_grid_data)
 				end
 			end
 		end
 
-	sort_data
+	sort_data( a_grid_data : attached like grid_data)
 			-- Sort `grid_data' according to `sorted_column' and `sorting_order'.
-		require
-			grid_data_not_void: grid_data /= Void
 		local
 			l_sorter: QUICK_SORTER [like row_data]
 			l_agent_sorter: AGENT_EQUALITY_TESTER [like row_data]
-			l_grid_data: like grid_data
 		do
 			inspect
 				sorted_column
@@ -235,17 +232,12 @@
 				when 3 then create l_agent_sorter.make (agent sort_on_delta)
 			end
 			create l_sorter.make (l_agent_sorter)
-			l_grid_data := grid_data
-			check attached l_grid_data end -- Implied by precondition
-			l_sorter.sort (l_grid_data)
+			l_sorter.sort (a_grid_data)
 		end
 
-	update_grid_content
-			-- Fill grid using `grid_data'
-		require
-			grid_data_not_void: grid_data /= Void
+	update_grid_content ( a_grid_data : attached like grid_data)
+			-- Fill grid using `a_grid_data'
 		local
-			l_data: like grid_data
 			l_row_data: like row_data
 			l_item: MA_GRID_LABEL_ITEM
 			i, l_count, l_delta: INTEGER
@@ -254,16 +246,14 @@
 			l_grid: like object_grid
 		do
 			from
-				l_data := grid_data
 				l_grid := object_grid
 				grid_util.grid_remove_and_clear_all_rows (l_grid)
 				i := 1
-				check attached l_data end -- Implied by precondition `grid_data_not_void'
-				l_data.start
+				a_grid_data.start
 			until
-				l_data.after
+				a_grid_data.after
 			loop
-				l_row_data := l_data.item_for_iteration
+				l_row_data := a_grid_data.item_for_iteration
 				if not filter.filter_class (l_row_data.type_name) then
 					l_str := l_row_data.type_name
 					check
@@ -298,7 +288,7 @@
 					end
 					i := i + 1
 				end
-				l_data.forth
+				a_grid_data.forth
 			end
 				-- We launch a collection, so that no bad information is displayed
 				-- for referers.
@@ -448,101 +438,91 @@
 	add_to_reference_table (a_object_id: INTEGER; a_map: HASH_TABLE [ARRAYED_LIST [ANY], INTEGER_32])
 			-- Added all referer relations of objects of `a_object_id'.
 		require
-			tables_created: reference_table /= Void and name_table /= Void
 			a_map_not_void: a_map /= Void
 			has: a_map.has (a_object_id)
-			set: attached object_table
-			set: attached name_table
-			set: attached reference_table
 		local
 			l_name, l_field_name: STRING
 			l_int: INTERNAL
-			l_objects_of_type: detachable ARRAYED_LIST [ANY]
 			l_index: NATURAL
 			l_item: ANY
 			l_referee: detachable ANY
 			l_field_count: INTEGER
 			i: INTEGER
-			l_object_table: like object_table
-			l_name_table: like name_table
-			l_reference_table: like reference_table
 		do
 			create l_int
 			l_name := l_int.type_name_of_type (a_object_id)
-			l_objects_of_type := a_map.item (a_object_id)
-			check attached l_objects_of_type end -- Implied by precondition `has'
-			l_object_table := object_table
-			check attached l_object_table end -- Implied by precondition `set'
-			l_reference_table := reference_table
-			check attached l_reference_table end -- Implied by precondition `set'						
 
-			from
-				l_objects_of_type.start
-			until
-				l_objects_of_type.after
-			loop
-				l_item := l_objects_of_type.item
-				l_index := l_object_table.index (l_item)
-				if last_selected_object /= Void and then l_item = last_selected_object then
-					selected_index := l_index
-					last_selected_object := Void
-				end
-					--| Fixme: we don't know whether it is an once object or not.
-				l_name_table := name_table
-				check attached l_name_table end -- Implied by precondition `set'
-				l_name_table.put (l_name, l_index)
-				check
-					not l_name_table.conflict
-				end
-				if attached {SPECIAL [detachable ANY]} l_item as l_special then
-					l_field_name := once "(special_field)"
-					from
-						i := l_special.lower
-					until
-						i > l_special.upper
-					loop
-						l_referee := l_special.item (i)
-						if l_referee /= Void then
-							l_reference_table.extend (l_index, l_object_table.index (l_referee), l_field_name)
-						end
-						i := i + 1
+			if attached a_map.item (a_object_id) as l_objects_of_type  and attached object_table as l_object_table and attached reference_table as l_reference_table then
+				from
+					l_objects_of_type.start
+				until
+					l_objects_of_type.after
+				loop
+					l_item := l_objects_of_type.item
+					l_index := l_object_table.index (l_item)
+					if last_selected_object /= Void and then l_item = last_selected_object then
+						selected_index := l_index
+						last_selected_object := Void
 					end
-				elseif attached {TUPLE} l_item as l_tuple then
-					l_field_name := once "(tuple_field)"
-					from
-						i := l_tuple.lower
-					until
-						i > l_tuple.upper
-					loop
-						l_referee := l_tuple.item (i)
-						if l_referee /= Void then
-							l_reference_table.extend (l_index, l_object_table.index (l_referee), l_field_name)
+						--| Fixme: we don't know whether it is an once object or not.
+					if attached name_table as l_name_table then
+						l_name_table.put (l_name, l_index)
+						check
+							not l_name_table.conflict
 						end
-						i := i + 1
-					end
-				else
-					from
-						l_field_count := l_int.field_count_of_type (a_object_id)
-						i := 1
-					until
-						i > l_field_count or l_item = Current
-					loop
-						l_referee := l_int.field (i, l_item)
-						if l_referee /= Void then
-							l_field_name := l_int.field_name (i, l_item)
-							l_reference_table.extend (l_index, l_object_table.index (l_referee), l_field_name)
+						if attached {SPECIAL [detachable ANY]} l_item as l_special then
+							l_field_name := once "(special_field)"
+							from
+								i := l_special.lower
+							until
+								i > l_special.upper
+							loop
+								l_referee := l_special.item (i)
+								if attached l_referee then
+									l_reference_table.extend (l_index, l_object_table.index (l_referee), l_field_name)
+								end
+								i := i + 1
+							end
+						elseif attached {TUPLE} l_item as l_tuple then
+							l_field_name := once "(tuple_field)"
+							from
+								i := l_tuple.lower
+							until
+								i > l_tuple.upper
+							loop
+								l_referee := l_tuple.item (i)
+								if l_referee /= Void then
+									l_reference_table.extend (l_index, l_object_table.index (l_referee), l_field_name)
+								end
+								i := i + 1
+							end
+						else
+							from
+								l_field_count := l_int.field_count_of_type (a_object_id)
+								i := 1
+							until
+								i > l_field_count or l_item = Current
+							loop
+								l_referee := l_int.field (i, l_item)
+								if l_referee /= Void then
+									l_field_name := l_int.field_name (i, l_item)
+									l_reference_table.extend (l_index, l_object_table.index (l_referee), l_field_name)
+								end
+								i := i + 1
+							end
 						end
-						i := i + 1
+					else
+						check attached_l_name_table : false end -- Implied by precondition `set'
 					end
+					l_objects_of_type.forth
 				end
-				l_objects_of_type.forth
+			else
+				check has_object: False end
 			end
 		end
 
 	build_once_object_table
 			-- Record once object in `once_object_table'.
-		require
-			set: attached object_table
 		local
 			l_obj: like once_objects
 			i: INTEGER
@@ -550,25 +530,24 @@
 			l_index: like selected_index
 			l_int: INTERNAL
 			l_once_object_table: like once_object_table
-			l_object_table: like object_table
 		do
-			create l_int
-			create l_once_object_table.make (100)
-			once_object_table := l_once_object_table
-			l_obj := once_objects
-			from
-				i := l_obj.lower
-			until
-				i > l_obj.upper
-			loop
-				l_item := l_obj.item (i)
-				if l_item /= Void then
-					l_object_table := object_table
-					check attached l_object_table end -- Implied by precondition `set'
-					l_index := l_object_table.index (l_item)
-					l_once_object_table.force (l_index, l_index)
+			if attached object_table as l_object_table then
+				create l_int
+				create l_once_object_table.make (100)
+				once_object_table := l_once_object_table
+				l_obj := once_objects
+				from
+					i := l_obj.lower
+				until
+					i > l_obj.upper
+				loop
+					l_item := l_obj.item (i)
+					if l_item /= Void then
+							l_index := l_object_table.index (l_item)
+							l_once_object_table.force (l_index, l_index)
+					end
+					i := i + 1
 				end
-				i := i + 1
 			end
 		end
 
@@ -599,14 +578,15 @@
 	row_data: TUPLE [type_name: STRING; number_of_objects: INTEGER; variation_since_last_time: INTEGER; type_id: INTEGER]
 			-- Type for the data inserted in `output_grid'
 			-- It is [type_name, number_of_objects, variation_since_last_time, type_id].
-		local
-			l_result: detachable like row_data
+		require
+			not_callable : False
 		do
-			check False end -- Anchor type only
-			check attached l_result end -- Satisfy void-safe compiler
-			Result := l_result
+			check False then end
+		ensure
+			for_typing_only : False
 		end
 
+
 	object_grid: EV_GRID
 			-- the main grid to show object snapshot datas
 
@@ -720,7 +700,7 @@
 	object_grid_not_void: object_grid /= Void
 
 note
-	copyright:	"Copyright (c) 1984-2012, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software
Index: ma_references_table.e
===================================================================
--- ma_references_table.e	(revision 95541)
+++ ma_references_table.e	(working copy)
@@ -67,14 +67,11 @@
 		local
 			l_hash: detachable like references_by_referee
 		do
-			if not relations.has_key (a_referee) then
-				create l_hash.make (20)
-					-- Here we prevent extending pairs exsited or with equivalent key and value.
-				relations.force (l_hash, a_referee)
-			else
-				l_hash := relations.found_item
+			l_hash := relations.item (a_referee)
+			if l_hash = Void then
+			  create l_hash.make (20)
+			  relations.force (l_hash, a_referee)
 			end
-			check l_hash /= Void end -- Implied by previous if clause
 			l_hash.force ([a_referee, data], a_referrer)
 		end
 
@@ -81,7 +78,7 @@
 feature -- Removal
 
 	remove (a_referrer: G; a_referee: H)
-			-- Remove relation between `'a_referrer' and `a_referee'.
+			-- Remove relation between `'a_referrer' and `a_referee' if it exists a relation.
 		require
 			a_referrer_not_void: a_referrer /= Void
 			a_referee_not_void: a_referee /= Void
@@ -88,9 +85,8 @@
 		local
 			l_hash: detachable like references_by_referee
 		do
-			if relations.has_key (a_referee) then
-				l_hash := relations.found_item
-				check l_hash /= Void end -- Implied by `has_key'
+			l_hash := relations.item (a_referee)
+			if  l_hash /= Void then
 				l_hash.remove (a_referrer)
 				if l_hash.is_empty then
 					relations.remove (a_referee)
@@ -103,14 +99,14 @@
 	relations: HASH_TABLE [like references_by_referee, H];
 
 note
-	copyright:	"Copyright (c) 1984-2006, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
-			 Eiffel Software
-			 356 Storke Road, Goleta, CA 93117 USA
-			 Telephone 805-685-1006, Fax 805-685-6869
-			 Website http://www.eiffel.com
-			 Customer support http://support.eiffel.com
+			Eiffel Software
+			5949 Hollister Ave., Goleta, CA 93117 USA
+			Telephone 805-685-1006, Fax 805-685-6869
+			Website http://www.eiffel.com
+			Customer support http://support.eiffel.com
 		]"
 
 end
Index: ma_route_to_once_searcher.e
===================================================================
--- ma_route_to_once_searcher.e	(revision 95541)
+++ ma_route_to_once_searcher.e	(working copy)
@@ -40,8 +40,8 @@
 													%Please select a start point in Object Grid%N%
 													%and refresh again with Collecting Statics enabled.")
 				l_info_box.show
-			else
-				build
+			elseif attached reference_table as l_reference_table then
+				build (l_reference_table)
 			end
 		end
 
@@ -84,71 +84,81 @@
 			l_grid: like grid
 			l_route_stack: like route_stack
 		do
-			if attached grid then
-				l_grid := grid
-			else
+			l_grid := grid
+			if l_grid = Void then
 				create l_grid
 				grid := l_grid
 				init_grid (l_grid)
 				result_panel.extend (l_grid)
 			end
-			check l_grid /= Void end -- Implied by previous if clause
 			l_column := l_grid.column_count + 1
 			l_route_stack := route_stack
-			check attached l_route_stack end -- Implied by precondition `set'
-			l_array := l_route_stack.linear_representation
-			l_grid.set_row_count_to (l_array.count.max (l_grid.row_count))
-			l_grid.set_column_count_to (l_column)
-			l_grid.column (l_column).set_title ("Route" + l_column.out)
-			from
-				l_array.start
-			until
-				l_array.after
-			loop
-				if not l_array.islast then
-					l_next_index := l_array [l_array.index + 1]
-				else
-					l_last := True
-				end
-				if not l_last then
-					l_reference_table := reference_table
-					check l_reference_table /= Void end -- Implied by precondition `set'
-					l_tuple := l_reference_table.references_by_referee (l_next_index).item (l_array.item)
-					if l_tuple /= Void then
-						if attached {STRING} l_tuple.data as l_string then
-							l_field_name := l_string
+			if attached l_route_stack as l_r then
+				l_array := l_r.linear_representation
+				l_grid.set_row_count_to (l_array.count.max (l_grid.row_count))
+				l_grid.set_column_count_to (l_column)
+				l_grid.column (l_column).set_title ("Route" + l_column.out)
+				from
+					l_array.start
+				until
+					l_array.after
+				loop
+					if not l_array.islast then
+						l_next_index := l_array [l_array.index + 1]
+					else
+						l_last := True
+					end
+					if not l_last then
+						l_reference_table := reference_table
+						if attached l_reference_table as l_ref then
+							l_tuple := l_ref.references_by_referee (l_next_index).item (l_array.item)
 						else
-								--|FIXME: 2012/04/06 Shouldn't this be "(unknown)", instead of setting it Void? See review#7644004.
-							l_field_name := Void
+							check attached_l_reference_table : false end -- Implied by precondition `set'
 						end
+						if l_tuple /= Void then
+							if attached {STRING} l_tuple.data as l_string then
+								l_field_name := l_string
+							else
+									--|FIXME: 2012/04/06 Shouldn't this be "(unknown)", instead of setting it Void? See review#7644004.
+								l_field_name := Void
+							end
+						else
+							l_field_name := once "(unknown)"
+						end
 					else
-						l_field_name := once "(unknown)"
+							--|FIXME: 2012/04/06 Shouldn't this be "(unknown)", instead of setting it Void? See review#7644004.
+						l_field_name := Void
 					end
-				else
-						--|FIXME: 2012/04/06 Shouldn't this be "(unknown)", instead of setting it Void? See review#7644004.
-					l_field_name := Void
+					if l_field_name = Void then
+						l_field_name := once ""
+					else
+						l_field_name := l_field_name.twin
+						l_field_name.prepend (".")
+					end
+						-- Optimization, since we know that only the first object is once object.
+					if l_array.isfirst then
+						l_once := once "*"
+					else
+						l_once := once ""
+					end
+					l_name_table := name_table
+					if attached l_name_table as l_n then
+						l_name_table_item := l_n.item (l_array.item)
+						if attached l_name_table_item as l_name_item then
+							l_text := l_once + l_array.item.out + once ": {" + l_name_item + once "}" + l_field_name
+							create l_item.make_with_text (l_text)
+							l_item.set_tooltip (l_text)
+							l_grid.set_item (l_column, l_array.index, l_item)
+							l_array.forth
+						else
+							check attached_l_name_table_item : false end -- FIXME: Implied by ...?
+						end
+					else
+						check attached_l_name_table : false end -- Implied by precondition `set'
+					end
 				end
-				if l_field_name = Void then
-					l_field_name := once ""
-				else
-					l_field_name := l_field_name.twin
-					l_field_name.prepend (".")
-				end
-					-- Optimization, since we know that only the first object is once object.
-				if l_array.isfirst then
-					l_once := once "*"
-				else
-					l_once := once ""
-				end
-				l_name_table := name_table
-				check l_name_table /= Void end -- Implied by precondition `set'
-				l_name_table_item := l_name_table.item (l_array.item)
-				check l_name_table_item /= Void end -- FIXME: Implied by ...?
-				l_text := l_once + l_array.item.out + once ": {" + l_name_table_item + once "}" + l_field_name
-				create l_item.make_with_text (l_text)
-				l_item.set_tooltip (l_text)
-				l_grid.set_item (l_column, l_array.index, l_item)
-				l_array.forth
+			else
+				check attached_l_route_stack : false end -- Implied by precondition `set'
 			end
 		end
 
@@ -173,25 +183,21 @@
 			-- Support Copy.
 		require
 			a_key_not_void: a_key /= Void
-			grid_set: attached grid
 		local
 			l_env: EV_ENVIRONMENT
-			l_grid: like grid
 		do
-			create l_env
-			if attached l_env.application as l_app and then l_app.ctrl_pressed then
-				inspect a_key.code
-				when {EV_KEY_CONSTANTS}.key_a then
-					l_grid := grid
-					check l_grid /= Void end -- Implied by precondition `grid_set'
-					select_all_row (l_grid)
-				when {EV_KEY_CONSTANTS}.key_c then
-					l_grid := grid
-					check l_grid /= Void end -- Implied by precondition `grid_set'					
-					if not l_grid.selected_items.is_empty then
-						copy_selected_items (l_grid)
+			if attached grid as l_grid then
+				create l_env
+				if attached l_env.application as l_app and then l_app.ctrl_pressed then
+					inspect a_key.code
+					when {EV_KEY_CONSTANTS}.key_a then
+						select_all_row (l_grid)
+					when {EV_KEY_CONSTANTS}.key_c then
+						if not l_grid.selected_items.is_empty then
+							copy_selected_items (l_grid)
+						end
+					else
 					end
-				else
 				end
 			end
 		end
@@ -307,20 +313,17 @@
 
 feature {NONE} -- Implementation
 
-	build
+	build ( a_reference_table : attached like reference_table)
 			-- Build route.
-		require
-			set: attached reference_table
 		local
-			l_reference_table: like reference_table
 			l_route_stack: like route_stack
+			l_visited_references : attached like visited_references
 		do
 			create l_route_stack.make (1000)
 			route_stack := l_route_stack
-			l_reference_table := reference_table
-			check l_reference_table /= Void end -- Implied by precondition `set'
-			create visited_references.make (l_reference_table.referee_count)
-			if deep_visit_node (start_index) then
+			create l_visited_references.make (a_reference_table.referee_count)
+			visited_references := l_visited_references
+			if deep_visit_node (start_index, a_reference_table, l_route_stack, l_visited_references) then
 				-- Found route
 				check
 					route_stack_not_empty: not l_route_stack.is_empty
@@ -347,64 +350,59 @@
 
 feature {NONE} -- Implementation
 
-	deep_visit_node (a_referee: like start_index): BOOLEAN
+	deep_visit_node (a_referee: like start_index;
+					 a_reference_table : attached like reference_table;
+					 a_route_stack  : attached like route_stack;
+					 a_visited_references  : attached like visited_references): BOOLEAN
 			-- Deep visit a node, Ture is found once object.
 		require
-			set: attached reference_table
-			set: attached route_stack
-			set: attached visited_references
+			set: attached a_reference_table.references_by_referee (a_referee)
 		local
-			l_all_referrers, l_visited_referrers: HASH_TABLE [TUPLE [like start_index, detachable ANY], like start_index]
+			l_visited_referrers: HASH_TABLE [TUPLE [like start_index, detachable ANY], like start_index]
 			l_referrer: like start_index
 			l_all_referrers_count: INTEGER
-			l_visited_references: like visited_references
-			l_reference_table: like reference_table
-			l_route_stack: like route_stack
 		do
-			if is_visited (a_referee) then
+			if is_visited (a_referee, a_route_stack) then
 				Result := False
 			else
-				l_route_stack := route_stack
-				check l_route_stack /= Void end -- Implied by precondition `set'
-				l_route_stack.put (a_referee)
-				l_reference_table := reference_table
-				check l_reference_table /= Void end -- Implied by precondition `set'
-				l_all_referrers := l_reference_table.references_by_referee (a_referee)
-				l_all_referrers_count := l_all_referrers.count
-				if l_all_referrers_count = 0 then
-						-- We reach the end. No referrer.
-					if is_once_object (a_referee) then
+				a_route_stack.put (a_referee)
+				if attached a_reference_table.references_by_referee (a_referee) as l_all_referrers  then
+					l_all_referrers_count := l_all_referrers.count
+					if l_all_referrers_count = 0 then
+							-- We reach the end. No referrer.
+						if is_once_object (a_referee) then
+							Result := True
+						else
+							Result := False
+						end
+					elseif is_once_object (a_referee) then
 						Result := True
 					else
-						Result := False
-					end
-				elseif is_once_object (a_referee) then
-					Result := True
-				else
-					l_visited_references := visited_references
-					check attached l_visited_references end -- Implied by precondition `set'
-					l_visited_referrers := l_visited_references.references_by_referee (a_referee)
-					if l_all_referrers_count = l_visited_referrers.count then
-							-- Go back one
-						Result := False
-						l_route_stack.remove
-					else
-						from
-							l_all_referrers.start
-						until
-							l_all_referrers.after or Result
-						loop
-							l_referrer := l_all_referrers.key_for_iteration
-							if not l_visited_referrers.has_key (l_referrer) then
-								l_visited_references.extend (l_referrer, a_referee, Void)
-								Result := deep_visit_node (l_referrer)
+						l_visited_referrers := a_visited_references.references_by_referee (a_referee)
+						if l_all_referrers_count = l_visited_referrers.count then
+								-- Go back one
+							Result := False
+							a_route_stack.remove
+						else
+							from
+								l_all_referrers.start
+							until
+								l_all_referrers.after or Result
+							loop
+								l_referrer := l_all_referrers.key_for_iteration
+								if not l_visited_referrers.has_key (l_referrer) then
+									a_visited_references.extend (l_referrer, a_referee, Void)
+									Result := deep_visit_node (l_referrer, a_reference_table, a_route_stack, a_visited_references)
+								end
+								l_all_referrers.forth
 							end
-							l_all_referrers.forth
+							if not Result then
+								a_route_stack.remove
+							end
 						end
-						if not Result then
-							l_route_stack.remove
-						end
 					end
+				else
+					check attached_l_reference_table_references_by_referee : false end -- Implied by precondition `set'
 				end
 			end
 		end
@@ -430,28 +428,18 @@
 			end
 		end
 
-	is_visited (a_node: like start_index): BOOLEAN
+	is_visited (a_node: like start_index; a_route_stack : attached like route_stack): BOOLEAN
 			-- Is `a_node' visited?
-		require
-			set: attached route_stack
-		local
-			l_route_stack: like route_stack
 		do
-			l_route_stack := route_stack
-			check l_route_stack /= Void end -- Implied by precondition `set'
-			Result := l_route_stack.has (a_node)
+			Result := a_route_stack.has (a_node)
 		end
 
 	is_once_object (a_object: like start_index): BOOLEAN
 			-- Is `a_object' once?
-		require
-			set: attached once_objects_table
-		local
-			l_table: like once_objects_table
 		do
-			l_table := once_objects_table
-			check attached l_table end -- Implied by precondition `set'
-			Result := l_table.has (a_object)
+			if attached once_objects_table as l_table  then
+				Result := l_table.has (a_object)
+			end
 		end
 
 	route_stack: detachable ARRAYED_STACK [like start_index]
@@ -465,7 +453,7 @@
 	result_panel_not_void: result_panel /= Void
 
 note
-	copyright:	"Copyright (c) 1984-2012, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software
Index: memory_analyzer-safe.ecf
===================================================================
--- memory_analyzer-safe.ecf	(revision 95541)
+++ memory_analyzer-safe.ecf	(working copy)
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="ISO-8859-1"?>
-<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-10-0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.eiffel.com/developers/xml/configuration-1-10-0 http://www.eiffel.com/developers/xml/configuration-1-10-0.xsd" name="memory_analyzer" uuid="BF699013-E4A2-4C7F-AA12-4376BEA92D93" library_target="memory_analyzer">
+<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-12-0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.eiffel.com/developers/xml/configuration-1-12-0 http://www.eiffel.com/developers/xml/configuration-1-12-0.xsd" name="memory_analyzer" uuid="BF699013-E4A2-4C7F-AA12-4376BEA92D93" library_target="memory_analyzer">
 	<target name="memory_analyzer">
 		<description>Memory analyzer library: Track down your memory usage within your application.
       Copyright (c) 1984-2006, Eiffel Software and others.
@@ -12,7 +12,7 @@
 		</option>
 		<library name="base" location="$ISE_LIBRARY\library\base\base-safe.ecf"/>
 		<library name="base_extension" location="$ISE_LIBRARY\library\base_extension\base_extension-safe.ecf"/>
-		<library name="graph" location="$ISE_LIBRARY\library\graph\graph-safe.ecf"/>
+		<library name="graph" location="C:\Users\andersoxie\Documents\GitHub\EG-complete-safe\graph-safe.ecf"/>
 		<library name="time" location="$ISE_LIBRARY\library\time\time-safe.ecf"/>
 		<library name="vision2" location="$ISE_LIBRARY\library\vision2\vision2-safe.ecf"/>
 		<cluster name="memory_analyzer" location=".\"/>
Index: memory_analyzer.ecf
===================================================================
--- memory_analyzer.ecf	(revision 95541)
+++ memory_analyzer.ecf	(working copy)
@@ -1,12 +1,14 @@
 <?xml version="1.0" encoding="ISO-8859-1"?>
-<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-10-0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.eiffel.com/developers/xml/configuration-1-10-0 http://www.eiffel.com/developers/xml/configuration-1-10-0.xsd" name="memory_analyzer" uuid="BF699013-E4A2-4C7F-AA12-4376BEA92D93" library_target="memory_analyzer">
+<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-12-0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.eiffel.com/developers/xml/configuration-1-12-0 http://www.eiffel.com/developers/xml/configuration-1-12-0.xsd" name="memory_analyzer" uuid="BF699013-E4A2-4C7F-AA12-4376BEA92D93" library_target="memory_analyzer">
 	<target name="memory_analyzer">
-		<description>Memory analyzer library: Track down your memory usage within your application.&#10;      Copyright (c) 1984-2006, Eiffel Software and others.&#10;      Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt).</description>
+		<description>Memory analyzer library: Track down your memory usage within your application.
+      Copyright (c) 1984-2006, Eiffel Software and others.
+      Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt).</description>
 		<root all_classes="true"/>
 		<file_rule>
 			<exclude>/\.svn</exclude>
 		</file_rule>
-		<option warning="true" is_attached_by_default="false" syntax="standard">
+		<option warning="true" full_class_checking="false" is_attached_by_default="false" void_safety="none" syntax="standard">
 		</option>
 		<library name="base" location="$ISE_LIBRARY\library\base\base.ecf"/>
 		<library name="base_extension" location="$ISE_LIBRARY\library\base_extension\base_extension.ecf"/>
Index: object_graph/ma_figure_factory.e
===================================================================
--- object_graph/ma_figure_factory.e	(revision 95541)
+++ object_graph/ma_figure_factory.e	(working copy)
@@ -14,33 +14,30 @@
 feature -- Basic operations
 
 	new_node_figure (a_node: EG_NODE): EG_LINKABLE_FIGURE
-			-- Create a node figure for `a_node'.
+			-- <Precursor>
 		do
 			Result := create {MA_OBJECT_NODE}.make_with_model (a_node)
 		end
 
 	new_cluster_figure (a_cluster: EG_CLUSTER): EG_CLUSTER_FIGURE
-			-- Create a cluster figure for `a_cluster'.
+			-- <Precursor>
 		do
 			Result := create {EG_SIMPLE_CLUSTER}.make_with_model (a_cluster)
 		end
 
-	new_link_figure (a_link: EG_LINK): EG_LINK_FIGURE
-			-- Create a link figure for `a_link'.
+	new_link_figure (a_link: EG_LINK; a_source, a_target: EG_LINKABLE_FIGURE): EG_LINK_FIGURE
+			-- <Precursor>
 		do
-			Result := create {MA_REFERENCE_LINK}.make_with_model (a_link)
+			Result := create {MA_REFERENCE_LINK}.make (a_link, a_source, a_target)
 		end
 
-	model_from_xml (node: attached like xml_element_type): EG_ITEM
-			-- Create an EG_ITEM from `node' if possible.
+	model_from_xml (node: like xml_element_type): EG_ITEM
+			-- <Precursor>
 		local
 --			node_name, source_name, target_name: STRING
 --			a_source, a_target: EG_LINKABLE
-			l_result: detachable like model_from_xml
 		do
-			check not_implemented: False end
-			check attached l_result end -- Satisfy void-safe compiler
-			Result := l_result
+			check not_implemented: False then end
 --			node_name := node.name
 --			if node_name.is_equal ("ELLIPSE_NODE") then
 --				create {EG_NODE} Result
@@ -63,14 +60,14 @@
 		end
 
 note
-	copyright:	"Copyright (c) 1984-2006, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
-			 Eiffel Software
-			 356 Storke Road, Goleta, CA 93117 USA
-			 Telephone 805-685-1006, Fax 805-685-6869
-			 Website http://www.eiffel.com
-			 Customer support http://support.eiffel.com
+			Eiffel Software
+			5949 Hollister Ave., Goleta, CA 93117 USA
+			Telephone 805-685-1006, Fax 805-685-6869
+			Website http://www.eiffel.com
+			Customer support http://support.eiffel.com
 		]"
 
 
Index: object_graph/ma_object_graph_mediator.e
===================================================================
--- object_graph/ma_object_graph_mediator.e	(revision 95541)
+++ object_graph/ma_object_graph_mediator.e	(working copy)
@@ -60,33 +60,25 @@
 			end
 		end
 
-	find_draw_node_by_object (a_object: ANY): EG_NODE
+	find_draw_node_by_object (a_object: ANY): detachable EG_NODE
 			-- Find in `objects_already_draw' return a EG_NODE which corresponding to object.
 		require
 			a_object_not_void : a_object /= Void
 		local
 			l_obj_with_node : TUPLE [obj: ANY; node: EG_NODE]
-			l_result: detachable like find_draw_node_by_object
 		do
 			from
 				objects_already_draw.start
 			until
-				l_result /= Void or objects_already_draw.after
+				Result /= Void or objects_already_draw.after
 			loop
 				l_obj_with_node := objects_already_draw.item_for_iteration
 					-- Test the address.
 				if l_obj_with_node.obj = a_object then
-					l_result := l_obj_with_node.node
-					check
-						result_not_void: l_result /= Void
-					end
+					Result := l_obj_with_node.node
 				end
 				objects_already_draw.forth
 			end
-			check attached l_result end -- FIXME: Implied by ...?
-			Result := l_result
-		ensure
-			result_not_void : Result /= Void
 		end
 
 	object_already_draw (a_object: ANY): BOOLEAN
@@ -172,26 +164,30 @@
 			graph.add_node (l_last_drawn_node)
 
 			fig := world.figure_from_model (l_last_drawn_node)
-			check attached fig end -- Implied by `l_last_drawn_node' has been just added
-			fig.set_point_position (ax, ay)
+			if attached fig as l_fig then
 
-			-- Make new node figure a drop target
-			fig.set_accept_cursor (accept_node)
-			fig.set_deny_cursor (deny_node)
---			fig.drop_actions.extend (agent on_link_drop (?, last_drawn_node))
+				l_fig.set_point_position (ax, ay)
 
-			-- Make new node figure pickable
---			fig.set_pebble (create {NODE_STONE}.make (last_drawn_node))
+				-- Make new node figure a drop target
+				l_fig.set_accept_cursor (accept_node)
+				l_fig.set_deny_cursor (deny_node)
+	--			l_fig.drop_actions.extend (agent on_link_drop (?, last_drawn_node))
 
-			fig.pointer_button_release_actions.extend (agent on_select_node)
-			l_tuple := [a_object, l_last_drawn_node]
-			check
-				a_object /= Void
-				last_drawn_node /= Void
+				-- Make new node figure pickable
+	--			l_fig.set_pebble (create {NODE_STONE}.make (last_drawn_node))
+
+				l_fig.pointer_button_release_actions.extend (agent on_select_node)
+				l_tuple := [a_object, l_last_drawn_node]
+				check
+					a_object /= Void
+					last_drawn_node /= Void
+				end
+				world.update
+				-- Put the object and the node into the hashtable
+				objects_already_draw.force (l_tuple, l_fig)
+			else
+				check attached_fig : false end -- Implied by `l_last_drawn_node' has been just added
 			end
-			world.update
-			-- Put the object and the node into the hashtable
-			objects_already_draw.force (l_tuple, fig)
 		end
 
 	on_select_node (a_x: INTEGER; a_y: INTEGER; a_button: INTEGER; a_x_tilt: DOUBLE; a_y_tilt: DOUBLE; a_pressure: DOUBLE; a_screen_x: INTEGER; a_screen_y: INTEGER)
@@ -234,6 +230,9 @@
 
 	find_refers
 			-- Find the refers to current slected node and draw the nodes which refer to it.
+		require
+			figures_exists: world.selected_figures.count > 0
+			attached_item : attached objects_already_draw.item (world.selected_figures.first)
 		local
 			l_nodes: ARRAYED_LIST [EG_FIGURE]
 			l_node: EG_FIGURE
@@ -240,7 +239,6 @@
 			l_object: ANY
 			l_refers: SPECIAL [ANY]
 			l_int,refer_count: INTEGER
-			l_link_node: EG_NODE
 			l_linkable: EG_LINKABLE
 			l_info_dlg: EV_INFORMATION_DIALOG
 			l_item: detachable TUPLE [obj: ANY; node: EG_NODE]
@@ -247,11 +245,10 @@
 			l_last_drawn_node: like last_drawn_node
 		do
 			l_nodes := world.selected_figures
-			if l_nodes.count > 0 then
-				l_node := l_nodes.first
-				l_item := objects_already_draw.item (l_node)
-				check attached l_item end -- FIXME: Implied by ...?
-				l_object :=	l_item.obj
+			l_node := l_nodes.first
+			l_item := objects_already_draw.item (l_node)
+			if attached l_item as l_i then
+				l_object :=	l_i.obj
 				l_refers := memory.referers (l_object)
 				from
 					l_int := 0
@@ -261,31 +258,40 @@
 				loop
 					if object_already_draw(l_refers.item (l_int))  then
 						-- add link to two already drawed object
-						l_link_node := find_draw_node_by_object(l_refers.item (l_int))
-						l_item := objects_already_draw.item (l_node)
-						check attached l_item end -- FIXME: Implied by ...?
-						l_linkable := l_item.node
-						check
-							l_linkable /= Void
+						if attached find_draw_node_by_object(l_refers.item (l_int)) as  l_link_node then
+							l_item := objects_already_draw.item (l_node)
+							if attached l_item as l_it then
+								l_linkable := l_it.node
+								check
+									l_linkable /= Void
+								end
+								add_link (l_linkable, l_link_node )
+							else
+								check attached_l_item : false end -- FIXME: Implied by that we iterate over the available number of items.
+							end
 						end
-						add_link (l_linkable, l_link_node )
 					else
 						add_node_random_pos(l_refers.item (l_int))
 						l_item := objects_already_draw.item (l_node)
-						check attached l_item end -- FIXME: Implied by ...?
-						l_linkable := l_item.node
-						check
-							l_linkable /= Void
+						if attached l_item as l_it then
+							l_linkable := l_it.node
+							check
+								l_linkable /= Void
+							end
+							l_last_drawn_node := last_drawn_node
+							if attached l_last_drawn_node as l_last then
+								add_link (l_linkable, l_last)
+							else
+								check attachedl_last_drawn_node : false end -- FIXME: Implied by ...?
+							end
+						else
+							check attached_l_item : false end -- Implied by that we iterate over the available number of items.
 						end
-						l_last_drawn_node := last_drawn_node
-						check attached l_last_drawn_node end -- FIXME: Implied by ...?
-						add_link (l_linkable, l_last_drawn_node)
 					end
 					l_int := l_int + 1
 				end
 			else
-				create l_info_dlg.make_with_text ("Please select a node first.")
-				l_info_dlg.show_relative_to_window (main_window)
+				check attached_l_item : false  end
 			end
 			world.update
 		end
@@ -441,6 +447,9 @@
 		once
 			create Result.make
 		end
+feature
+	objects_already_draw: HASH_TABLE [TUPLE [obj: ANY; node: EG_NODE], EG_FIGURE]
+			-- Objects which is already draw on the graph, ANY is the object which EG_NODE is correspond to
 
 feature {NONE} -- Fields
 
@@ -456,13 +465,12 @@
 	last_drawn_node: detachable EG_NODE
 			--Node which was just drawed
 
-	objects_already_draw: HASH_TABLE [TUPLE [obj: ANY; node: EG_NODE], EG_FIGURE]
-			-- Objects which is already draw on the graph, ANY is the object which EG_NODE is correspond to
-
 	object_drawing : EV_FRAME
 			-- Place this class to draw graphics of objects
+feature
 	world: EG_FIGURE_WORLD
 			-- World allowing to manipulate the graph.
+feature {NONE}
 	model_cell: MA_WORLD_CELL
 			-- Cell allowing to edit the graph.
 	graph: EG_GRAPH
@@ -486,7 +494,7 @@
 	objects_already_draw_has_no_void_item: True-- No Void items in `objects_already_draw'
 
 note
-	copyright:	"Copyright (c) 1984-2012, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software
Index: object_graph/ma_object_node.e
===================================================================
--- object_graph/ma_object_node.e	(revision 95541)
+++ object_graph/ma_object_node.e	(working copy)
@@ -21,9 +21,6 @@
 create
 	make_with_model
 
-create {MA_OBJECT_NODE}
-	make_filled
-
 feature {NONE} -- Initialization
 
 	default_create
@@ -60,7 +57,7 @@
 
 feature -- Access
 
-	model: detachable EG_NODE
+	model: EG_NODE
 			-- Model `Current' is a view for.
 
 	port_x: INTEGER
@@ -178,7 +175,7 @@
 	new_filled_list (n: INTEGER): like Current
 			-- New list with `n' elements.
 		do
-			create Result.make_filled (n)
+			check unimplemented: False then end
 		end
 
 invariant
@@ -185,14 +182,14 @@
 	node_figure_not_void: node_figure /= Void
 
 note
-	copyright:	"Copyright (c) 1984-2006, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
-			 Eiffel Software
-			 356 Storke Road, Goleta, CA 93117 USA
-			 Telephone 805-685-1006, Fax 805-685-6869
-			 Website http://www.eiffel.com
-			 Customer support http://support.eiffel.com
+			Eiffel Software
+			5949 Hollister Ave., Goleta, CA 93117 USA
+			Telephone 805-685-1006, Fax 805-685-6869
+			Website http://www.eiffel.com
+			Customer support http://support.eiffel.com
 		]"
 
 
Index: object_graph/ma_reference_link.e
===================================================================
--- object_graph/ma_reference_link.e	(revision 95541)
+++ object_graph/ma_reference_link.e	(working copy)
@@ -16,10 +16,10 @@
 		end
 
 create
-	make_with_model
+	make
 
 create {MA_REFERENCE_LINK}
-	make_filled
+	make_resized_from
 
 feature {NONE} -- Initialization
 
@@ -34,13 +34,15 @@
 			extend (line)
 		end
 
-	make_with_model (a_model: EG_LINK)
-			-- Make a link using `a_model'.
+	make (a_model: EG_LINK; a_source, a_target: like source)
+			-- Make a link using `a_model' as `model', `a_source' as `source' and `a_target' as `target'.
 		require
 			a_model_not_void: a_model /= Void
 		do
+			model := a_model
+			source := a_source
+			target := a_target
 			default_create
-			model := a_model
 			initialize
 
 			if a_model.is_directed then
@@ -56,8 +58,27 @@
 			disable_rotating
 
 			update
+		ensure
+			model_set: model = a_model
+			source_set: source = a_source
+			target_set: target = a_target
+			moving_disabled: not is_moving
+			scaling_disabled: not is_scaling
+			rotating_disabled: not is_rotating
 		end
 
+	make_resized_from (a_other: like Current; n: INTEGER)
+			-- Make a link using `a_other'
+			-- and resize the freshly created area with a count of `n'.
+		do
+			make (a_other.model, a_other.source, a_other.target)
+			area_v2 := area_v2.resized_area (n)
+		ensure
+			same_model: model = a_other.model
+			same_source_and_target: source = a_other.source and target = a_other.target
+			area_count: area_v2.count = n
+		end
+
 feature -- Access
 
 	set_color
@@ -73,7 +94,7 @@
 		end
 
 	xml_node_name: STRING
-			-- Name of `xml_element'.
+			-- <Precursor>
 		do
 			Result := "EG_SIMPLE_LINK"
 		end
@@ -99,16 +120,13 @@
 feature {EG_FIGURE, EG_FIGURE_WORLD} -- Update
 
 	update
-			-- Some properties may have changed.
+			-- <Precursor>
 		local
 			p1, p2: EV_COORDINATE
 			an_angle: DOUBLE
 			source_size: EV_RECTANGLE
-			l_model: like model
 		do
-			l_model := model
-			check attached l_model end -- FIXME: Implied by ...?
-			if not l_model.is_reflexive then
+			if not model.is_reflexive then
 				if attached source as l_source and then attached target as l_target then
 					p1 := line.point_array.item (0)
 					p2 := line.point_array.item (1)
@@ -150,7 +168,7 @@
 feature {NONE} -- Implementation
 
 	set_is_selected (an_is_selected: like is_selected)
-			-- Set `is_selected' to `an_is_selected'.
+			-- <Precursor>
 		do
 			is_selected := an_is_selected
 		end
@@ -162,9 +180,9 @@
 			-- The ellipse used when link `is_reflexive'.
 
 	on_is_directed_change
-			-- `model'.`is_directed' changed.
+			-- <Precursor>
 		do
-			if attached model as l_model and then l_model.is_directed then
+			if model.is_directed then
 				line.enable_end_arrow
 			else
 				line.disable_end_arrow
@@ -173,26 +191,25 @@
 			line.center_invalidate
 		end
 
-feature {NONE} -- Implementation
-
 	new_filled_list (n: INTEGER): like Current
-			-- New list with `n' elements.
+			-- <Precursor>
 		do
-			create Result.make_filled (n)
+			create Result.make_resized_from (Current, n)
 		end
 
 invariant
 	line_not_void: line /= Void
+	mdeol_not_void: model /= Void
 
 note
-	copyright:	"Copyright (c) 1984-2006, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
-			 Eiffel Software
-			 356 Storke Road, Goleta, CA 93117 USA
-			 Telephone 805-685-1006, Fax 805-685-6869
-			 Website http://www.eiffel.com
-			 Customer support http://support.eiffel.com
+			Eiffel Software
+			5949 Hollister Ave., Goleta, CA 93117 USA
+			Telephone 805-685-1006, Fax 805-685-6869
+			Website http://www.eiffel.com
+			Customer support http://support.eiffel.com
 		]"
 
 
Index: singletons/ma_icons_singleton.e
===================================================================
--- singletons/ma_icons_singleton.e	(revision 95541)
+++ singletons/ma_icons_singleton.e	(working copy)
@@ -34,13 +34,13 @@
 
 	pixmap_path: PATH
 			-- Path containing all of the Memory Analyzer icons
-		local
-			l_result: like internal_pixmap_path
-		do
-			l_result := internal_pixmap_path
-			check attached l_result end -- FIXME: Implied by ...?
+	do
+		if attached internal_pixmap_path as l_result then
 			Result := l_result
+		else
+			create Result.make_current
 		end
+	end
 
 	internal_pixmap_path: detachable like pixmap_path
 			-- Path where have icons image.
@@ -263,7 +263,7 @@
 			-- Icon names
 
 note
-	copyright:	"Copyright (c) 1984-2012, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software
Index: singletons/ma_shared_pixmap_factory.e
===================================================================
--- singletons/ma_shared_pixmap_factory.e	(revision 95541)
+++ singletons/ma_shared_pixmap_factory.e	(working copy)
@@ -82,7 +82,6 @@
 		deferred
 		ensure
 			result_not_void: Result /= Void
-			not_result_is_empty: not Result.is_empty
 		end
 
 	image_matrix: EV_PIXMAP
@@ -100,8 +99,11 @@
 			result_compares_objects: Result.object_comparison
 		end
 
+
+
+
 note
-	copyright:	"Copyright (c) 1984-2012, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software
Index: singletons/ma_singleton_factory.e
===================================================================
--- singletons/ma_singleton_factory.e	(revision 95541)
+++ singletons/ma_singleton_factory.e	(working copy)
@@ -73,12 +73,13 @@
 			-- MEMORY_TOOL_WINDOW instance
 		require
 			set: is_main_window_set
-		local
-			l_item: detachable MA_WINDOW
 		do
-			l_item := internal_main_window.item
-			check attached l_item end -- Implied by precondition
-			Result := l_item
+			if attached internal_main_window.item as l_item then
+				Result := l_item
+			else
+				check l_item_attached : false end -- Implied by precondition
+				create Result.make ("")  -- Since the behaviour is undefined when precondition is not satisfied we are allowed to return an undefined window.
+			end
 		ensure
 			result_not_void: Result /= Void
 		end
@@ -235,14 +236,14 @@
 	internal_main_window_not_void: internal_main_window /= Void
 
 note
-	copyright:	"Copyright (c) 1984-2008, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
-			 Eiffel Software
-			 356 Storke Road, Goleta, CA 93117 USA
-			 Telephone 805-685-1006, Fax 805-685-6869
-			 Website http://www.eiffel.com
-			 Customer support http://support.eiffel.com
+			Eiffel Software
+			5949 Hollister Ave., Goleta, CA 93117 USA
+			Telephone 805-685-1006, Fax 805-685-6869
+			Website http://www.eiffel.com
+			Customer support http://support.eiffel.com
 		]"
 
 end
Index: widgets/ma_constants_imp.e
===================================================================
--- widgets/ma_constants_imp.e	(revision 95541)
+++ widgets/ma_constants_imp.e	(working copy)
@@ -453,8 +453,12 @@
 			l_item: detachable STRING
 		do
 			l_item := all_constants.item (a_name)
-			check l_item /= Void end -- Implied by precondition `has_constant'
-			Result := l_item.twin
+			if attached l_item as l_i then
+				Result := l_item.twin
+			else
+				check l_item_attached : false end -- Implied by precondition `has_constant'
+				create Result.make_empty -- Since the behaviour is undefined when precondition is not satisfied we are allowed to return an empty string
+			end
 		ensure
 			Result_not_void: Result /= Void
 		end
@@ -470,8 +474,12 @@
 			l_item: detachable STRING
 		do
 			l_item := all_constants.item (a_name)
-			check l_item /= Void end -- Implied by precondition `has_constant'
-			l_string := l_item.twin
+			if attached l_item as l_i then
+				l_string := l_item.twin
+			else
+				check l_item_attached : false end -- Implied by precondition `has_constant'
+				create l_string.make_empty -- Since the behaviour is undefined when precondition is not satisfied we are allowed to return 0
+			end
 			check
 				is_integer: l_string.is_integer
 			end
@@ -580,14 +588,14 @@
 	all_constants_not_void: all_constants /= Void
 
 note
-	copyright:	"Copyright (c) 1984-2008, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
-			 Eiffel Software
-			 356 Storke Road, Goleta, CA 93117 USA
-			 Telephone 805-685-1006, Fax 805-685-6869
-			 Website http://www.eiffel.com
-			 Customer support http://support.eiffel.com
+			Eiffel Software
+			5949 Hollister Ave., Goleta, CA 93117 USA
+			Telephone 805-685-1006, Fax 805-685-6869
+			Website http://www.eiffel.com
+			Customer support http://support.eiffel.com
 		]"
 
 end -- class MA_CONSTANTS_IMP
Index: widgets/ma_filter_window.e
===================================================================
--- widgets/ma_filter_window.e	(revision 95541)
+++ widgets/ma_filter_window.e	(working copy)
@@ -182,13 +182,18 @@
 		local
 			l_last_row: detachable EV_GRID_ROW
 		do
-			add_new_row (Void)
+			add_new_row (Void) -- Construct a new row where the first item is editable.
 			l_last_row := grid.last_visible_row
-			check attached l_last_row end -- FIXME: Implied by ...?
-			if attached {EV_GRID_EDITABLE_ITEM} l_last_row.item (1) as l_item then
-				l_item.activate
+			if attached l_last_row as l_last_r then
+				if attached {EV_GRID_EDITABLE_ITEM} l_last_row.item (1) as l_item then
+					l_item.activate
+				else
+					check not_editable_item: False end
+					-- FIXMED: Implied by ...? Do we miss a precondition or invariant?
+				end
 			else
-				check not_editable_item: False end
+				check l_last_row_attached : false end
+				-- FIXME: Implied by ...? Do we miss a precondition or invariant?			
 			end
 		end
 
@@ -291,13 +296,11 @@
 	a_filter_data: TUPLE [class_name: STRING; selected: BOOLEAN; description: STRING]
 			-- A anchor, should not be called
 		require
-			False
-		local
-			l_result: detachable like a_filter_data
+			not_callable : False
 		do
-			check False end -- Anchor type only
-			check attached l_result end -- Satisfy void-safe compiler
-			Result := l_result
+			check False then end
+		ensure
+			for_typing_only : False
 		end
 
 	hash_table_datas_to_arrayed_list_datas: MA_ARRAYED_LIST_STORABLE [like a_filter_data]
@@ -354,7 +357,7 @@
 	grid_not_void: grid /= Void
 
 note
-	copyright:	"Copyright (c) 1984-2012, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software
Index: widgets/ma_grid_check_box_item.e
===================================================================
--- widgets/ma_grid_check_box_item.e	(revision 95541)
+++ widgets/ma_grid_check_box_item.e	(working copy)
@@ -21,7 +21,7 @@
 			-- Creation method.
 		do
 			create selected_changed_actions
-			
+
 			default_create
 			expose_actions.extend (agent draw_overlay_pixmap)
 			pointer_button_press_actions.force_extend (agent handle_pointer_pressed)
@@ -94,30 +94,28 @@
 			-- Draw the pixmap which represent whether current is selected.
 		require
 			a_drawable_not_void: a_drawable /= Void
-		local
-			l_parent_2: detachable EV_CONTAINER
 		do
-			if is_selected and attached parent as l_parent then
-				if l_parent.has_focus then
-					a_drawable.set_foreground_color (l_parent.focused_selection_color)
+			if attached parent as l_parent then
+				if is_selected then
+					if l_parent.has_focus then
+						a_drawable.set_foreground_color (l_parent.focused_selection_color)
+					else
+						a_drawable.set_foreground_color (l_parent.non_focused_selection_color)
+					end
 				else
-					a_drawable.set_foreground_color (l_parent.non_focused_selection_color)
+					if attached row.background_color as l_row_background_color then
+						a_drawable.set_foreground_color (l_row_background_color)
+					else
+						a_drawable.set_foreground_color (l_parent.background_color)
+					end
 				end
-			else
-				if attached row.background_color as l_row_background_color then
-					a_drawable.set_foreground_color (l_row_background_color)
+				a_drawable.fill_rectangle (0, 0, a_drawable.width, a_drawable.height)
+				if internal_selected then
+					draw_selected (a_drawable)
 				else
-					l_parent_2 := parent
-					check attached l_parent_2 end -- FIXME: Implied by ...?
-					a_drawable.set_foreground_color (l_parent_2.background_color)
+					draw_unselected (a_drawable)
 				end
 			end
-			a_drawable.fill_rectangle (0, 0, a_drawable.width, a_drawable.height)
-			if internal_selected then
-				draw_selected (a_drawable)
-			else
-				draw_unselected (a_drawable)
-			end
 		end
 
 	draw_selected (a_drawable: EV_DRAWABLE)
@@ -242,14 +240,14 @@
 	selected_changed_actions_not_void: selected_changed_actions /= Void
 
 note
-	copyright:	"Copyright (c) 1984-2006, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
-			 Eiffel Software
-			 356 Storke Road, Goleta, CA 93117 USA
-			 Telephone 805-685-1006, Fax 805-685-6869
-			 Website http://www.eiffel.com
-			 Customer support http://support.eiffel.com
+			Eiffel Software
+			5949 Hollister Ave., Goleta, CA 93117 USA
+			Telephone 805-685-1006, Fax 805-685-6869
+			Website http://www.eiffel.com
+			Customer support http://support.eiffel.com
 		]"
 
 
Index: widgets/ma_window.e
===================================================================
--- widgets/ma_window.e	(revision 95541)
+++ widgets/ma_window.e	(working copy)
@@ -60,8 +60,8 @@
 		do
 			set_main_window (Current)
 
-			attached_timer.actions.extend (agent timer_event)
-			attached_timer.set_interval (refresh_interval)
+			timer.actions.extend (agent timer_event)
+			timer.set_interval (refresh_interval)
 			main_book.drop_actions.extend (agent main_book_drop_pebble)
 			main_book.drop_actions.set_veto_pebble_function (agent main_book_dropable)
 
@@ -84,7 +84,7 @@
 			search_route_button.select_actions.extend (agent search_route)
 		ensure then
 			main_window_set: main_window_not_void
-			timer_action_set: attached_timer.actions.count > 0
+			timer_action_set: timer.actions.count > 0
 			notebook_drop_action_set: main_book.drop_actions.count > 0
 			update_interval_set_normal: refresh_interval = refresh_interval_normal
 			auto_refresh_button_selected: auto_refresh.is_selected
@@ -138,9 +138,9 @@
 	destroy
 			-- Destroy window, clear singleton.
 		do
-			attached_timer.set_interval (0)
-			attached_timer.actions.wipe_out
-			timer := Void
+			timer.set_interval (0)
+			timer.actions.wipe_out
+			timer.set_interval (0)
 			main_book.drop_actions.wipe_out
 			filter_setting.drop_actions.wipe_out
 			show_actions.wipe_out
@@ -199,14 +199,14 @@
 			-- Enable or disable auto refresh memory graph.
 		do
 			if auto_refresh.is_selected then
-				attached_timer.set_interval (refresh_interval)
+				timer.set_interval (refresh_interval)
 				auto_refresh.set_tooltip ("Auto refresh enabled")
 			else
-				attached_timer.set_interval (0)
+				timer.set_interval (0)
 				auto_refresh.set_tooltip ("Auto refresh disabled")
 			end
 		ensure then
-			timer_state_changed: old attached_timer.interval /= attached_timer.interval
+			timer_state_changed: old timer.interval /= timer.interval
 			auto_refresh_tooltip_changed: old auto_refresh.tooltip /= auto_refresh.tooltip
 		end
 
@@ -221,7 +221,7 @@
 				analyze_object_snap.set_finding_route_to_once (False)
 			end
 		ensure then
---			timer_state_changed: old attached_timer.interval /= attached_timer.interval
+--			timer_state_changed: old timer.interval /= timer.interval
 			auto_refresh_tooltip_changed: old auto_refresh.tooltip /= auto_refresh.tooltip
 		end
 
@@ -228,25 +228,25 @@
 	auto_refresh_change_speed
 			-- Change the refresh speed.
 		do
-			if attached_timer.interval /= 0 then
+			if timer.interval /= 0 then
 				inspect refresh_interval
 					when refresh_interval_low then
 						refresh_interval := refresh_interval_normal
-						attached_timer.set_interval (refresh_interval)
+						timer.set_interval (refresh_interval)
 						refresh_speed.set_tooltip ("Refresh speed is normal")
 					when refresh_interval_normal then
 						refresh_interval := refresh_interval_hi
-						attached_timer.set_interval (refresh_interval)
+						timer.set_interval (refresh_interval)
 						refresh_speed.set_tooltip ("Refresh speed is hi")
 					when refresh_interval_hi then
 						refresh_interval := refresh_interval_low
-						attached_timer.set_interval (refresh_interval)
+						timer.set_interval (refresh_interval)
 						refresh_speed.set_tooltip ("Refresh speed is low")
 				end
 			end
 		ensure then
-			refresh_speed_toollip_changed: attached_timer.interval /= 0 implies old refresh_speed.tooltip /= refresh_speed.tooltip
-			timer_interval_changed: attached_timer.interval /= 0 implies old attached_timer.interval /= attached_timer.interval
+			refresh_speed_toollip_changed: timer.interval /= 0 implies old refresh_speed.tooltip /= refresh_speed.tooltip
+			timer_interval_changed: timer.interval /= 0 implies old timer.interval /= timer.interval
 		end
 
 	arrange_circle_clicked
@@ -436,23 +436,9 @@
 	analyze_route_searcher: MA_ROUTE_TO_ONCE_SEARCHER
 			-- Searcher for routes to once object.
 
-	timer: detachable EV_TIMEOUT
+	timer:  EV_TIMEOUT
 			-- The timer used for update histogram and history.
 
-	attached_timer: EV_TIMEOUT
-			-- Attached `timer'
-		require
-			set: attached timer
-		local
-			l_result: like timer
-		do
-			l_result := timer
-			check attached l_result end -- Implied by precondition
-			Result := l_result
-		ensure
-			not_void: attached Result
-		end
-
 	refresh_interval: INTEGER
 			-- The time of interval between refersh.
 
@@ -482,7 +468,7 @@
 	main_book_has_tab_states_compare: main_book.has (tab_states_compare)
 
 note
-	copyright:	"Copyright (c) 1984-2012, Eiffel Software and others"
+	copyright:	"Copyright (c) 1984-2014, Eiffel Software and others"
 	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
 	source: "[
 			Eiffel Software
