Hello, I'm trying to make SPARK package for Debian, not yet successful, but I think this could be done.
I'm currently trying to compile version 2010-SMT of gnat-gpl (is SMT
part of the version or something else). Current status is:
sparklalr - compiles ok
examiner - a lot of warnings about invalid unchecked_conversion in
dictionary-rawdict.adb, example:
dictionary-rawdict.adb:4751:07: warning: types for unchecked conversion have
different sizes
dictionary-rawdict.adb:4751:07: warning: size of "Globalvariableref" is 64,
size of "Reftype" is 32
I think this only happens on 64-bit architectures and is a real
bug there. Here Reftype is defined in examinerconstants.ads as
follows:
type RefType is range 0 .. Natural'Last;
--# assert RefType'Base is Integer;
Globalvariableref in the error message is an access type, so it
will not fit into RefType. So reftype should be something like
Integer_Address, but then what to do with the range and with
assert?
Another problem is compiller error (probably fixed in
gcc-snapshot, but there are other problems with it, see bug
#616362):
gcc-4.4 -c -g -gnatwae -gnat05 -gnatwl -gnaty3abefhiklnprt
-I../lib/spark/current -I../common/versioning -gnatf -O1 -fstack-check sem.adb
raised STORAGE_ERROR : stack overflow (or erroneous memory access)
simplifier & checker - those two parts are written in prolog. I was able
to compile them using swi-prolog with some changes. But to be
sure that everything works some testing is needed.
wraputility - ok
pogs - ok
sparkformat - the same problem in dictionary-rawdict.adb as with
examiner.
sparkmake - ok
sparksimp - ok
viktor - ok
victor_wrapper - ok
So the largest problem for now is definition of RefType. And I'm not
sure at all what to do with it. Also I have no idea how binary
distribution for x86_64 was compiled. Maybe it was compiled with older
compuler that does not emit that warning and binary distribution is
broken? This is from gdb:
(gdb) print examinerconstants.RefType(0xffffffff)
$5 = -1
Any ideas?
Regards,
Eugeniy Meshcheryakov
signature.asc
Description: Digital signature
