indexing
description: "COM LARGE_INTEGER 64-bit integer"
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
class interface
ECOM_LARGE_INTEGER
create
make
ensure WEL_STRUCTURE
not_shared: not shared
make_from_pointer (a_pointer: POINTER)
require ECOM_STRUCTURE
valid_pointer: a_pointer /= default_pointer
make_from_integer (integer: INTEGER)
ensure
exists
feature
item: POINTER
WEL_ANY
quad_part: INTEGER_64
QuadPart
feature
structure_size: INTEGER
ensure WEL_STRUCTURE
positive_result: Result > 0
feature
exists: BOOLEAN
item
WEL_ANY
ensure WEL_ANY
Result = (item /= default_pointer)
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
feature
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
feature
dispose
Current
Current
WEL_ANY
feature
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
feature
initialize
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
initialize_with_character (a_character: CHARACTER)
a_character
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
memory_copy (source_pointer: POINTER; length: INTEGER)
lengthsource_pointeritem
WEL_STRUCTURE
require WEL_STRUCTURE
length_small_enough: length <= structure_size
length_large_enough: length > 0
exists: exists
feature
set_quad_part (a_quad_part: INTEGER_64)
quad_parta_quad_part
set_value (source: like Current)
ECOM_STRUCTURE
require ECOM_STRUCTURE
non_void: source /= void
valid_source: source.item /= default_pointer
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- ECOM_LARGE_INTEGER