I have the following parent package which defines several types

aes.ads

package AES is    
    type Byte is range 0..2**8  - 1;
    type Input_Buffer is array(Natural range <>) of Byte;
    type Output_Buffer is array(Natural range <>) of Byte;
    type Key is array(Natural range <>) of Byte;
    subtype AES_128_Key is Key(0..127);
    subtype AES_192_Key is Key(0..191);
    subtype AES_256_Key is Key(0..255);
    type Operation is (Encrypt, Decrypt);

    function AES_CBC_128(Input: Input_Buffer; Key: AES_128_Key; Op: Operation) return Output_Buffer;
    function AES_CBC_192(Input: Input_Buffer; Key: AES_192_Key; Op: Operation) return Output_Buffer;
    function AES_CBC_256(Input: Input_Buffer; Key: AES_256_Key; Op: Operation) return Output_Buffer;

private
    type Word is range 0..2**32 - 1;
    type State is array(0..3, 0..3) of Byte;
    type States is array(Natural range <>) of State;
    type Round_Key is array(0..16) of Byte;
    type Key_Schedule is array(Natural range <>) of Round_Key;
end AES;

aes.adb

with AES.AES_Cipher; use AES.AES_Cipher;
with AES.AES_Inv_Cipher; use AES.AES_Inv_Cipher;

package body AES is

-- other definitions

function AES_Common(St: State; K: Key; Op: Operation) return Output_Buffer is
    Schedule: Key_Schedule := Key_Expansion(K);
begin
    return (case Op is
        when Encrypt => Cipher(St, Schedule),
        when Decrypt => Inv_Cipher(St, Schedule)
    );
end AES_Common;

-- more definitions

end AES;

and then two child packages (aes-aes_inv_cipher is very similar to aes-aes_cipher so has been omitted)

aes-aes_cipher.ads

package AES.AES_Cipher is
    function Cipher(St: State; Schedule: Key_Schedule) return State;
end AES.AES_Cipher;

aes-aes_cipher.adb

package body AES.AES_Cipher is

function Cipher(St: State; Schedule: Key_Schedule) return State is
begin
    
    return St;
end Cipher;

end AES.AES_Cipher;

These are called from main.adb

with AES; use AES;

procedure Main is
    Input: Input_Buffer(0..35) := (others => Byte(44));
    K: AES_128_Key := (others => Byte(55));
    Output: Output_Buffer(0..35);
begin
    Output := AES_CBC_128(Input, K, Encrypt);
end Main;

This does not compile with the following error

aes-aes_cipher.ads:2:25: error: "State" is not visible (more references follow)
aes-aes_cipher.ads:2:25: error: non-visible (private) declaration at aes.ads:17
aes-aes_cipher.ads:2:42: error: "Key_Schedule" is not visible (more references follow)
aes-aes_cipher.ads:2:42: error: non-visible (private) declaration at aes.ads:20

I thought because aes-aes_cipher is a child package of aes it could access the private definitions in aes.ads but the error suggests otherwise. If this is not possible, how can I restructure the program so it works as expected? I am using gnatmake version 13.2.0 on Windows.

Hi!

? Interfaces.C.char’Size always equal to Ada.Stream.Stream_element’Size ?

If they are not the same, what are the most common sizes?

Thanks!

6 posts - 4 participants

Read full topic

The 28th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2024) will take place in Barcelona, Spain from 11 to 14 June, and comprises different tracks and co-located events.

Submission deadlines: 15 January for journal track papers; 26 February for industrial track and work-in-progress track papers, tutorial and workshop proposals. Submit early: tutorial/workshop proposals will be evaluated ASAP, with decisions from 1 January 2024!

More information on the conference site, including an extensive list of topics, and details on the call for contributions for the various tracks.

www.ada-europe.org/conference2024

#AEiC2024 #AdaEurope #AdaProgramming

1 post - 1 participant

Read full topic

I wonder. Is gnatd.v a better option than
pragma preelaborate

Is preelaborate more compiler portable? Though I do not use the features that it protects against such as dynamic dispatch, so it is simply an unneeded restriction for me with Gnat. However gnatd.v seems to offer more such as in regard to uninitialised variables? Assuming it works as I had no compile issues .

see 7.7

https://docs.adacore.com/spark2014-docs/html/lrm/packages.html

2 posts - 2 participants

Read full topic

We all know and love Ada.Containers.Vectors. Here's an example of its usage:

with Ada.Text_IO;
with Ada.Containers.Vectors;

procedure Example is
   use Ada.Text_IO;

   package Vectors_Integer is new Ada.Containers.Vectors (Natural, Integer);
   use Vectors_Integer;

   My_Vec : Vector := 1 & 2 & 3;
