Difference between revisions of "Void-Safe Library Results"
(→WEL) |
|||
| (5 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
List of bugs found by compiling our library in void-safe mode. | List of bugs found by compiling our library in void-safe mode. | ||
| + | |||
| + | ==EiffelTime== | ||
| + | * 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 | ||
| + | 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 | ||
| + | </e> | ||
| + | |||
| + | ==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== | ==WEL== | ||
| Line 5: | Line 29: | ||
<e> | <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> | ||
| + | |||
| + | * Call on Void target found in <e>{WEL_MSGBOXPARAMS}.make_by_id</e>, the code protected against `a_window' being Void but then in the final call still used `a_window' instead of the computed `handle': | ||
| + | |||
| + | <e> | ||
| + | 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)) | ||
</e> | </e> | ||
Latest revision as of 20:44, 3 February 2009
List of bugs found by compiling our library in void-safe mode.
Contents
EiffelTime
- Possible call on void target found in
{DATE_TIME_PARSER}.parse.code.item (i).count_maxwas 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_itembecause 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))
