-
Notifications
You must be signed in to change notification settings - Fork 0
/
memory_array.e
60 lines (48 loc) · 1.17 KB
/
memory_array.e
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
class
MEMORY_ARRAY [G -> MEMORY_STRUCTURE create make, make_by_pointer end]
create
make
feature {NONE}
make (a_count, a_item_size: INTEGER)
local
structure_size: INTEGER
zeroes: ARRAY [NATURAL_8]
do
count := a_count
item_size := a_item_size
-- Add one for the last NULL item
structure_size := (count + 1) * a_item_size
create representation.make (structure_size)
-- Fill with zero
create zeroes.make_filled (0, 1, structure_size)
representation.put_array (zeroes, 0)
-- Create instances
create instances.make_filled (create {G}.make, 1, count)
across
1 |..| count is i
loop
instances [i] := create {G}.make_by_pointer (representation.item + (i - 1) * a_item_size)
end
ensure
count = a_count
representation.count = (count + 1) * a_item_size
end
representation: MANAGED_POINTER
instances: ARRAY [G]
item_size: INTEGER
feature
count: INTEGER
item alias "[]" (a_index: INTEGER): G
require
a_index >= 1
a_index <= count
do
Result := instances [a_index]
end
pointer: POINTER
do
Result := representation.item
end
invariant
across instances is i all i.structure_size = item_size end
end