begin
   Put_Line (Integer'Image (My_Vec (0)));
end Example;

My question is simple: how does My_Vec (0) work, and how can I recreate this behavior in a type of my own?

I have been searching the internet for a while but I can't find to seem any explanation for how this expression works. The subscript operator, which uses the same syntax as the function call operator, cannot be overloaded using the normal syntax for operator overloading. I've read the package specification for Ada.Containers.Vectors, and there doesn't seem to be any explicit means through which Vector overloads this operator. I had guessed that the Element function might have something to do with it, but have been unable to use it to define a type of my own that replicates Vector's behavior. I'm at a complete loss on how to overload the subscript operator, even though it is clear that it is possible.

Not that I’m personally worried, but just saw this: Visual Studio for Mac 'retired': From open source, to closed source, to dead • DEVCLASS

5 posts - 4 participants

Read full topic

When using the procedure Set_Line (File, X) after using the procedure Skip_Line(File, Y) the error, END.ERROR is raised when X <= Y
(except when X = Y = 1).

When the procedure Set_Line (File, X) is called on a File of mode IN_FILE, it internally calls Skip_Line until the file line number reaches X.
If X is not equal than the current line in the file, the procedure will continuously skip lines until it reaches another page with a matching line. (RM 2022 p.g.523)

I am curious about the reasoning for this functionality as it has caused an amusing problem in the trivial program I am writing.
The program will get the number of lines from a .txt file and select a random line to print to the console. A word of the day program.
Minimal Example of Issue:

with Ada.Text_IO; use Ada.Text_IO;

procedure Main is

   File_Name : constant String := "TEST.txt";
   Test_File : File_Type;

begin
   Create (Test_File, Out_File, File_Name);

   for I in 1 .. 10 loop
      Put_Line (Test_File, "Line :" & Integer'Image (I));
   end loop;

   Close (Test_File);
   Open (Test_File, In_File, "Test.txt");

   Skip_Line (Test_File, 5);

   Set_Line (Test_File, 4);

end Main;
--Will raise End_Error

I would think that the procedure would check if X < File.Line then perform further actions. While am able to work around this, I am interested to understand the reasoning.
Thanks.

9 posts - 5 participants

Read full topic

It’s that time of year again!

Advent of Code is a series of daily programming puzzles from December 1st to 25th, becoming progressively more difficult each day. The puzzles can be completed in any programming language- inputs are short text files and the solutions are integers. Many people use these puzzles to learn a new language or try new techniques.

Last year, we had lively daily discussions and solutions in both Ada and SPARK on the forum. This year, I want to open the conversation up to any language with a focus on safety or reliability- Ada, SPARK, MISRA-C, or any other metallic compounds.

I think we can reuse last year’s leaderboard code 1708445-6a8f7730, which you can join on the Private Leaderboards page while logged into your AoC account.

5 posts - 3 participants

Read full topic

Hi,
Using GNAT v11.2/0-4 for ARM (Alire), the following procedure Unbiased_Rounding for Float works as expected.

function Unbiased_Rounding (X : Float) return Float is
Y : Float;
begin
Asm (“vrintn.f32 %0,%1”,
Outputs => Float’asm_output (“=t”, Y),
Inputs => Float’asm_input (“t”, X));
return Y;
end Unbiased_Rounding;

according to Machine Constraints (Using the GNU Compiler Collection (GCC))
the constraint t means "VFP floating-point registers s0-s31. Used for 32 bit values” and the constraint w means "VFP floating-point registers d0-d31 and the appropriate subset d0-d15 based on command line options. Used for 64 bit values only”

therefore we wrote our long_float version as

function Unbiased_Rounding (X : Long_Float) return Long_Float is
Y : Long_Float;
begin
Asm (“vrintn.f64 %0,%1”,
Outputs => Long_Float’asm_output (“=w”, Y),
Inputs => Long_Float’asm_input (“w”, X));
return Y;
end Unbiased_Rounding;

however this fails to compile.
GNAT 11.2/0-4 (Alire) complains
Error: invalid instruction shape – `vrintn.f64 s14,s14’

presumably because the operands are S registers rather than double precisions D registers.
Is this a bug or have we misunderstood something?

Best wishes,
Ahlan

8 posts - 4 participants

Read full topic

I was throwing something together recently, and realized none of my Pre and Post conditions were being caught.

Why is -gnata not enabled by default in new projects?

9 posts - 6 participants

Read full topic

When gnatprove is used with “–counterexamples=on” inside GNAT Studio it is able to present a detailed trace[1]:

This nice trace only seems to work inside GNAT Studio, not inside the VSCode AdaCore.ada plugin. Is there a way to output this trace to a text console (e.g. by passing an option to the gnatprove command-line command) so that this trace feature can be used outside GNAT Studio?

[1] 7.2. How to View GNATprove Output — SPARK User's Guide 25.0w

2 posts - 2 participants

Read full topic

I’m playing with tasks and have a question about select with delay until.

I have a task with the following body (the full implementation is on GitHub):

Wait : loop
   select
      -- Wait for pings. When they come, reset Last_Ping.
      accept Ping do
          Log.Debug ("Received ping.");
          Last_Ping := Clock;
      end Ping;
   or
      -- If there is no ping within the expected interval, do something.
      delay until (Last_Ping + Expected_Ping_Interval);
      Log.Error ("Timeout!");
      -- Do something.
      -- Is there any way to keep running the task loop here? 
   end select;
end loop Wait;

From how I understand the select, it waits for the specified delay - if there is a Ping before the end of the delay, the loop iteration is finished and the next iteration is started, again waiting for the specified delay or accepting a Ping.

Now, when the delay is over and there was no entry in Ping, it does not proceed with the next loop iteration but is finished, right? Why is that? And is there a way to write this loop so the task continues running?

(Also happily take pointers to good resources for learning about task behavior in more depth. )

6 posts - 3 participants

Read full topic

When I have added -fstack-check to an ARM cortex light project then I get the build error undefined reference to __gnat_stack_check.

It works fine on a full runtime.

Is that expected?

Can it be fixed?

4 posts - 3 participants

Read full topic