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 | ------------------------------------------------------------------------------
-- Copyright (C) 2020 by Heisenbug Ltd. (gh+spat@heisenbug.eu)
--
-- This work is free. You can redistribute it and/or modify it under the
-- terms of the Do What The Fuck You Want To Public License, Version 2,
-- as published by Sam Hocevar. See the LICENSE file for more details.
------------------------------------------------------------------------------
pragma License (Unrestricted);
------------------------------------------------------------------------------
--
-- SPARK Proof Analysis Tool
--
-- S.P.A.T. - Object representing the "timing" JSON object.
--
------------------------------------------------------------------------------
private with Ada.Tags;
with SPAT.Entity;
with SPAT.Field_Names;
with SPAT.Preconditions;
package SPAT.Timing_Item is
use all type GNATCOLL.JSON.JSON_Value_Type;
---------------------------------------------------------------------------
-- Has_Required_Fields
---------------------------------------------------------------------------
function Has_Required_Fields (Object : in JSON_Value;
Version : in File_Version) return Boolean
is
((case Version is
when GNAT_CE_2019 =>
Preconditions.Ensure_Field (Object => Object,
Field => Field_Names.Proof,
Kind => JSON_Float_Type),
-- Here, we don't really check for required fields anymore, there
-- is a whole bunch of items starting with "gnatwhy3.". If they are not
-- present that means the "corresponding phase wasn't run at all" (@kanigsson)
-- and we just assume 0.0 s.
when GNAT_CE_2020 =>
True) and
Preconditions.Ensure_Field (Object => Object,
Field => Field_Names.Flow_Analysis,
Kind => JSON_Float_Type));
-- Information obtained from the timing section of a .spark file.
type T is new Entity.T with private;
---------------------------------------------------------------------------
-- Create
---------------------------------------------------------------------------
not overriding
function Create (Object : in JSON_Value;
Version : in File_Version) return T with
Pre => Has_Required_Fields (Object => Object,
Version => Version);
---------------------------------------------------------------------------
-- Flow
---------------------------------------------------------------------------
not overriding
function Flow (This : in T) return Duration;
---------------------------------------------------------------------------
-- Proof
---------------------------------------------------------------------------
not overriding
function Proof (This : in T) return Duration;
---------------------------------------------------------------------------
-- Version
---------------------------------------------------------------------------
not overriding
function Version (This : in T) return File_Version;
None : constant T;
private
type T is new Entity.T with
record
Version : File_Version; -- version of file encountered.
-- FIXME: Storing the version here is a bit stupid. The only time
-- we need this, we also have a file name and makes much
-- more sense to store the version information there,
-- albeit maybe slightly more inefficient.
Proof : Duration; -- Total time the prover spent.
Flow : Duration; -- Total time of flow analysis.
end record;
---------------------------------------------------------------------------
-- Image
---------------------------------------------------------------------------
overriding
function Image (This : in T) return String is
(Ada.Tags.External_Tag (T'Class (This)'Tag) & ": (" &
"Version => " & This.Version'Image &
", Proof => " & This.Proof'Image &
", Flow => " & This.Flow'Image & ")");
None : constant T := T'(Entity.T with
Version => File_Version'First,
Proof => 0.0,
Flow => 0.0);
---------------------------------------------------------------------------
-- Flow
---------------------------------------------------------------------------
not overriding
function Flow (This : in T) return Duration is
(This.Flow);
---------------------------------------------------------------------------
-- Proof
---------------------------------------------------------------------------
not overriding
function Proof (This : in T) return Duration is
(This.Proof);
---------------------------------------------------------------------------
-- Version
---------------------------------------------------------------------------
not overriding
function Version (This : in T) return File_Version is
(This.Version);
end SPAT.Timing_Item;
|