❌ About FreshRSS

Normal view

There are new articles available, click to refresh the page.
Before yesterdayNewest questions tagged ada - Stack Overflow

Why can't I use subtypes from limited withed packages in subprogram declarations?

In Ada 2012, a limited with can be used from one file (for example, User) to import types from another package (for example, Provider), even when that package needs to import the current file. This is useful in cases where you have two mutually dependent types, such as the following, but you have them in two different packages, so you can't just use an incomplete type declaration like this:

    type Point;
    type Line;    -- incomplete types

    type Point is
        record
            L, M, N: access Line;
    end record;

    type Line is
        record
            P, Q, R: access Point;
    end record;

(the above example is from John Barnes' Programming in Ada 2012, section 13.5 Mutually dependent types)

However, my question doesn't even need mutually dependent types. I'm trying to compile some Ada code that was autogenerated using gcc -fdump-ada-spec -C some_c_header.h, which happens to contain some procedures and/or functions that have parameters being passed as access constant (const * in C), and I see no reason this shouldn't work using limited with, as fdump-ada-spec generates for me.

Why can't I use any subtypes from Provider inside a subprogram declaration? Using regular types is fine, but when trying to use subtypes gcc complains they do not exist in that package.

provider.ads

package Provider is

   type Fine_Type is range 0 .. 10_000;
   subtype Bad_Type is Fine_Type;

end Provider;

user.ads:

limited with Provider;

package User is

   procedure Do_It (A : access constant Provider.Bad_Type);

end User;

For completeness, here are stubs for the rest of the files you would need:

user.adb

package body User is

   procedure Do_It (A : access constant Provider.Bad_Type) is
   begin
      null;
   end Do_It;

end User;

limited_with_test.gpr

project limited_with_test is

   for Source_Dirs use ("src");
   for Main use ("main.adb");

   for Exec_Dir use "bin";
   for Object_Dir use "obj";
   for Create_Missing_Dirs use "True";

end limited_with_test;

If you put the sources into a directory called src, you can call gprbuild in the directory containing that directory and the gpr file, and you get:

$ gprbuild
using project file limited_with_test.gpr
Compile
   [Ada]          main.adb
user.ads:5:49: error: "Bad_Type" not declared in "Provider"
gprbuild: *** compilation phase failed

How to mark unreachable code in Ada/SPARK

I have the following code:

   function Linear_Search (A : Elem_Array; E : Elem) return Index is
   begin
      for i in A'Range loop
         pragma Loop_Invariant (for some J in i .. A'Last => A (J) = E);
         if A (i) = E then
            return i;
         end if;
      end loop;
      return A'Last;
   end Linear_Search;

This function has a precondition that says that the array contains the element searched for:

   function Contains (A : Elem_Array; E : Elem) return Boolean is
     (for some I in A'Range => A (I) = E);

   function Linear_Search (A : Elem_Array; E : Elem) return Index with
      Pre  => Contains (A, E),
      Post => A (Linear_Search'Result) = E;

So I would like to remove the return statement after the loop, or at least mark it as unreachable for clarity; is there any way to do that such that the compiler can also use that to optimize? What is the recommended way to mark unreachable code in Ada/SPARK?

Can you cheat contracts / asserts in SPARK?

Suppose I have a subprogram written using the SPARK Ada subset with postconditions verifying some property - for example, that the returned array is sorted, whose body just calls out to a function external to SPARK - for example, a C/C++ function that sorts arrays. Is there any way to force SPARK to assume, after this call, that the array will be sorted?

How to std::rotate in Ada?

Does an equivalent to std::rotate exist in the Ada standard libraries? If not, is there a consensus in the Ada community of some non-standard algorithms library for this sort of operation? I found the Ada Standard Generic Library but it was a proof of concept from 1996 and does not include rotate for arrays (it does for trees, though).

I whittled down the demo on the cppreference page linked above:

#include <algorithm>
#include <iostream>
#include <vector>

auto print = [](auto const& remark, auto const& v) {
    std::cout << remark;
    for (int n : v)
        std::cout << n << ' ';
    std::cout << '\n';
};

int main()
{
    std::vector<int> v{2, 4, 2, 0};

    print("before rotate:\t\t", v);

    // simple rotation to the left
    std::rotate(v.begin(), v.begin() + 1, v.end());

    print("simple rotate left:\t", v);

    // simple rotation to the right
    std::rotate(v.rbegin(), v.rbegin() + 1, v.rend());

    print("simple rotate right:\t", v);
}

The equivalent Ada would be this, if I had a drop-in replacement for the std::rotate calls:

with Ada.Text_IO;
with Ada.Characters;
with Ada.Characters.Latin_1;

procedure Main is
   Tab : Character renames Ada.Characters.Latin_1.HT;

   type Number_List_Type is array (1 .. 4) of Integer;

   procedure Print (Remark : String; Numbers : Number_List_Type) is
      use Ada.Text_IO;
      Endline : Character renames Ada.Characters.Latin_1.LF;
   begin
      Put (Remark);
      for N of Numbers loop
         Put (N'Image & ' ');
      end loop;
      Put (Endline);
   end;

   V : Number_List_Type := (2, 4, 2, 0);
begin
   print("before rotate:" & Tab & Tab, v);

   -- simple rotation to the left
   -- std::rotate(v.begin(), v.begin() + 1, v.end());

   print("simple rotate left:" & Tab, v);

   -- simple rotation to the right
   -- std::rotate(v.rbegin(), v.rbegin() + 1, v.rend());

   print("simple rotate right:" & Tab, v);
end Main;

Expected output:

before rotate:          2 4 2 0
simple rotate left:     4 2 0 2
simple rotate right:    2 4 2 0

Where is the actual character set for Ada program text defined?

I'm trying to make a tree-sitter parser, so that IDEs (in this case, Vim) can parse and do more advanced manipulation of Ada program text, such as extract-subprogram and rename-variable. But there seem to be some problems defining the character set.

In the Ada 2012 Reference Manual, I found a list of vague category descriptions, of the form 'Any character whose General Category is X' which means that for instance, besides the underscore, all of these ( ‿ ⁀ ⁔ ︳ ︴ ﹍ ﹎ ﹏ _) are also allowed in an identifier, which seems absurd, and GNAT rejects with 'illegal character'. The list is prefaced by this statement:

"The actual set of graphic symbols used by an implementation for the visual representation of the text of an Ada program is not specified."

Does that really mean there's no way to know which characters should be accepted?

Two pages on, these examples are explicitly given as valid identifiers, and yet GNAT 2021 rejects them:

procedure Main is
   Πλάτων  : constant := 12;     -- Plato
   Чайковский : constant := 12;  -- Tchaikovsky
   θ, φ : constant := 12;        -- Angles
begin
   null;
end Main;
$ gprbuild
using project file foo.gpr
Compile
   [Ada]          main.adb
main.adb:2:04: error: declaration expected
main.adb:2:05: error: illegal character
main.adb:3:04: error: declaration expected
main.adb:3:05: error: illegal character
main.adb:4:05: error: illegal character
gprbuild: *** compilation phase failed

Where is the actual character set for Ada programs defined? Has GNAT 2021 got it wrong?

An example program using Unicode characters in identifiers is below for your experimentation. Note that the use of wide characters in the literal string is outside the scope of the question.

main.adb:

with Ada.Wide_Text_IO; use Ada.Wide_Text_IO;

procedure Main is
   δεδομένα_πράμα : constant Wide_String := "Ο Πλάτων θα ενέκρινε";
begin
   Put_Line (Δεδομένα_πράμα);
end Main;

foo.gpr

project foo is

   for Source_Dirs use (".");
   for Main use ("main.adb");

   package Compiler is
      for Default_Switches ("ada") use ("-gnatW8", "-gnatiw");
   end Compiler;

end foo;

To build & run:

gprbuild
./main
❌
❌