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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
with Ada.Text_IO; use Ada.Text_IO;
-- !! will disappear in favour of Ada.Exceptions
with Multi_precision_integers.IO;
package body Multi_precision_integers.Check is
package IOi renames Multi_precision_integers.IO;
-- Don't be afraid by the bug reporting tools,
-- they are unlikely to pop out of a programme ;-)
Bug_file: Ada.Text_IO.File_type;
Bug_file_name: constant String:= "mupreint.bug";
-- The flaw detection (DEBUG mode) could suffer from
-- a chicken-and-egg problem: e.g. "*" works, but the "/"
-- to verify it doesn't !
Multiply_flawed_div1_has_rest : exception;
Multiply_flawed_div1_wrong_quotient : exception;
Multiply_flawed_div2_has_rest : exception;
Multiply_flawed_div2_wrong_quotient : exception;
Div_Rem_flawed : exception;
procedure Open_Bug_Report is
begin
Create( Bug_file, out_file, Bug_file_name );
Put_Line( Bug_file, "Bug in Multi_precision_integers");
end Open_Bug_Report;
procedure Close_Bug_Report is
begin
Close( Bug_file );
-- These console messages can provoke a silent quit in GUI apps,
-- so we put them after closing the report.
Put_Line( "Bug in Multi_precision_integers !");
Put_Line( "For details, read file: " & Bug_file_name);
end Close_Bug_Report;
procedure Test( m: multi_int; test_last: Boolean:= True ) is
last_nz: index_int:= 0;
Negative_block,
Last_index_has_zero,
Field_last_outside_range, Field_last_is_negative: exception;
begin
if m.zero then return; end if; -- 0, nothing to test
if m.last_used > m.n then raise Field_last_outside_range; end if;
if m.last_used < 0 then raise Field_last_is_negative; end if;
for i in 0 .. m.last_used loop
if m.blk(i) < 0 then
raise Negative_block;
end if;
if m.blk(i) /= 0 then
last_nz:= i;
end if;
end loop;
if test_last and then 0 < last_nz and then last_nz < m.last_used then
raise Last_index_has_zero;
end if;
end Test;
procedure Check_Multiplication(i1,i2,i3: in multi_int) is
jeu: constant:= 5; -- 0 suffit
q1: Multi_int( i2.last_used + jeu );
r1: Multi_int( i1.last_used + i2.last_used + jeu );
q2: Multi_int( jeu );
r2: Multi_int( i2.last_used + jeu );
procedure Bug_Report is
begin
Open_Bug_Report;
Put_Line( Bug_file, "Multiply_and_verify");
Put( Bug_file, "i1 ="); IOi.Put_in_blocks(Bug_file, i1); New_Line(Bug_file);
Put( Bug_file, "i2 ="); IOi.Put_in_blocks(Bug_file, i2); New_Line(Bug_file);
Put( Bug_file, "i3 ="); IOi.Put_in_blocks(Bug_file, i3); New_Line(Bug_file);
end Bug_Report;
begin
Test(i1);
Test(i2);
if not (i1.zero or i2.zero) then
-- Now we divide i3 by i1, q1 should be = i2
Div_Rem_internal_both_export(i3,i1, q1,r1);
if not r1.zero then
Bug_Report;
Close_Bug_Report;
raise Multiply_flawed_div1_has_rest;
end if;
if not Equal( q1, i2 ) then
Bug_Report;
Put( Bug_file, "q1 ="); IOi.Put_in_blocks(Bug_file, q1); New_Line(Bug_file);
Close_Bug_Report;
raise Multiply_flawed_div1_wrong_quotient;
end if;
-- Now we divide q1 by i2, should be = 1
Div_Rem_internal_both_export(q1,i2, q2,r2);
if not r2.zero then
Bug_Report;
Close_Bug_Report;
raise Multiply_flawed_div2_has_rest;
end if;
if not Equal( q2, Multi(1) ) then
Bug_Report;
Put( Bug_file, "q2 ="); IOi.Put_in_blocks(Bug_file, q1); New_Line(Bug_file);
Close_Bug_Report;
raise Multiply_flawed_div2_wrong_quotient;
end if;
end if;
end Check_Multiplication;
procedure Check_Div_Rem(i1,i2,q,r: in multi_int) is
procedure Bug_Report is
begin
Open_Bug_Report;
Put_Line( Bug_file, "Div_Rem_and_verify");
Put( Bug_file, "i1 ="); IOi.Put_in_blocks(Bug_file, i1); New_Line(Bug_file);
Put( Bug_file, "i2 ="); IOi.Put_in_blocks(Bug_file, i2); New_Line(Bug_file);
Put( Bug_file, "q ="); IOi.Put_in_blocks(Bug_file, q); New_Line(Bug_file);
Put( Bug_file, "r ="); IOi.Put_in_blocks(Bug_file, r); New_Line(Bug_file);
end Bug_Report;
begin
Test(i1);
Test(i2);
if not Equal( i1, i2*q + r ) then
Bug_Report;
Close_Bug_Report;
raise Div_Rem_flawed;
end if;
Test(q);
Test(r);
end Check_Div_Rem;
end Multi_precision_integers.Check;
|
