indexing
description: "Wrapper of FILETIME structure"
author: "Marina Nudelman"
date: "$Date$"
revision: "$Revision$"
class interface
WEL_FILE_TIME
create
make
item
WEL_STRUCTURE
ensure WEL_STRUCTURE
not_shared: not shared
make_by_pointer (a_pointer: POINTER)
itema_pointer
item
a_pointer
WEL_ANY
ensure WEL_ANY
item_set: item = a_pointer
shared: shared
make_by_current_time
ensure
initialized: item /= default_pointer
make_by_file_access_time (a_file: FILE)
a_file
require
non_void_file: a_file /= void
ensure
initialized: item /= default_pointer
make_by_file_modification_time (a_file: FILE)
a_file
require
non_void_file: a_file /= void
ensure
initialized: item /= default_pointer
make_by_file_creation_time (a_file: FILE)
a_file
require
non_void_file: a_file /= void
ensure
initialized: item /= default_pointer
feature
item: POINTER
WEL_ANY
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
local_file_time: WEL_FILE_TIME
Current
system_time: WEL_SYSTEM_TIME
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
universal_file_time: WEL_FILE_TIME
Current
feature
initialize
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
initialize_with_character (a_character: CHARACTER)
a_character
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
is_equal (a_file_time: WEL_FILE_TIME): BOOLEAN
a_file_timeCurrent
require ANY
other_not_void: other /= void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
is_larger_than (a_file_time: WEL_FILE_TIME): BOOLEAN
Currenta_file_time
require
non_default_item: item /= default_pointer
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
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_FILE_TIME