This repository was archived by the owner on May 22, 2023. It is now read-only.
File tree 5 files changed +45
-54
lines changed
5 files changed +45
-54
lines changed Original file line number Diff line number Diff line change 2
2
with System ;
3
3
with Gneiss_Internal.Syscall ;
4
4
with Gneiss_Internal.Client ;
5
+ with Gneiss_Internal.Util ;
5
6
with Gneiss_Protocol.Session ;
6
7
7
8
package body Gneiss.Memory.Client with
16
17
External_Name => " gneiss_memfd_create" ,
17
18
Global => (In_Out => Gneiss_Internal.Platform_State);
18
19
19
- function Get_First (Length : Integer) return Buffer_Index;
20
- function Get_Last (Length : Integer) return Buffer_Index;
21
-
22
- function Get_First (Length : Integer) return Buffer_Index is
23
- (if Length < 1 then Buffer_Index'First + 1 else Buffer_Index'First);
24
-
25
- function Get_Last (Length : Integer) return Buffer_Index
26
- is
27
- begin
28
- if Length < 1 then
29
- return Buffer_Index'First;
30
- end if ;
31
- if Long_Integer (Length) < Long_Integer (Buffer_Index'Last - Buffer_Index'First + 1 ) then
32
- return Buffer_Index (Long_Integer (Buffer_Index'First) + Long_Integer (Length) - 1 );
33
- else
34
- return Buffer_Index'Last;
35
- end if ;
36
- end Get_Last ;
20
+ function Get_First is new Gneiss_Internal.Util.Get_First (Buffer_Index);
21
+ function Get_Last is new Gneiss_Internal.Util.Get_Last (Buffer_Index);
37
22
38
23
procedure Initialize (Session : in out Client_Session;
39
24
Cap : Capability;
Original file line number Diff line number Diff line change 1
1
2
2
with Gneiss_Internal.Syscall ;
3
+ with Gneiss_Internal.Util ;
3
4
4
5
package body Gneiss.Memory.Server with
5
6
SPARK_Mode
6
7
is
7
8
8
- function Get_First (Length : Integer) return Buffer_Index;
9
- function Get_Last (Length : Integer) return Buffer_Index;
10
-
11
- function Get_First (Length : Integer) return Buffer_Index is
12
- (if Length < 1 then Buffer_Index'First + 1 else Buffer_Index'First);
13
-
14
- function Get_Last (Length : Integer) return Buffer_Index
15
- is
16
- begin
17
- if Length < 1 then
18
- return Buffer_Index'First;
19
- end if ;
20
- if Long_Integer (Length) < Long_Integer (Buffer_Index'Last - Buffer_Index'First + 1 ) then
21
- return Buffer_Index (Long_Integer (Buffer_Index'First) + Long_Integer (Length) - 1 );
22
- else
23
- return Buffer_Index'Last;
24
- end if ;
25
- end Get_Last ;
9
+ function Get_First is new Gneiss_Internal.Util.Get_First (Buffer_Index);
10
+ function Get_Last is new Gneiss_Internal.Util.Get_Last (Buffer_Index);
26
11
27
12
procedure Modify (Session : in out Server_Session;
28
13
Ctx : in out Context)
Original file line number Diff line number Diff line change
1
+
2
+ package body Gneiss_Internal.Util with
3
+ SPARK_Mode
4
+ is
5
+
6
+ function Get_First (Length : Integer) return Buffer_Index is
7
+ (if Length < 1 then Buffer_Index'First + 1 else Buffer_Index'First);
8
+
9
+ function Get_Last (Length : Integer) return Buffer_Index
10
+ is
11
+ begin
12
+ if Length < 1 then
13
+ return Buffer_Index'First;
14
+ end if ;
15
+ if Long_Integer (Length) < Long_Integer (Buffer_Index'Last - Buffer_Index'First + 1 ) then
16
+ return Buffer_Index (Long_Integer (Buffer_Index'First) + Long_Integer (Length) - 1 );
17
+ else
18
+ return Buffer_Index'Last;
19
+ end if ;
20
+ end Get_Last ;
21
+
22
+ end Gneiss_Internal.Util ;
Original file line number Diff line number Diff line change
1
+
2
+ package Gneiss_Internal.Util with
3
+ SPARK_Mode
4
+ is
5
+
6
+ generic
7
+ type Buffer_Index is range <>;
8
+ function Get_First (Length : Integer) return Buffer_Index;
9
+
10
+ generic
11
+ type Buffer_Index is range <>;
12
+ function Get_Last (Length : Integer) return Buffer_Index;
13
+
14
+ end Gneiss_Internal.Util ;
Original file line number Diff line number Diff line change 2
2
with System ;
3
3
with Gneiss_Internal.Syscall ;
4
4
with Gneiss_Internal.Client ;
5
+ with Gneiss_Internal.Util ;
5
6
with Gneiss_Protocol.Session ;
6
7
7
8
package body Gneiss.Rom.Client with
8
9
SPARK_Mode
9
10
is
10
11
11
- function Get_First (Length : Integer) return Buffer_Index;
12
- function Get_Last (Length : Integer) return Buffer_Index;
13
-
14
- function Get_First (Length : Integer) return Buffer_Index is
15
- (if Length < 1 then Buffer_Index'First + 1 else Buffer_Index'First);
16
-
17
- function Get_Last (Length : Integer) return Buffer_Index
18
- is
19
- begin
20
- if Length < 1 then
21
- return Buffer_Index'First;
22
- end if ;
23
- if Long_Integer (Length) < Long_Integer (Buffer_Index'Last - Buffer_Index'First + 1 ) then
24
- return Buffer_Index (Long_Integer (Buffer_Index'First) + Long_Integer (Length) - 1 );
25
- else
26
- return Buffer_Index'Last;
27
- end if ;
28
- end Get_Last ;
12
+ function Get_First is new Gneiss_Internal.Util.Get_First (Buffer_Index);
13
+ function Get_Last is new Gneiss_Internal.Util.Get_Last (Buffer_Index);
29
14
30
15
procedure Initialize (Session : in out Client_Session;
31
16
Cap : Gneiss.Capability;
You can’t perform that action at this time.
0 commit comments