https://gcc.gnu.org/bugzilla/show_bug.cgi?id=125063
Bug ID: 125063
Summary: First time doing this: Ran GNATPROVE, encountered
error, was asked to post it here.
Product: gcc
Version: 12.5.0
Status: UNCONFIRMED
Severity: normal
Priority: P3
Component: ada
Assignee: unassigned at gcc dot gnu.org
Reporter: robert.boettcher.sf at gmail dot com
CC: dkm at gcc dot gnu.org
Target Milestone: ---
Created attachment 64302
--> https://gcc.gnu.org/bugzilla/attachment.cgi?id=64302&action=edit
Content of source files after Filename.*:
the system type;
the options given when GCC was configured/built;
Using built-in specs.
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-linux-gnu/12/lto-wrapper
OFFLOAD_TARGET_NAMES=nvptx-none:amdgcn-amdhsa
OFFLOAD_TARGET_DEFAULT=1
Target: x86_64-linux-gnu
Configured with: ../src/configure -v --with-pkgversion='Ubuntu
12.3.0-1ubuntu1~22.04.3' --with-bugurl=file:///usr/share/doc/gcc-12/README.Bugs
--enable-languages=c,ada,c++,go,d,fortran,objc,obj-c++,m2 --prefix=/usr
--with-gcc-major-version-only --program-suffix=-12
--program-prefix=x86_64-linux-gnu- --enable-shared --enable-linker-build-id
--libexecdir=/usr/lib --without-included-gettext --enable-threads=posix
--libdir=/usr/lib --enable-nls --enable-clocale=gnu --enable-libstdcxx-debug
--enable-libstdcxx-time=yes --with-default-libstdcxx-abi=new
--enable-gnu-unique-object --disable-vtable-verify --enable-plugin
--enable-default-pie --with-system-zlib --enable-libphobos-checking=release
--with-target-system-zlib=auto --enable-objc-gc=auto --enable-multiarch
--disable-werror --enable-cet --with-arch-32=i686 --with-abi=m64
--with-multilib-list=m32,m64,mx32 --enable-multilib --with-tune=generic
--enable-offload-targets=nvptx-none=/build/gcc-12-YswQCa/gcc-12-12.3.0/debian/tmp-nvptx/usr,amdgcn-amdhsa=/build/gcc-12-YswQCa/gcc-12-12.3.0/debian/tmp-gcn/usr
--enable-offload-defaulted --without-cuda-driver --enable-checking=release
--build=x86_64-linux-gnu --host=x86_64-linux-gnu --target=x86_64-linux-gnu
Thread model: posix
Supported LTO compression algorithms: zlib zstd
gcc version 12.3.0 (Ubuntu 12.3.0-1ubuntu1~22.04.3)
the complete command line that triggers the bug;
~/.local/share/alire/releases/gnatprove_*/bin/gnatprove --level=4 -P matrix.gpr
--mode=all --info --counterexamples=on -v
the compiler output (error messages, warnings, etc.);
robert@RB-SF:~/Desktop/SPARK/MistralVibe$
~/.local/share/alire/releases/gnatprove_*/bin/gnatprove --level=4 -P matrix.gpr
--mode=all --info --counterexamples=on -v
Phase 1 of 3: generation of data representation information ...
gprbuild --subdirs=gnatprove/data_representation --no-object-check
--restricted-to-languages=ada -s -v -j1 -c -P matrix.gpr -cargs:Ada -S
-gnatR2js -gnatws -gnatis
Phase 2 of 3: generation of Global contracts ...
gprbuild --subdirs=gnatprove/phase1 --no-object-check
--restricted-to-languages=ada --gnatprove -s -v -j1 -c -P matrix.gpr --db
/home/robert/.local/share/alire/releases/gnatprove_15.1.0_aad9a73f/share/spark/config/frames
-cargs:Ada -gnatc
-gnates=/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/8f0d3db3.tmp
-gnatis
object directory "/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/phase1"
created for project Matrix
Changing to object directory of "Matrix":
"/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/phase1/"
/home/robert/.local/share/alire/releases/gnatprove_15.1.0_aad9a73f/libexec/spark/bin/gnat2why
-c -x ada -gnatA -g -gnata -gnatX -gnatw.e -gnatc
-gnates=/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/8f0d3db3.tmp
-gnatis -gnatec=/tmp/GPR.6742/GNAT-TEMP-000003.TMP
-gnatem=/tmp/GPR.6742/GNAT-TEMP-000004.TMP
/home/robert/Desktop/SPARK/MistralVibe/matrix_test.adb
/home/robert/.local/share/alire/releases/gnatprove_15.1.0_aad9a73f/libexec/spark/bin/gnat2why
-c -x ada -gnatA -g -gnata -gnatX -gnatw.e -gnatc
-gnates=/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/8f0d3db3.tmp
-gnatis -gnatec=/tmp/GPR.6742/GNAT-TEMP-000003.TMP
-gnatem=/tmp/GPR.6742/GNAT-TEMP-000004.TMP
/home/robert/Desktop/SPARK/MistralVibe/matrix.adb
Phase 3 of 3: flow analysis and proof ...
gprbuild --subdirs=gnatprove/ --complete-output --restricted-to-languages=ada
--gnatprove -s -v -j1 -c -P matrix.gpr --db
/home/robert/.local/share/alire/releases/gnatprove_15.1.0_aad9a73f/share/spark/config/gnat2why
-cargs:Ada -gnatc
-gnates=/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/97f50a62.tmp
Changing to object directory of "Matrix":
"/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/"
/home/robert/.local/share/alire/releases/gnatprove_15.1.0_aad9a73f/libexec/spark/bin/gnat2why
-c -x ada -gnatA -g -gnata -gnatX -gnatw.e -gnatc
-gnates=/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/97f50a62.tmp
-gnatec=/tmp/GPR.6763/GNAT-TEMP-000003.TMP
-gnatem=/tmp/GPR.6763/GNAT-TEMP-000004.TMP
/home/robert/Desktop/SPARK/MistralVibe/matrix_test.adb
-gnateO=/tmp/GPR.6763/GNAT-TEMP-000005.TMP
matrix_test.adb:42:19: medium: assertion might fail
42 | pragma Assert (C(1, 1) = 84);
| ^~~~~~~~~~~~
matrix_test.adb:43:19: medium: assertion might fail
43 | pragma Assert (C(1, 2) = 90);
| ^~~~~~~~~~~~
matrix_test.adb:44:19: medium: assertion might fail
44 | pragma Assert (C(2, 1) = 198);
| ^~~~~~~~~~~~~
matrix_test.adb:45:19: medium: assertion might fail
45 | pragma Assert (C(3, 3) = 450);
| ^~~~~~~~~~~~~
/home/robert/.local/share/alire/releases/gnatprove_15.1.0_aad9a73f/libexec/spark/bin/gnat2why
-c -x ada -gnatA -g -gnata -gnatX -gnatw.e -gnatc
-gnates=/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/97f50a62.tmp
-gnatec=/tmp/GPR.6763/GNAT-TEMP-000003.TMP
-gnatem=/tmp/GPR.6763/GNAT-TEMP-000004.TMP
/home/robert/Desktop/SPARK/MistralVibe/matrix.adb
-gnateO=/tmp/GPR.6763/GNAT-TEMP-000005.TMP
+===========================GNAT BUG DETECTED==============================+
| 1.0 (spark) 1:0: value expected (got DOC_END) |
| No source file position information available |
| Compiling /home/robert/Desktop/SPARK/MistralVibe/matrix.adb |
| Please submit a bug report; see https://gcc.gnu.org/bugs/ . |
| Use a subject line meaningful to you and us to track the bug. |
| Include the entire contents of this bug box in the report. |
| Include the exact command that you entered. |
| Also include sources listed below. |
+==========================================================================+
Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).
/home/robert/Desktop/SPARK/MistralVibe/matrix.adb
/home/robert/Desktop/SPARK/MistralVibe/matrix.ads
matrix.adb:16:26: info: unrolling loop
matrix.adb:17:29: info: unrolling loop
matrix.adb:18:32: info: unrolling loop
compilation abandoned
gprbuild: *** compilation phase failed
spark_report
/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/gnatprove.alfad
Summary logged in
/home/robert/Desktop/SPARK/MistralVibe/obj/gnatprove/gnatprove.out
gnatprove: error during flow analysis and proof
and
the preprocessed file (*.i*) that triggers the bug, generated by adding
-save-temps to the complete compilation command, or, in the case of a bug
report for the GNAT front end, a complete set of source files (see below).
-- precprocessed file not possible, as I ran GNATPROVE. Please see
text-attachment source files-
