cubedos-lib.ads

1--------------------------------------------------------------------------------
2-- FILE : cubedos-lib.ads
3-- SUBJECT: Specification of a package serving as a parent to the CubedOS runtime library.
4-- AUTHOR : (C) Copyright 2024 by Vermont State University
5--
6-- This package also defines a number of useful, library-wide data types.
7--------------------------------------------------------------------------------
8pragma SPARK_Mode(On);
9
10package CubedOS.Lib is
11 pragma Pure;
12
13 type Octet is mod 2**8;
14 type Double_Octet is mod 2**16;
15 type Quadruple_Octet is mod 2**32;
16 type Octuple_Octet is mod 2**64;
17
18 -- Limiting the maximum size of arrays simplfies proving freedom from overflow in array index computations.
19 -- There is no other particular reason for this limit; it is arbitrary. The limit should be high enough to
20 -- satisfy any reasonable application.
21 --
22 -- There are situations where an Octet_Array needs to hold multiple octet sequences at once where at least
23 -- one of those sequences can be as much as 2**16 long. For example, the data in a space packet can be up to
24 -- 2**16 long, and the header is an addition 6 octets. Creating an Octet_Array that can hold the entire
25 -- packet might require 2**16 + 6 octets in total. For this reason, the upper bound on Octet_Array is 2**17.
26 --
27 Maximum_Array_Size : constant := 2**17;
28
29 -- Starting the index type at 0 is consistent with low level expectations.
30 subtype Octet_Array_Index is Natural range 0 .. Maximum_Array_Size - 1;
31 subtype Octet_Array_Count is Natural range 0 .. Maximum_Array_Size;
32 type Octet_Array is array (Octet_Array_Index range <>) of Octet
33 with Component_Size => 8;
34
35
36 -- Declare intrinsic shift functions for these types.
37
38 function Shift_Left(Value : in Octet; Count : in Natural) return Octet
39 with
40 Import,
41 Convention => Intrinsic,
42 Global => null;
43
44 function Shift_Right(Value : in Octet; Count : in Natural) return Octet
45 with
46 Import,
47 Convention => Intrinsic,
48 Global => null;
49
50 function Shift_Left(Value : in Double_Octet; Count : in Natural) return Double_Octet
51 with
52 Import,
53 Convention => Intrinsic,
54 Global => null;
55
56 function Shift_Right(Value : in Double_Octet; Count : in Natural) return Double_Octet
57 with
58 Import,
59 Convention => Intrinsic,
60 Global => null;
61
62 function Shift_Left(Value : in Quadruple_Octet; Count : in Natural) return Quadruple_Octet
63 with
64 Import,
65 Convention => Intrinsic,
66 Global => null;
67
68 function Shift_Right(Value : in Quadruple_Octet; Count : in Natural) return Quadruple_Octet
69 with
70 Import,
71 Convention => Intrinsic,
72 Global => null;
73
74end CubedOS.Lib;