From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,9f79bf3a95fa27f0 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Received: by 10.68.223.40 with SMTP id qr8mr442904pbc.0.1338479889682; Thu, 31 May 2012 08:58:09 -0700 (PDT) Path: l9ni4183pbj.0!nntp.google.com!news2.google.com!goblin2!goblin1!goblin.stu.neva.ru!newsfeed.datemas.de!newsfeed.x-privat.org!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: Tero Koskinen Newsgroups: comp.lang.ada Subject: Re: gnat on debian arm Date: Thu, 31 May 2012 18:58:01 +0300 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: <20120531185801.51e93d86262e008c3fb3e0bb@iki.fi> References: <16156496.430.1335368506343.JavaMail.geo-discussion-forums@vbfg3> <2686916.432.1335368932863.JavaMail.geo-discussion-forums@vbbcc6> <26671007.3422.1335369791593.JavaMail.geo-discussion-forums@vbbfr18> <0e3eb9b5-b250-4780-964b-d52148f4636f@googlegroups.com> <8362ce33-33fb-47e9-8d49-520a15d2733d@fr28g2000vbb.googlegroups.com> NNTP-Posting-Host: dsl-trebrasgw2-fe9cde00-96.dhcp.inet.fi Mime-Version: 1.0 X-Trace: munin.nbi.dk 1338479884 32703 80.222.156.96 (31 May 2012 15:58:04 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 31 May 2012 15:58:04 +0000 (UTC) X-Newsreader: Sylpheed 3.2.0beta6 (GTK+ 2.24.10; x86_64-redhat-linux-gnu) Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Date: 2012-05-31T18:58:01+03:00 List-Id: Hi, On Wed, 30 May 2012 06:53:40 -0700 (PDT) Ludovic Brenta 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 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: ... 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: Євгеній Мещеряков 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: 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/