Normal view

There are new articles available, click to refresh the page.
Before yesterdayNews from the Ada programming language world

How the weakest preconditions and the verification conditions for the following specification statements can be derived using the postcondition [closed]

How can the weakest preconditions and the verification conditions for the following specification statements be derived using the postcondition hoisting technique and proof rules for sequence and assignment?

{ true } 
M := X; 
N := Y; 
A := 2 * M + N; 
N := N – 1; 
M := A 
{ M > N}  

How to incorporate proof aspects into the specification so that every function and procedure has a Post aspect and, if required, a Pre aspect

How to incorporate proof aspects into the specification so that every function and procedure has a Post aspect and, if required, a Pre aspect that outlines the proper behaviour of the code below:

package Stack with SPARK_Mode is
pragma Elaborate_Body;

   Stack_Size : constant := 100;
   type Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
   type Vector is array(Index_Range) of Integer;

   S: Vector;
   Pointer: Pointer_Range;

   function isEmpty return Boolean;
   procedure Push(X : in Integer)
       Global => (In_out => (S, Pointer)),
       Depends => (S => (S, Pointer, X),
                   Pointer => Pointer);

   procedure Pop(X : out Integer)
       Global => (input => S, in_out => Pointer),
       Depends => (Pointer => Pointer,
                   X => (S, Pointer));

end Stack;

GPRbuild: relocation truncated to fit R_X86_64

I'm dealing with huge global lists in Ada. When building I'm getting the error during linking: relocation truncated to fit R_X86_64_PC32 and link of main.adb failed. I saw that GCC has the flag -mcmodel=medium, is there something similar for gprbuild or does anyone has a hint how to deal with huge global lists?

Thanks in advance.

How to deallocate Ada Record from CPP

I am attempting to free a heap allocated Ada tagged record from cpp. I have used the code AdacoreU as a starting place.

I receive the following error when running the code below.

double free or corruption (out)

raised PROGRAM_ERROR : unhandled signal

Am I overthinking things? Do I need an Ada based deallocation mechanism.

What is my real end goal? I would like to use dynamic libraries to create a plugin infrastructure where each library is its own factory for a given type. Something along the lines of boost dll but with ada based dynamic libraries.

