Void-Safe Library Results

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

EiffelTime

• Possible call on void target found in {DATE_TIME_PARSER}.parse. code.item (i).count_max was called but from the "if" clause followed, code.item (i) could be void.

if has_seps then
	pos2 := find_separator (s, pos1)
else
	pos2 := (pos1 + 'code.item (i).count_max' - 1) * -1
end
extract_substrings (s, pos1, pos2)
pos2 := abs (pos2)
if code.item (i) = Void then
	pos1 := s.count + 1
else
	...
end

EiffelWeb

• 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.

Eiffel2Java

• {JAVA_CLASS}.name, which could be void, was used in {JAVA_OBJECT} without protection.

WEL

• Call on Void target found in {WEL_TREE_VIEW}.insert_item because there is no guarantee that `user_tree_view_item' will be attached in `an_item':

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

• Call on Void target found in {WEL_MSGBOXPARAMS}.make_by_id, the code protected against `a_window' being Void but then in the final call still used `a_window' instead of the computed `handle':

if a_window /= Void then
	handle := a_window.item
else
	handle := default_pointer
end
structure_make
cwel_msgboxparams_set (item, 'a_window.item', a_main_arguments.resource_instance.item,
	a_wel_string1.item,
	a_wel_string2.item, a_style, cwin_make_int_resource (an_id),
	cwin_make_lang_id (a_language, a_sublanguage))