pragma Ada_2022;
with ada.numerics.generic_real_arrays;
with Ada.Text_IO;
procedure test1 is
type real is digits 6;
use type real;
package gra is new ada.numerics.generic_real_arrays (real => real);
use gra;
a : constant real_matrix(1..2,1..2) := [[1.0, 0.0], [0.0, 2.0]];
e : constant real_vector := Eigenvalues(a);
begin
for i in e'Range loop
Ada.Text_IO.Put_Line(i'Image & e(i)'Image);
end loop;
end test1;
This gives the eigenvalues 2 and 1 (as expected). However, when I just copy in the same code in a larger program like this:
declare
type real is digits 6;
package gra is new ada.numerics.generic_real_arrays (real => real); -- <--line 4375
use gra;
a : constant real_matrix(1..2,1..2) := [[1.0, 0.0], [0.0, 2.0]];
e : constant real_vector := Eigenvalues(a);
begin
for i in e'Range loop
Ada.Text_IO.Put_Line(i'Image & e(i)'Image);
end loop;
end;
Then I get the following error message (when running the code):
“System error message: failed precondition from s-gearop.ads:549 instantiated at a-ngrear.adb:78 instantiated at kobio0.adb:4375”
I feel a bit lost. My point is to trace down an error. Any hint?
I compiled successfully your first code snippet. I then deleted the declaration part and the body. Inside the now empty body, I copied the second code snippet. I was also able to successfully compile the code.
My conclusion would be that it is likely that this code is not the one causing the issues, but it is potentially something around it. The compiler may be going a bit crazy and may not know exactly what is causing the issue and it may be pointing to the lines of code that you write here…
Does the error really only appear when you add this code? What happens if you comment out only this section?
For info, the problem only seems to be related to “Eigenvalues”. Determinant and Inverse function well:
declare
type real is digits 6;
package gra is new ada.numerics.generic_real_arrays (real => real);
use gra;
a : constant real_matrix(1..2,1..2) := [[1.0, 0.0], [0.0, 2.0]];
d : constant real := Determinant(a);
b : constant real_matrix := Inverse(a);
-- e : constant real_vector := Eigenvalues(a);
begin
New_Line(2);
Put("a: ");
for i in a'Range(1) loop
New_Line;
for j in a'Range(2) loop
Put( a(i,j),4,2,0);
end loop;
end loop;
New_Line(2);
Put("b: ");
for i in a'Range(1) loop
New_Line;
for j in b'Range(2) loop
Put( b(i,j),4,2,0);
end loop;
end loop;
New_Line(2);
Ada.Text_IO.Put_Line("Determinant: " & to_string1(d));
end;
``
fernando@localhost:~/Dirt> cat test.adb
pragma Ada_2022;
with ada.numerics.generic_real_arrays;
with Ada.Text_IO;
procedure test1 is
begin
declare
type real is digits 6;
package gra is new ada.numerics.generic_real_arrays (real => real); -- <--line 4375
use gra;
a : constant real_matrix(1..2,1..2) := [[1.0, 0.0], [0.0, 2.0]];
e : constant real_vector := Eigenvalues(a);
begin
for i in e'Range loop
Ada.Text_IO.Put_Line(i'Image & e(i)'Image);
end loop;
end;
end test1;
fernando@localhost:~/Dirt> gnatmake -gnatwa -gnata -gnatX0 test
gnatmake: "test" up to date.
fernando@localhost:~/Dirt> gnatmake -gnatwa -gnata -gnatX0 test -s
gcc -c -gnatwa -gnata -gnatX0 test.adb
test.adb:4:11: warning: file name does not match unit name, should be "test1.adb" [enabled by default]
gnatbind -x test.ali
gnatlink test.ali
gnatlink: warning: executable name "test" may conflict with shell command
fernando@localhost:~/Dirt> ./test
raised ADA.ASSERTIONS.ASSERTION_ERROR : failed precondition from s-gearop.ads:549 instantiated at a-ngrear.adb:78 instantiated at test.adb:8
The Eigenvalues function calls Jacobi (no issues there) and Sort_Eigensystem (this is where the exception is raised)
Sort_Eigensystem makes a few function calls:
#0 system.assertions.raise_assert_failure (msg=...) at s-assert.adb:41
#1 0x0000000000405148 in test1.gra.swap_column (a=..., left=2, right=<optimized out>)
at /usr/lib64/gcc/x86_64-suse-linux/14/adainclude/s-gearop.ads:549
#2 0x00000000004052a0 in test1.gra.sort_eigensystem.swap (left=<optimized out>, right=right@entry=1)
at /usr/lib64/gcc/x86_64-suse-linux/14/adainclude/a-ngrear.adb:751
#3 0x0000000000405360 in test1.gra.sort_eigensystem.sort.sort.xchg (j=j@entry=2, k=k@entry=1)
at /usr/lib64/gcc/x86_64-suse-linux/14/adainclude/a-cogeso.adb:71
#4 0x00000000004053cb in test1.gra.sort_eigensystem.sort.sort.sift (s=s@entry=1)
at /usr/lib64/gcc/x86_64-suse-linux/14/adainclude/a-cogeso.adb:97
#5 0x000000000040548a in test1.gra.sort_eigensystem.sort.sort (first=<optimized out>, last=<optimized out>)
at /usr/lib64/gcc/x86_64-suse-linux/14/adainclude/a-cogeso.adb:117
#6 0x0000000000405504 in test1.gra.sort_eigensystem.sort (first=<optimized out>, last=<optimized out>)
at /usr/lib64/gcc/x86_64-suse-linux/14/adainclude/a-cgaaso.adb:46
#7 0x0000000000405556 in test1.gra.sort_eigensystem (values=..., vectors=...)
at /usr/lib64/gcc/x86_64-suse-linux/14/adainclude/a-ngrear.adb:756
#8 0x0000000000406be9 in test1__B_1__gra__F240b.1 ()
#9 0x0000000000406c4e in test1.gra.eigenvalues (a=...) at /usr/lib64/gcc/x86_64-suse-linux/14/adainclude/a-ngrear.adb:496
#10 0x0000000000406cfe in test1 () at test.adb:11
When Swap_Column is called (file s-gearop.ads) with assertions enabled, the precondition fails. Here are its contracts and body:
-----------------
-- Swap_Column --
-----------------
generic
type Scalar is private;
type Matrix is array (Integer range <>, Integer range <>) of Scalar;
procedure Swap_Column (A : in out Matrix; Left, Right : Integer)
with
Pre => Left in A'Range (2)
and then Right in A'Range (2);
-----------------
-- Swap_Column --
-----------------
procedure Swap_Column (A : in out Matrix; Left, Right : Integer) is
Temp : Scalar;
begin
for J in A'Range (1) loop
Temp := A (J, Left);
A (J, Left) := A (J, Right);
A (J, Right) := Temp;
end loop;
end Swap_Column;
In this case, Left had the value of 2, while I could not find the A'Range(2) (optimised out and I am not too good with GDB).
The code does seem to produce the correct output when compiled with no checks… And Swap_Column is called by other GNAT functions… And the data does seem correct… Mmmm…
Is there a bug somewhere in here or is the contract not that correct?
Mmm… I can’t help you any further as I do not have that much more time, but this is quite interesting. Best regards,
Fer
I did a quick conversion to use my gnat_math_extensions package (and discovered a usability bug in the process). It gives the same output results as the original does without assertions enabled, except that the elements are swapped - not sure this is a problem.
Hi Simon, have you dug a bit deeper? I kind feel that this may be a bug with the contracts… Maybe this could be submitted as a bug report to GCC? Or maybe @ebriot could lend us a hand with his AdaCore support?
Hi,
Sorry, I think it would be abusing the support contract to report other people’s bug when they have no chance of impacting our own code (the last time I reported a bug, it was because we were also using the same type of construct ourselves, so it was preventive – we do not use EigenValues though).
You should however report it yourself, since AdaCore is always interested in having small, self-contained reproducers.