Modified Code below:


  1 #include <iostream>
  2 #include "animal.h"
  4 extern "C" {
  5     void adainit (void);
  6     void adafinal (void);
  7     Animal* new_animal();
  8     void del_animal(Animal *);
  9 }
 11 int main(void) {
 12     adainit();
 13     Animal* A = new_animal();
 14     std::cout << A->age() << std::endl;
 15     //delete A;   
 16     del_animal(A);
 17     adafinal();
 18     return 0;
 19 };

  2 with Interfaces.C;
  4 package ALib is
  6     type Animal is tagged record
  7         The_Age :;
  8     end record;
  9     pragma Convention (CPP, Animal);
 11     type Animal_Class_Access is access Animal'Class;
 13     function New_Animal return access Animal'Class;
 14     pragma Export(CPP, New_Animal);
 16     procedure Del_Animal (this : in out Animal_Class_Access);
 17     pragma Export(CPP, Del_Animal);
 19     function Age(X : Animal) return;
 20     pragma Export(CPP, Age);
 22 end ALib;


  1 with ada.unchecked_deallocation;
  3 package body ALib is
  5     function New_Animal
  6         return access Animal'Class is
  7     begin
  8         return new Animal'(The_Age => 20);
  9     end New_Animal;
 12     procedure Del_Animal (this : in out Animal_Class_Access) is
 13         procedure Free is new ada.unchecked_deallocation(Animal'Class, Animal_Class_Access);
 14     begin
 15         Free(this);
 16         --null;
 17     end Del_Animal;
 19     function Age(X : Animal)
 20         return is
 21     begin
 22         return X.The_Age;
 23     end Age;
 25 end ALib;

other resources used as a starting point Interfacing with C++ at the Class Level

What have I attempted:

  • Used various combinations of the type and access type when attempting to create the Free procedure
    • Animal, type Animal_Access is access Animal
    • Animal'Class, type Animal_Class_Access is access Animal'Class
    • Animal, type Animal_Access is access Animal'Class
  • I was at some point under the impression that I should be using system address for the pointers to the Animal object as either part of the return on New_Animal and as the argument to Del_Animal

What did I expect:

I expected to clean up Ada heap objects from Ada.

How is Ada and GPR supposed to handle conditional compilation? [duplicate]

I'm rewriting C source to Ada and on some places there is conditional compilation for handling different platforms, such as windows vs posix, DEBUG, or architecture. For what I can tell neither Ada nor GPR has the notion of conditional compilation.

What's the Ada way of handling it?


/* Determine if a process is alive. */
#ifndef _WIN32
   if (kill(pid, 0) && errno == ESRCH)
      return 0; /* pid does not exist */
   HANDLE h;
   if ((h = OpenProcess(PROCESS_QUERY_INFORMATION, FALSE, (DWORD)pid)) == 0)
      return 0; /* pid does not exist */
   return 1;

Building GCC 12.2.0 on Ventura for aarch64

These are notes on building GCC 12.2.0 and GNAT tools for Apple silicon.

There were two main problems:

  • the base package was built on an Intel machine (lockheed - named after Shadowcat’s companion dragon), running Monterey (macOS 12).
  • the build machine, an M1 mac Mini (temeraire - named after Naomi Novik’s dragon) was by this time running Ventura (macOS 13), but I wanted to make sure that users could continue to run on Monterey.
Read more »

Trying to use GPS for Ada and keep having problems trying to compile and run the code

I am currently trying to run a program in GPS and this is my first time trying to use Ada and don't quite understand some things to it. I have some code that was told was supposed to run but can't seem to get it running. When I try to compile it or run the code, I keep getting an error message: "end of file expected. file can only be one compilation unit." I also included a photo to help show the problem. I'd appreciate any tips or hints on how to solve this please!

enter image description here

Self dependency in Spark 2014

I'm trying to write the flow dependency of a procedure in Ada and Spark 2014 and the compiler give me a medium warning that

medium: missing dependency "null => MyBool"
medium: incorrect dependency "MyBool => MyBool"

Here is my .ads file:

SPARK_Mode (On);
package TestDep is

  pragma Elaborate_Body;

  MyBool: Boolean := False;

  procedure ToFalse with
    Global => (In_Out => MyBool),
    Depends => (MyBool =>+ null),
    Pre => (MyBool = True),
    Post => (MyBool = False);

end TestDep;

and in the .adb:

pragma SPARK_Mode (On);
package body TestDep is

  procedure ToFalse is
    MyBool := False;
  end ToFalse;

end TestDep;

I'm new to Ada and Spark and I'm still learning it, but from the AdaCore documentation I've saw that Depends => (X =>+ null) should indicate that the value of X at the end of the procedure only depends on the value of X and nothing else.

Why does the compiler give me those warning ? Am I doing something wrong ?

Ada GNAT.SOCKETS.SOCKET_ERROR:[11] Resource temporarily unavailable

I'm using the following socket server on windows, which works fine. When I try to execute this code on linux I get the following error message:

GNAT.SOCKETS.SOCKET_ERROR:[11] Resource temporarily unavailable

Does anybody has a hint whats going wrong?

Thanks a lot in advance.

with Ada.Text_IO; use Ada.Text_IO;
with GNAT.Sockets; use GNAT.Sockets;
with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;

procedure Server is
   Channel : Stream_Access;
   Server : Socket_Type;
   Address : Sock_Addr_Type;
   Socket : Socket_Type;
   receive_str : Unbounded_String;
   Receive_Character : Character;
   Put_Line("Server Config Started...");
   Create_Socket(Socket => Server);
   Set_Socket_Option(Socket => Server, Level => Socket_Level, Option => (Name => Reuse_Address, Enabled => True));
   Set_Socket_Option(Server, Socket_Level, (Receive_Timeout, Timeout => 1.0));
   Bind_Socket(Server, Address => (Family => Family_Inet, Addr => Inet_Addr(""), Port => 65432));

      Accept_Socket(Server, Socket, Address);
      receive_str := To_Unbounded_String("");
      Channel := Stream(Socket);
         Character'Read(Channel, Receive_Character);
         exit when Receive_Character = '@';
         Append(receive_str, Receive_Character);
      end loop;
      Put_Line("ReceiveStr" & To_String(receive_str));
      String'Write(Channel, "OK123");
   end loop;
end Server;

Gnatcheck custom rules

I'm trying to obtain a list of global variables declared in a large Ada project. gnatcheck has a rule for that: Global_Variables, but that rule is not exhaustive:

"Flag any variable declaration that appears immediately within the specification of a library package or library generic package. Variable declarations in nested packages and inside package instantiations are not flagged"

I'd like to be able to obtain the list of variables declared in package instantiations as well. I would try to implement my own gnatcheck custom rule, but cannot seem to find where the rules are implemented. This doc says it's supposed to be in share/lkql, but there is no such directory in my GNAT Studio installations (I've looked at GNAT Pro 19.2, GNAT Pro 22.1 and Gnat Community 2021). Windows cannot find any .lkql file.

Is it possible to make such a rule? If so, how/where? Are there alternatives to gnatcheck to obtain the list of global variables?

Cannot Run GNATStudio - WSL

I've checked the other questions and this case doesn't seem to be covered. I'm running Ubuntu in WSL on my windows machine and I'm trying to run GNATStudio, any time I attempt to run the program either via Alire or by calling it I receive the following error.

 error while loading shared libraries: cannot open shared object file: No such file or directory

I've already done the basics, and verified I have the correct file installed. Calling apt-file find produces the following.

root@DESKTOP-F319G5G:/opt# apt-file find
libxcb-shm0: /usr/lib/x86_64-linux-gnu/
libxcb-shm0: /usr/lib/x86_64-linux-gnu/

I've confirmed the location is in my path, as well and have restarted a few times. I'm really not too sure what my next steps should be. Any help is much appreciated!

How can I install the ZFP (Zero Foot Print) RTS (Run Time System) for AVR with the Alire package manager for Ada?

How can I install the ZFP (Zero Foot Print) RTS (Run Time System) for AVR with the Alire package manager for Ada?

My project file, I think correctly, contains:

project Avr is
   for Runtime("Ada") use "zfp";
   for Target use "avr-elf";
end Avr;

alire.toml hopefully correction contains:

gnat_avr_elf = ">=11.2.4"

Unfortunately, when running alr build, I get:

gprconfig: can't find a toolchain for the following configuration:
gprconfig: language 'ada', target 'avr-elf', runtime 'zfp'

I found documentation for programming AVR with Ada, but this assumes that I build the tool-chain myself and not have a package manager at least providing the GNU tool-chain.

The same applies to Programming Arduino with Ada.

gnatcoll-db includes, need to understand routines in python

I was using gnatcoll-db, but the limitations made me to rewrite in Ada. There are two routines in (in python) that I don't understand, specifically compute_table_aliases and fields_count_array.

Any help will be welcome. Of course, the modifications can be shared between all of us.

Edited to complete information:

My project fork is here. I don't want to copy here the complete routines from as I don't know exactly the license terms of ACS. can be downloaded from

The routines that I want to translate to Ada are:

  • compute_table_aliases, lines 2407 to 2448. Really I don't understand the algorithm.
  • fields_count_array and fields_count, lines 2372 to 2397. For these routines I have a translation to Ada but when testing, the result is OK except in a few cases.

Here is my translation to Ada:

Max_Depth : constant := 3; type Counts_Array is array (0 .. Max_Depth) of Integer;

  function Fields_Count_Array (T         : Table_Description;
                               Follow_LJ : Boolean;
                               DepthMax  : Integer;
                               FKStop    : Field := No_Field)
                            return Counts_Array is
     FK_Stop : Boolean; -- to be reset before each call to fields_count_
     Depth   : Integer := 0;
     Temp    : Counts_Array;

     function Fields_Count (T         : Table_Description;
                            Depth     : Integer;
                            Follow_LJ : Boolean;
                            FKStop    : Field := No_Field) return Integer;
     function Fields_Count (T         : Table_Description;
                            Depth     : Integer;
                            Follow_LJ : Boolean;
                            FKStop    : Field := No_Field)
                         return Integer is
        Result : Integer;
        procedure Process_FK (FK : in out Field);
        procedure Process_FK (FK : in out Field) is
           if FK = FKStop then
              FK_Stop := True;
           end if;
           if FK_Stop then
           end if;
           if Follow_LJ or (not FK.Can_Be_Null) then
              Result := Result +
                Fields_Count (Pointed_Table (FK), Depth - 1, Follow_LJ);
           end if;
        end Process_FK;
        Result := Num_Fields (T);
        if Depth > 0 then
           For_Each_FK (T, Process_FK'Access);
        end if;
        return Result;
     end Fields_Count;

     while Depth <= DepthMax loop
        FK_Stop := False;
        Temp (Depth) := Fields_Count (T, Depth, Follow_LJ, FKStop);
        Depth := Depth + 1;
     end loop;
     return Temp;
  end Fields_Count_Array;

Note that all type definitions come from gnatcoll-sql.

I understand that this is difficult to follow, perphaps may be better if I send a report on the modifications and the complete new Ada package replacing How?

Starting Gnat Studio with Alire fails

I have had a try at using Gnat Studio with the Alire package manager. Launching Gnat Studio using the 'alr edit' command is causing Gnat Studio to crash. I have had a look at the log file and there are several .dll files causing exceptions. The file entries are like this:

[PROJECTS.EXCEPTIONS] Unexpected exception: raised CONSTRAINT_ERROR : gnatcoll-projects.adb:5729 index check failed _PROJECTS.EXCEPTIONS_ [C:\GNATSTUDIO\bin\gps.libgnatcoll\libgnatcoll.dll] _PROJECTS.EXCEPTIONS_ 0x7ffc78dcecb8 ??? at ???

Gnat Studio opens in an 'inconsistent state' and crashes.

Regards Mike

adding -gnatp flag to a file/package in GPS [duplicate]

I use Ada With GPS (GNAT Programming Studio). The flag "-gnatp" when building will ignore among others constraint errors.

I know a way to add the flag to all the files, using Edit->Preferences->Build target.

Is there a way to choose when the builder will this flag, meaning setting the flag to a file or a package?

Cannot run Gnat Studio

I'm trying to run Gnat Studio on Ubuntu 22.04 but I get the following error:

/opt/gnatstudio/bin/gnatstudio_exe: error while loading shared libraries: cannot open shared object file: No such file or directory

I have installed it via the following steps:

  • Downloaded the "x86 GNU Linux (64 bits)" community edition and ran this
  • Ran /opt/GNAT/2021/doinstall
  • Ran /opt/gnatstudio/bin/gnatstudio and got the above error (sudo-running this yields the same error)

I'm wondering if this is down to 22.04 being a very recent release and some shared libraries are missing from the installation bundle?

Any pointers would be much appreciated.