Re: gnat on debian arm

[Tero Koskinen <tero.koskinen@iki.fi>]

Hi,

On Wed, 30 May 2012 06:53:40 -0700 (PDT)
Ludovic Brenta <ludovic@ludovic-brenta.org> wrote:

> Roderick Chapman wrote on comp.lang.ada:
> > My Raspberry Pi arrived this morning, so a port of the SPARK
> > Examiner might be on the cards next... :-)
> 
> Already done IIUC, simply say:
> 
> aptitude install spark
> 
> on Debian testing or unstable on your Raspberry Pi

Spark does not seem to work on my Gumstix Overo with Debian sid/armhf:
[15:54 gumstix:21] ~/tmp/s 
% file /usr/bin/spark
/usr/bin/spark: ELF 32-bit LSB executable, ARM, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.26, BuildID[sha1]=0x78a4a2b6adb64112268ce9ad41bdc0b29b7527ff, stripped
[15:54 gumstix:22] ~/tmp/s 
% spark
zsh: killed     spark
[15:55 gumstix:23] ~/tmp/s 
% gdb spark
GNU gdb (GDB) 7.4.1-debian
Copyright (C) 2012 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.  Type "show copying"
and "show warranty" for details.
This GDB was configured as "arm-linux-gnueabihf".
For bug reporting instructions, please see:
<http://www.gnu.org/software/gdb/bugs/>...
Reading symbols from /usr/bin/spark...(no debugging symbols found)...done.
(gdb) run
Starting program: /usr/bin/spark 
During startup program terminated with signal SIGKILL, Killed.
(gdb) start
Function "main" not defined.
Make breakpoint pending on future shared library load? (y or [n]) y

Temporary breakpoint 1 (main) pending.
Starting program: /usr/bin/spark 
During startup program terminated with signal SIGKILL, Killed.
(gdb)

% apt-cache show spark
Package: spark
Version: 2011.0.deb-5
Installed-Size: 6161
Maintainer: Євгеній Мещеряков <eugen@debian.org>
Architecture: armhf
Depends: libc6 (>= 2.13-28), libgcc1 (>= 1:4.4.0), libgmp10, libgnat-4.6 (>= 4.6.3-3), libstdc++6 (>= 4.4.0), swi-prolog-nox (>= 5.10.4~)
Suggests: gnat, alt-ergo
Description-en: SPARK programming language toolset
 SPARK is a formally-defined computer programming language based on the
 Ada programming language, intended to be secure and to support the
 development of high integrity software used in applications and systems
 where predictable and highly reliable operation is essential either for
 reasons of safety or for business integrity.
 .
 This package contains the tools necessary for checking if programs adhere
 to the SPARK rules and the tools to show freedom of runtime exceptions in
 those programs. To compile SPARK programs use any standards-compliant Ada
 compiler, such as GNAT.
Homepage: http://libre.adacore.com/libre/tools/spark-gpl-edition/
Description-md5: 0512d6610268f233b9345bda401dbf34
Tag: devel::lang:ada, implemented-in::ada, interface::commandline,
 role::program, works-with::software:source
Section: devel
Priority: optional
Filename: pool/main/s/spark/spark_2011.0.deb-5_armhf.deb
Size: 2550856
MD5sum: fc2d4f2ff3e0fea69fbd57a0be9b18c8
SHA1: ed3622e1f1cb4d493e43193cbe10ff7b4ed83483
SHA256: 67f3ed2d7bb4a3f6aae1520dd0f5c05376d446b0d8d00e7700de85b09d360324

[15:56 gumstix:25] ~/tmp/s 
% 


'checker' works:

[15:56 gumstix:25] ~/tmp/s 
% checker
SPARK Proof Checker GPL 2011
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.



Please type filename, without extension, in lowercase, within single
quotes if it is not in this directory, followed by a full-stop.
FILENAME.vcg and FILENAME.fdl will be read.
Filename? abc.

No .vcg file of this name exists.

List of .vcg files in current region:
       <THERE ARE NONE>Please try again.

Please type filename, without extension, in lowercase, within single
quotes if it is not in this directory, followed by a full-stop.
FILENAME.vcg and FILENAME.fdl will be read.
Filename? .

errorStream user_input:10:18 Syntax error: Unexpected end of clause
 


-- 
Tero Koskinen - http://iki.fi/tero.koskinen/