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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
|
-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
--------------------------------------------------------------------------------
--Synopsis: --
-- --
--Procedure to analyse a .SIV file --
-- --
--------------------------------------------------------------------------------
separate (VCS)
procedure AnalyseSimplifiedVCFile
(Report_File : in SPARK_IO.File_Type;
Filename : in E_Strings.T;
VC_File_Date_Time : in E_Strings.T;
SIV_File_Date_Time : out E_Strings.T;
Error_In_SIV_File : out Boolean)
is
Bad_File_Format : Boolean := False;
Dummy_Close_Status : SPARK_IO.File_Status;
File_Line : E_Strings.T;
Finished_With_File : Boolean;
Open_Status : SPARK_IO.File_Status;
Process_Success : Boolean;
Read_Line_Success : Boolean;
Simplified_VC_File : SPARK_IO.File_Type := SPARK_IO.Null_File;
File_Status : File_Status_T;
Simplification_Date_Time : E_Strings.T;
VC_Generation_Date_Time_From_SIV_File : E_Strings.T;
Trimmed_Line : E_Strings.T;
Current_VC_Name : E_Strings.T;
-------------------------------------------------------------------------
-- NOTE, this procedure also removes the comma inserted in the string
-- by the simplifier
--
procedure Extract_Dates_And_Times_From_Simplified_VC_File
(Simplified_VC_File : in SPARK_IO.File_Type;
VC_Generation_Date_Time : out E_Strings.T;
Simplification_Date_Time : out E_Strings.T;
File_Status : out File_Status_T)
--# global in out SPARK_IO.File_Sys;
--# derives File_Status,
--# Simplification_Date_Time,
--# SPARK_IO.File_Sys,
--# VC_Generation_Date_Time from Simplified_VC_File,
--# SPARK_IO.File_Sys;
is
File_Line : E_Strings.T;
Trimmed_Line : E_Strings.T;
Gen_Date_Time : E_Strings.T;
Simp_Date_Time : E_Strings.T;
Subprogram_Found : Boolean := False;
begin
File_Status := Not_Corrupt;
VC_Generation_Date_Time := E_Strings.Empty_String;
Simplification_Date_Time := E_Strings.Empty_String;
--Check for completly empty file.
E_Strings.Get_Line (File => Simplified_VC_File,
E_Str => File_Line);
if E_Strings.Is_Empty (E_Str => File_Line) and SPARK_IO.End_Of_File (Simplified_VC_File) then
File_Status := Corrupt_Empty_File;
else
--Keep on reading from this file, until the desired information is retrieved
--or the end of the fikle is reached.
loop
Trimmed_Line := E_Strings.Trim (File_Line);
-- find date
-- (There is an implicit assumption that the date, if present, will appear
-- before the subprogram name.)
-- When the Examiner is in plain_output mode, the DATE line doesn't appear.
if E_Strings.Eq1_String (E_Str => E_Strings.Section (Trimmed_Line, 1, 7),
Str => "CREATED") then
-- extract the VC generation date and time from the string
Gen_Date_Time :=
E_Strings.Section (Trimmed_Line, SIV_File_VC_Generation_Date_Start_Column, SIV_File_VC_Generation_Date_Length);
E_Strings.Append_String (E_Str => Gen_Date_Time,
Str => " ");
E_Strings.Append_Examiner_String
(E_Str1 => Gen_Date_Time,
E_Str2 => E_Strings.Section
(Trimmed_Line,
SIV_File_VC_Generation_Time_Start_Column,
SIV_File_VC_Generation_Time_Length));
VC_Generation_Date_Time := Gen_Date_Time;
-- extract the simplification date and time from the string
Simp_Date_Time :=
E_Strings.Section (Trimmed_Line, SIV_File_Simplification_Date_Start_Column, SIV_File_Simplification_Date_Length);
E_Strings.Append_String (E_Str => Simp_Date_Time,
Str => " ");
E_Strings.Append_Examiner_String
(E_Str1 => Simp_Date_Time,
E_Str2 => E_Strings.Section
(Trimmed_Line,
SIV_File_Simplification_Time_Start_Column,
SIV_File_Simplification_Time_Length));
Simplification_Date_Time := Simp_Date_Time;
end if;
Subprogram_Found := Is_Valid_Subprogram (Trimmed_Line);
exit when (Subprogram_Found or SPARK_IO.End_Of_File (Simplified_VC_File));
E_Strings.Get_Line (File => Simplified_VC_File,
E_Str => File_Line);
end loop;
end if;
if (File_Status = Not_Corrupt) and not Subprogram_Found then
File_Status := Corrupt_Unknown_Subprogram;
end if;
-- if date has not been found must be in plain output mode
-- The above is a false assumption -- the file may just be corrupt. However, the
-- effect below of setting the string as unknown date is reasonable for both cases.
if E_Strings.Is_Empty (E_Str => VC_Generation_Date_Time) then
E_Strings.Append_String (E_Str => VC_Generation_Date_Time,
Str => Unknown_VCG_Date);
E_Strings.Append_String (E_Str => Simplification_Date_Time,
Str => Unknown_SIV_Date);
end if;
end Extract_Dates_And_Times_From_Simplified_VC_File;
-------------------------------------------------------------------------
-- look at the next non-blank line to see whether it starts
-- "*** true". If so the VC has been discharged. Otherwise, increment
-- the counter of undischarged VCs, and set the flag that an undischarged
-- VC has been found
procedure Process_New_Simplified_VC_Line
(Simplified_VC_File : in SPARK_IO.File_Type;
VC_Name : in E_Strings.T;
Success : out Boolean)
--# global in out FatalErrors.State;
--# in out SPARK_IO.File_Sys;
--# in out VCHeap.State;
--# derives FatalErrors.State,
--# VCHeap.State from *,
--# Simplified_VC_File,
--# SPARK_IO.File_Sys,
--# VCHeap.State,
--# VC_Name &
--# SPARK_IO.File_Sys,
--# Success from Simplified_VC_File,
--# SPARK_IO.File_Sys;
is
File_Line : E_Strings.T;
Read_Line_Success : Boolean;
begin
Read_Next_Non_Blank_Line (File => Simplified_VC_File,
Success => Read_Line_Success,
File_Line => File_Line);
if not Read_Line_Success then
Success := False;
else
Success := True;
if E_Strings.Eq1_String (E_Str => E_Strings.Section (File_Line, 1, 8),
Str => "*** true") then
if E_Strings.Eq1_String (E_Str => E_Strings.Section (File_Line, 15, 15),
Str => "* contradiction") then
VCHeap.Set_VC_State (VC_Name, VCDetails.VC_Proved_By_Contradiction);
elsif E_Strings.Eq1_String (E_Str => E_Strings.Section (File_Line, 15, 14),
Str => "* proved using") then
VCHeap.Set_VC_State (VC_Name, VCDetails.VC_Proved_Using_User_Proof_Rules);
elsif VCHeap.Get_VC_State (VC_Name) /= VCDetails.VC_Proved_By_Examiner then
VCHeap.Set_VC_State (VC_Name, VCDetails.VC_Proved_By_Inference);
end if;
elsif VCHeap.Get_VC_State (VC_Name) /= VCDetails.VC_Proved_By_Examiner then
-- The VC is undischarged if it has not been discharged by the
-- Examiner.
VCHeap.Set_VC_State (VC_Name, VCDetails.VC_Undischarged);
end if;
end if;
end Process_New_Simplified_VC_Line;
--------------------------------------------------------------------------
begin -- AnalyseSimplifiedVCFile
-- open simplified VC file
E_Strings.Open
(File => Simplified_VC_File,
Mode_Of_File => SPARK_IO.In_File,
Name_Of_File => Filename,
Form_Of_File => "",
Status => Open_Status);
if Open_Status /= SPARK_IO.Ok then
FatalErrors.Process (FatalErrors.Could_Not_Open_Input_File, E_Strings.Empty_String);
end if;
--No errors, until discover otherwise.
Error_In_SIV_File := False;
Extract_Dates_And_Times_From_Simplified_VC_File
(Simplified_VC_File => Simplified_VC_File,
VC_Generation_Date_Time => VC_Generation_Date_Time_From_SIV_File,
Simplification_Date_Time => Simplification_Date_Time,
File_Status => File_Status);
case File_Status is
when Not_Corrupt =>
null;
when Corrupt_Empty_File =>
SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "************* SIV file corrupt: empty file ************", 0);
SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
Error_In_SIV_File := True;
when Corrupt_Unknown_Subprogram =>
SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "************* SIV file corrupt: missing subprogram name ************", 0);
SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
Error_In_SIV_File := True;
end case;
--Only continue working on this file if an error has not been seen.
--(Previously POGS would attempt to work with corrupt files. This feature has the
-- capacity to produce confusing and wrong results.)
if not (Error_In_SIV_File) then
if CommandLine.Data.IgnoreDates
or else E_Strings.Eq_String (E_Str1 => VC_Generation_Date_Time_From_SIV_File,
E_Str2 => VC_File_Date_Time) then
if not CommandLine.Data.IgnoreDates then
SPARK_IO.New_Line (Report_File, 1);
SPARK_IO.Put_String (Report_File, "VCs simplified ", 0);
E_Strings.Put_Line (File => Report_File,
E_Str => Simplification_Date_Time);
end if;
-- find first non blank line
-- if we get to the end of the file first, flag a fatal error
Read_Next_Non_Blank_Line (File => Simplified_VC_File,
Success => Read_Line_Success,
File_Line => File_Line);
if not Read_Line_Success then
SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "************* SIV file corrupt: no data beyond header ************", 0);
SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
Bad_File_Format := True;
else
Finished_With_File := False;
-- process file line-by-line
-- on entry to the loop there is already a valid line in the
-- File_Line buffer
Current_VC_Name := E_Strings.Empty_String;
while not Finished_With_File loop
-- examine line and act accordingly
if Is_New_Range_Line (Line => File_Line) then
Append_Next_Line_From_File (Line => File_Line,
File => Simplified_VC_File);
elsif Is_New_VC_Line (Line => File_Line) then
Trimmed_Line := E_Strings.Trim (File_Line);
Current_VC_Name :=
E_Strings.Section
(E_Str => Trimmed_Line,
Start_Pos => 1,
Length => E_Strings.Get_Length (E_Str => Trimmed_Line) - 1);
Process_New_Simplified_VC_Line
(Simplified_VC_File => Simplified_VC_File,
VC_Name => Current_VC_Name,
Success => Process_Success);
if not Process_Success then
SPARK_IO.Put_String (Report_File, "*** Warning: Bad format in simplified VC file ***", 0);
Finished_With_File := True;
Bad_File_Format := True;
end if;
end if;
if not Finished_With_File then
-- read next line and check if VC has been proved false
Read_Next_Non_Blank_Line (File => Simplified_VC_File,
Success => Read_Line_Success,
File_Line => File_Line);
if Is_Trivially_False_VC (Line => File_Line) then
VCHeap.Set_VC_State (Current_VC_Name, VCDetails.VC_False);
end if;
-- if unsuccessful then check EOF
-- and set Finished_With_File accordingly
if not Read_Line_Success then
if SPARK_IO.End_Of_File (Simplified_VC_File) then
Finished_With_File := True;
else
FatalErrors.Process (FatalErrors.Problem_Reading_File, E_Strings.Empty_String);
end if;
end if;
end if;
end loop;
end if;
else
-- SIV file is out of date
SPARK_IO.New_Line (Report_File, 1);
SPARK_IO.Put_Line (Report_File, "*** Warning: Simplified VC file out of date ***", 0);
SPARK_IO.Put_String (Report_File, "VCs Generated: ", 0);
E_Strings.Put_String (File => Report_File,
E_Str => VC_File_Date_Time);
SPARK_IO.New_Line (Report_File, 1);
SPARK_IO.Put_String (Report_File, "SIV File Date: ", 0);
E_Strings.Put_String (File => Report_File,
E_Str => Simplification_Date_Time);
SPARK_IO.New_Line (Report_File, 1);
Bad_File_Format := True;
end if;
end if;
--# accept F, 10, Dummy_Close_Status, "Dummy_Close_Status unused here" &
--# F, 10, Simplified_VC_File, "Simplified_VC_File unused here";
SPARK_IO.Close (Simplified_VC_File, Dummy_Close_Status);
--# end accept;
SIV_File_Date_Time := Simplification_Date_Time;
--Either an error being raised, or a 'Bad_File_Format'
--being detected is an error.
Error_In_SIV_File := Error_In_SIV_File or Bad_File_Format;
--# accept F, 33, Dummy_Close_Status, "Dummy_Close_Status unused here";
end AnalyseSimplifiedVCFile;
|
