Void-Safe Library Results - Revision history

Ted at 04:44, 4 February 2009

2009-02-04T04:44:25Z

2009-02-03T18:02:59Z

‎EiffelWeb

2009-02-03T06:31:44Z

Added EiffelWeb example

2009-02-03T06:30:41Z

Cosmetics

2009-02-02T07:29:01Z

Added EiffelTime example

2009-01-22T18:25:05Z

More found bugs

2009-01-21T07:21:14Z

‎WEL

2009-01-21T07:20:43Z

‎WEL

2009-01-21T06:35:30Z

New page: List of bugs found by compiling our library in void-safe mode. ==WEL==

New page

List of bugs found by compiling our library in void-safe mode.

==WEL==

@@ Line 21: / Line 21: @@
 * In HTML_PAGE.out we did not satisfy the inherited postcondition that ensures Result is not Void.
 * A lot of missing precondition for checking arguments were not Void and thus putting the library at risk.
 ==WEL==

@@ Line 20: / Line 20: @@
 ==EiffelWeb==
 * In HTML_PAGE.out we did not satisfy the inherited postcondition that ensures Result is not Void.
 ==WEL==

@@ Line 17: / Line 17: @@
 end
 </e>
 ==WEL==

@@ Line 4: / Line 4: @@
 * Possible call on void target found in <e>{DATE_TIME_PARSER}.parse</e>. <e>code.item (i).count_max</e> was called but from the "if" clause followed, <e>code.item (i)</e> could be void.
 <e>
-	if has_seps then
+if has_seps then
-		pos2 := find_separator (s, pos1)
+	pos2 := find_separator (s, pos1)
-	else
+else
-		pos2 := (pos1 + 'code.item (i).count_max' - 1) * -1
+	pos2 := (pos1 + 'code.item (i).count_max' - 1) * -1
-	end
+end
-	extract_substrings (s, pos1, pos2)
+extract_substrings (s, pos1, pos2)
-	pos2 := abs (pos2)
+pos2 := abs (pos2)
-	if code.item (i) = Void then
+if code.item (i) = Void then
-		pos1 := s.count + 1
+	pos1 := s.count + 1
-	else
+else
-		...
+	...
-	end
+end
 </e>
 ==WEL==
 * Call on Void target found in <e>{WEL_TREE_VIEW}.insert_item</e> because there is no guarantee that `user_tree_view_item' will be attached in `an_item':

@@ Line 1: / Line 1: @@
 List of bugs found by compiling our library in void-safe mode.
 ==WEL==
 * Call on Void target found in <e>{WEL_TREE_VIEW}.insert_item</e> because there is no guarantee that `user_tree_view_item' will be attached in `an_item':

@@ Line 5: / Line 5: @@
 <e>
-	insert_item (an_item: WEL_TREE_VIEW_INSERT_STRUCT)
+insert_item (an_item: WEL_TREE_VIEW_INSERT_STRUCT)
-			-- Insert `an_item' in the tree.
+		-- Insert `an_item' in the tree.
-		require
+	require
-			exists: exists
+		exists: exists
-			an_item_not_void: an_item /= Void
+		an_item_not_void: an_item /= Void
-			an_item_exists: an_item.exists
+		an_item_exists: an_item.exists
-		local
+	local
-			l_user_item: WEL_TREE_VIEW_ITEM
+		l_user_item: WEL_TREE_VIEW_ITEM
-		do
+	do
-			last_item := {WEL_API}.send_message_result (item, Tvm_insertitem, to_wparam (0), an_item.item)
+		last_item := {WEL_API}.send_message_result (item, Tvm_insertitem,
-			an_item.tree_view_item.set_h_item (last_item)
+			to_wparam (0), an_item.item)
-			an_item.user_tree_view_item.set_h_item (last_item)
+		an_item.tree_view_item.set_h_item (last_item)
-		ensure
+		an_item.'user_tree_view_item.set_h_item (last_item)'
-			new_count: count = old count + 1
+	ensure
-		end
+		new_count: count = old count + 1
 </e>

@@ Line 2: / Line 2: @@
 ==WEL==
-* Call on Void target found in {WEL_TREE_VIEW}.insert_item because there is no guarantee that `user_tree_view_item' will be set in `an_item':
+* Call on Void target found in <e>{WEL_TREE_VIEW}.insert_item</e> because there is no guarantee that `user_tree_view_item' will be attached in `an_item':
 <e>

← Older revision		Revision as of 07:20, 21 January 2009
Line 2:		Line 2:

	==WEL==		==WEL==
		+	* Call on Void target found in {WEL_TREE_VIEW}.insert_item because there is no guarantee that `user_tree_view_item' will be set in `an_item':
		+
		+	<e>
		+	insert_item (an_item: WEL_TREE_VIEW_INSERT_STRUCT)
		+	-- Insert `an_item' in the tree.
		+	require
		+	exists: exists
		+	an_item_not_void: an_item /= Void
		+	an_item_exists: an_item.exists
		+	local
		+	l_user_item: WEL_TREE_VIEW_ITEM
		+	do
		+	last_item := {WEL_API}.send_message_result (item, Tvm_insertitem, to_wparam (0), an_item.item)
		+	an_item.tree_view_item.set_h_item (last_item)
		+	an_item.user_tree_view_item.set_h_item (last_item)
		+	ensure
		+	new_count: count = old count + 1
		+	end
		+	</e>