fyi, GNAT and SPARK GPL 2016 are out

fyi, GNAT and SPARK GPL 2016 are out

[Nasser M. Abbasi]

fyi;
got this email from Ada core today:
-----------------------------------

Dear GNAT and SPARK GPL user,

We are pleased to announce the availability of the GNAT
and SPARK GPL 2016 toolsets.

GNAT GPL 2016 incorporates upgraded technology for the debugger
(GDB 7.10) along with support for the Windows 10 platform and many new features.

Ada runtime support has been extended for the STM32f429-disco,
STM32f469-disco and STM32F7-disco development boards based on the STM32 family of microcontrollers.

* ravenscar sfp/full for the stm32f429-disco board
* ravenscar sfp/full for the stm32f469-disco board
* ravenscar sfp/full for the stm32f7-disco board

SPARK GPL 2016 - the formal method verification toolset - includes the following new features:

- Support for concurrency with Ravenscar and type predicates
- Generation of counterexamples for unproved checks
- Better support of bitwise (modular) operations in proof
- Generation of global summary table

You will find documentation about the GNAT GPL 2016 and SPARK GPL 2016 toolset here:

http://libre.adacore.com/developers/documentation

Both toolsets can be downloaded:
* from the "Download" section on GNAT Tracker for GAP users http://www.adacore.com/academia
* from libre site libre.adacore.com

Re: fyi, GNAT and SPARK GPL 2016 are out

[daserlang]

On Wednesday, June 1, 2016 at 9:33:58 AM UTC-4, Nasser M. Abbasi wrote:
> fyi;
> got this email from Ada core today:
> -----------------------------------
> 
> Dear GNAT and SPARK GPL user,
> 
> We are pleased to announce the availability of the GNAT
> and SPARK GPL 2016 toolsets.
> 
> GNAT GPL 2016 incorporates upgraded technology for the debugger
> (GDB 7.10) along with support for the Windows 10 platform and many new features.
> 
> Ada runtime support has been extended for the STM32f429-disco,
> STM32f469-disco and STM32F7-disco development boards based on the STM32 family of microcontrollers.
> 
> * ravenscar sfp/full for the stm32f429-disco board
> * ravenscar sfp/full for the stm32f469-disco board
> * ravenscar sfp/full for the stm32f7-disco board
> 
> SPARK GPL 2016 - the formal method verification toolset - includes the following new features:
> 
> - Support for concurrency with Ravenscar and type predicates
> - Generation of counterexamples for unproved checks
> - Better support of bitwise (modular) operations in proof
> - Generation of global summary table
> 
> You will find documentation about the GNAT GPL 2016 and SPARK GPL 2016 toolset here:
> 
> http://libre.adacore.com/developers/documentation
> 
> Both toolsets can be downloaded:
> * from the "Download" section on GNAT Tracker for GAP users http://www.adacore.com/academia
> * from libre site libre.adacore.com

That's pretty cool.

I am curious.  Does anyone use SPARK at their job or hobby?  What's your experience like?

Re: fyi, GNAT and SPARK GPL 2016 are out

[mockturtle]

> I am curious.  Does anyone use SPARK at their job or hobby?  What's your experience like?

Almost... in the sense that I am planning to play with it (I'm curious), but so far I did not do yet.

Riccardo

Re: fyi, GNAT and SPARK GPL 2016 are out

[David Botton]

Did they fix the license bug in their runtimes or does it still virus the produced executables to be GPL only?

Re: fyi, GNAT and SPARK GPL 2016 are out

[Simon Wright]

David Botton <david@botton.com> writes:

> Did they fix the license bug in their runtimes or does it still virus
> the produced executables to be GPL only?

Still GPL-only.

Re: fyi, GNAT and SPARK GPL 2016 are out

[gautier_niouzes]

Nice release - with new optimizations in the run-time library... and a nice banana skin. In some cases, an application working well with GNAT for years may crash with a nasty raised PROGRAM_ERROR : EXCEPTION_ACCESS_VIOLATION - but only in a typical release mode; in a typical debug mode it works as before.

In a nutshell, if you are using Ada.Containers.*Maps, and have code like the P_KO procedure below, which is legal Ada 2005 & 2012, the executable will bomb when built with the -gnatp switch.

The cure is to use a cursor like in P_OK. It removes an exception part as well.

Is there an inclusion of pragma Suppress(Container_Checks) into the standard on its way ? Then the remarks such as A.18.4, 69/2 could be updated accordingly.
_________________________ 
Gautier's Ada programming 
http://gautiersblog.blogspot.com/search/label/Ada 
NB: follow the above link for a valid e-mail address 

-----------8<-----------8<-----------8<-----------8<-------

--  GNAT GPL 2016 pragma, suppression included in -gnatp switch
pragma Suppress(Container_Checks); 

with Ada.Strings.Unbounded.Hash;             use Ada.Strings.Unbounded;
with Ada.Containers.Hashed_Maps;
with Ada.Text_IO; use Ada.Text_IO;

procedure Test_2016 is

  package T_Dic is new Ada.Containers.Hashed_Maps
    (Key_Type        => Ada.Strings.Unbounded.Unbounded_String,
     Element_Type    => Positive,
     Hash            => Ada.Strings.Unbounded.Hash,
     Equivalent_Keys => Ada.Strings.Unbounded."=");
  
  dic: T_Dic.Map;
  n: Positive:= 1;
  
  procedure P_KO(s: String) is
    i: Integer;
  begin
    i:= dic.Element(To_Unbounded_String(s));
    Put_Line("Key found, element=" & Integer'Image(i));
  exception
    when Constraint_Error =>  --  A.18.4, 69/2
      Put_Line("Key not found");
      dic.Insert(To_Unbounded_String(s), n);
      n:= n + 1;
  end P_KO;
  
  procedure P_OK(s: String) is
    i: Integer;
    use T_Dic;
    curs: Cursor;
  begin
    curs:= dic.Find(To_Unbounded_String(s));
    if curs = No_Element then
      Put_Line("Key not found");
      dic.Insert(To_Unbounded_String(s), n);
      n:= n + 1;
    else
      i:= Element(curs);
      Put_Line("Key found, element=" & Integer'Image(i));
    end if;
  end P_OK;

begin
  P_OK("A");
  P_OK("A");
  P_KO("B");
  P_KO("B");
end;

Re: fyi, GNAT and SPARK GPL 2016 are out

[Georg Bauhaus]

On 04.06.16 18:13, gautier_niouzes@hotmail.com wrote:
> Is there an inclusion of pragma Suppress(Container_Checks) into the standard on its way ? Then the remarks such as A.18.4, 69/2 could be updated accordingly.

Doesn't your workaround demonstrate just how the behavior
shown by GNAT contradicts the one to expect from standards
conformance? Or is -gnatp now overruling the effect which

     Element (No_Element)

is supposed to have?

If this call is not the subject of some ACATS test, perhaps it
should become one?

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: fyi, GNAT and SPARK GPL 2016 are out

[Jeffrey R. Carter]

On 06/04/2016 09:13 AM, gautier_niouzes@hotmail.com wrote:
> 
> In a nutshell, if you are using Ada.Containers.*Maps, and have code like the
> P_KO procedure below, which is legal Ada 2005 & 2012, the executable will
> bomb when built with the -gnatp switch.

Apparently other containers as well, such as the example shown by Mosteo for
indefinite lists, though he's getting Storage_Error.

-- 
Jeff Carter
"Crucifixion's a doddle."
Monty Python's Life of Brian
82

Re: fyi, GNAT and SPARK GPL 2016 are out

[gautier_niouzes]

Le samedi 4 juin 2016 18:31:29 UTC+2, Georg Bauhaus a écrit :

> Doesn't your workaround demonstrate just how the behavior
> shown by GNAT contradicts the one to expect from standards
> conformance? Or is -gnatp now overruling the effect which
> 
>      Element (No_Element)
> 
> is supposed to have?

Indeed. Without pragma Suppress(Container_Checks) you get the RM05/12 behavior:
raised CONSTRAINT_ERROR : Test_2016.T_Dic.Element: Position cursor of function Element equals No_Element

(A.18.4 Maps: 33/2
function Element (Position : Cursor) return Element_Type;
34/2
If Position equals No_Element, then Constraint_Error is propagated. Otherwise, Element returns the element component of the node designated by Position.)

with pragma Suppress(Container_Checks) (or with -gnatp) you get
raised PROGRAM_ERROR : EXCEPTION_ACCESS_VIOLATION

No coincidence, since you have in a-cohama.adb (GPL 2016 version):
   function Element (Position : Cursor) return Element_Type is
   begin
      if Checks and then Position.Node = null then
         raise Constraint_Error with
           "Position cursor of function Element equals No_Element";
      end if;
      ...
and (one click away):
   Checks : constant Boolean := Container_Checks'Enabled;

Hence my question about Container_Checks being in a future version of the standard...
_________________________ 
Gautier's Ada programming 
http://sf.net/users/gdemont/

Re: fyi, GNAT and SPARK GPL 2016 are out

[Simon Wright]

Georg Bauhaus <bauhaus@futureapps.invalid> writes:

> On 04.06.16 18:13, gautier_niouzes@hotmail.com wrote:
>> Is there an inclusion of pragma Suppress(Container_Checks) into the
>> standard on its way ? Then the remarks such as A.18.4, 69/2 could be
>> updated accordingly.
>
> Doesn't your workaround demonstrate just how the behavior
> shown by GNAT contradicts the one to expect from standards
> conformance? Or is -gnatp now overruling the effect which
>
>     Element (No_Element)
>
> is supposed to have?
>
> If this call is not the subject of some ACATS test, perhaps it
> should become one?

-gnatp means "suppress all checks". So if you were to compile your
program with this option (at least without extensive testing, or proof),
it would be on your own head if it failed.

It looks as though the Windows compiler doesn't handle access violation
(which would normally be protected by a check) usefully.

Running the test_2016 program with Container_Checks suppressed under
gdb on OS X, I get

(gdb) catch exception
Catchpoint 1: all Ada exceptions
(gdb) run
Starting program: /Users/simon/tmp/cla/test_2016 
Key not found
Key found, element= 1

Program received signal SIGSEGV, Segmentation fault.
0x0000000100008619 in test_2016.t_dic.element (container=..., key=...)
    at /opt/gnat-gpl-2016/lib/gcc/x86_64-apple-darwin14.5.0/4.9.4/adainclude/a-cohama.adb:352
352	      return Node.Element;
(gdb) bt
#0  0x0000000100008619 in test_2016.t_dic.element (container=..., key=...)
    at /opt/gnat-gpl-2016/lib/gcc/x86_64-apple-darwin14.5.0/4.9.4/adainclude/a-cohama.adb:352
#1  0x000000010000b577 in test_2016.p_ko (s=...) at test_2016.adb:22
#2  0x0000000100006127 in test_2016 () at test_2016.adb:50
(gdb) l
347	      if Checks and then Node = null then
348	         raise Constraint_Error with
349	           "no element available because key not in map";
350	      end if;
351	
352	      return Node.Element;
353	   end Element;
354	
355	   function Element (Position : Cursor) return Element_Type is
356	   begin
(gdb) c
Continuing.

Catchpoint 1, CONSTRAINT_ERROR (erroneous memory access) at 0x000000010000b577 in test_2016.p_ko (s=...) at test_2016.adb:22
22	      i:= dic.Element(To_Unbounded_String(s));

whereas with Container_Checks not suppressed I see

Starting program: /Users/simon/tmp/cla/test_2016 
Key not found
Key found, element= 1

Catchpoint 1, CONSTRAINT_ERROR (Test_2016.T_Dic.Element: no element available because key not in map) at 0x000000010000d73d in test_2016.p_ko (s=...) at test_2016.adb:22
22	      i:= dic.Element(To_Unbounded_String(s));

so in both cases I get CE.

Re: fyi, GNAT and SPARK GPL 2016 are out

[ogpual]

Can anyone explain why my Ocaml builds started failing when I installed this new gnat release on linux mint? I think I understand that Ocaml uses gcc and gnat needs a gcc that does Ada where it will get found on the path.  However gcc is a compiler collection, and a collection that renders all elements after the first useless is severely limited.  Does the gnat gcc use a different search strategy for libraries or such that befuddles Ocaml?  Is there any standard way to get the different typical uses of gcc to work like they should?

Re: fyi, GNAT and SPARK GPL 2016 are out

[Simon Wright]

ogpual@gmail.com writes:

> Can anyone explain why my Ocaml builds started failing when I
> installed this new gnat release on linux mint?

Not specifically, but if you could say some more about the errors you
see when the builds fail it might help.

Also,
  where have you installed GNAT?
  what is your PATH? (and what used it to be before the GNAT install?)

Re: fyi, GNAT and SPARK GPL 2016 are out

[ogpual]

On Saturday, June 4, 2016 at 2:49:07 PM UTC-7, Simon Wright wrote:
> ogpual@gmail.com writes:
> 
> > Can anyone explain why my Ocaml builds started failing when I
> > installed this new gnat release on linux mint?
> 
> Not specifically, but if you could say some more about the errors you
> see when the builds fail it might help.
> 
> Also,
>   where have you installed GNAT?
>   what is your PATH? (and what used it to be before the GNAT install?)

The Ocaml opam install would fail with a shared library not found:  

/usr/gnat/bin/../libexec/gcc/x86_64-pc-linux-gnu/4.9.4/ld: cannot find libncurses.so.5

The ld on my path actually was /usr/bin/ld, but for some reason the one shown above was getting used.  I had inserted /usr/gnat/bin/ near the front of my path to get the new gnat release to run, and the gcc on my path was /usr/gnat/bin/gcc.


With gnat on my path after the standard binutils,  I get this from gprbuild:

Error: no native compiler found for language 'ada', default runtime

Re: fyi, GNAT and SPARK GPL 2016 are out

[Randy Brukardt]

<gautier_niouzes@hotmail.com> wrote in message 
news:b7b10479-4cbe-49f8-8db4-29611b736cb3@googlegroups.com...
...
>Is there an inclusion of pragma Suppress(Container_Checks) into the 
>standard
>on its way ? Then the remarks such as A.18.4, 69/2 could be updated 
>accordingly.

Unknown at this time; my preference is to give the containers proper Ada 
2012 preconditions; then one would use the normal Assertion_Policy to 
eliminate the checks. If we don't do that, then there probably would be a 
pragma Suppress.

                               Randy.

Re: fyi, GNAT and SPARK GPL 2016 are out

[Randy Brukardt]

"Georg Bauhaus" <bauhaus@futureapps.invalid> wrote in message 
news:niuvov$kvf$1@dont-email.me...
> On 04.06.16 18:13, gautier_niouzes@hotmail.com wrote:
>> Is there an inclusion of pragma Suppress(Container_Checks) into the 
>> standard on its way ? Then the remarks such as A.18.4, 69/2 could be 
>> updated accordingly.
>
> Doesn't your workaround demonstrate just how the behavior
> shown by GNAT contradicts the one to expect from standards
> conformance? Or is -gnatp now overruling the effect which
>
>     Element (No_Element)
>
> is supposed to have?
>
> If this call is not the subject of some ACATS test, perhaps it
> should become one?

I believe that is covered by an ACATS test. But it's irrelevant in this 
case, as one runs the ACATS with a particular set of options (which 
certainly does not include -gnatp). Every compiler has options that aren't 
(strictly speaking) Standards-conforming. Don't use those if you care. ;-)

                                          Randy.

Re: fyi, GNAT and SPARK GPL 2016 are out

[ahlan.marriott]

On Friday, 3 June 2016 09:16:09 UTC+2, Simon Wright  wrote:
> David Botton <david@botton.com> writes:
> 
> > Did they fix the license bug in their runtimes or does it still virus
> > the produced executables to be GPL only?
> 
> Still GPL-only.

Dear Simon,

Regarding licensing...
How can you find out under which license an executable was produced?
Is there a tool you can run on the executable or what?

Best wishes,
Ahlan

Re: fyi, GNAT and SPARK GPL 2016 are out

[gautier_niouzes]

Le dimanche 5 juin 2016 10:00:45 UTC+2, ahlan.m...@gmail.com a écrit :

> Regarding licensing...
> How can you find out under which license an executable was produced?
> Is there a tool you can run on the executable or what?

Yes, Notepad for instance. Open the executable and search for "GNAT Version"...

Now, from within the Ada program you can also get it: have a look at package GNAT.Compiler_Version
_________________________ 
Gautier's Ada programming 
http://gautiersblog.blogspot.com/search/label/Ada 
NB: follow the above link for a valid e-mail address 

Re: fyi, GNAT and SPARK GPL 2016 are out

[gautier_niouzes]

Le samedi 4 juin 2016 21:34:44 UTC+2, Simon Wright a écrit :

> It looks as though the Windows compiler doesn't handle access violation
> (which would normally be protected by a check) usefully.
> 
> Running the test_2016 program with Container_Checks suppressed under
> gdb on OS X, I get

Sure, it is well known that things work better on a Mac than on Windows ;-).
Perhaps it depends also on other switches such as -O2. Usually -gnatp is lost among a long list of options, like:
"-O2", "-gnatn", "-gnatp", "-fno-strict-aliasing", "-fipa-cp-clone", "-fgcse-after-reload", "-funroll-loops", "-fpeel-loops", "-ftracer", "-funswitch-loops", "-fweb", "-frename-registers", "-ftree-vectorize", "-mfpmath=sse", "-msse3"
_________________________ 
Gautier's Ada programming 
http://www.openhub.net/accounts/gautier_bd

Re: fyi, GNAT and SPARK GPL 2016 are out

[Simon Wright]

gautier_niouzes@hotmail.com writes:

> Le dimanche 5 juin 2016 10:00:45 UTC+2, ahlan.m...@gmail.com a écrit :
>
>> Regarding licensing...
>> How can you find out under which license an executable was produced?
>> Is there a tool you can run on the executable or what?
>
> Yes, Notepad for instance. Open the executable and search for "GNAT
> Version"...
>
> Now, from within the Ada program you can also get it: have a look at
> package GNAT.Compiler_Version

or on a Unix box
   $ strings {executable} | grep -i 'gnat version'

If this comes up with something like "GNAT Version: 6.1.0" there is a
pretty good chance that the executable was built against an RTS with the
GCC Runtime Library Exception.

But if it comes up with something like "GNAT Version: GPL 2016
(20160515-49)" then there still exists the remote possibility that the
RTS that was used did have the GCC Runtime Library Exception.

That would depend on someone investing quite a bit of patience in
getting the RTS to build and then checking it - hence, "remote".

If you're building for an embedded target, it's extremely unlikely you'd
find "GNAT Version" in the executable.

Re: fyi, GNAT and SPARK GPL 2016 are out

[Alejandro R. Mosteo]

On 04/06/16 19:36, Jeffrey R. Carter wrote:
> On 06/04/2016 09:13 AM, gautier_niouzes@hotmail.com wrote:
>>
>> In a nutshell, if you are using Ada.Containers.*Maps, and have code like the
>> P_KO procedure below, which is legal Ada 2005 & 2012, the executable will
>> bomb when built with the -gnatp switch.
>
> Apparently other containers as well, such as the example shown by Mosteo for
> indefinite lists, though he's getting Storage_Error.

And I'm not suppressing any checks (but then I think my problem comes by 
way of interfaces, I always hit bugs with those, it's my curse).

Re: fyi, GNAT and SPARK GPL 2016 are out

[Hadrien Grasland]

Le mercredi 1 juin 2016 15:33:58 UTC+2, Nasser M. Abbasi a écrit :
> fyi;
> got this email from Ada core today:
> -----------------------------------
> 
> Dear GNAT and SPARK GPL user,
> 
> We are pleased to announce the availability of the GNAT
> and SPARK GPL 2016 toolsets.
> 
> GNAT GPL 2016 incorporates upgraded technology for the debugger
> (GDB 7.10) along with support for the Windows 10 platform and many new features.
> 
> Ada runtime support has been extended for the STM32f429-disco,
> STM32f469-disco and STM32F7-disco development boards based on the STM32 family of microcontrollers.
> 
> * ravenscar sfp/full for the stm32f429-disco board
> * ravenscar sfp/full for the stm32f469-disco board
> * ravenscar sfp/full for the stm32f7-disco board
> 
> SPARK GPL 2016 - the formal method verification toolset - includes the following new features:
> 
> - Support for concurrency with Ravenscar and type predicates
> - Generation of counterexamples for unproved checks
> - Better support of bitwise (modular) operations in proof
> - Generation of global summary table
> 
> You will find documentation about the GNAT GPL 2016 and SPARK GPL 2016 toolset here:
> 
> http://libre.adacore.com/developers/documentation
> 
> Both toolsets can be downloaded:
> * from the "Download" section on GNAT Tracker for GAP users http://www.adacore.com/academia
> * from libre site libre.adacore.com

Pretty nice release as far as I am concerned: I can finally retire all of my workarounds related to the interactions between expression functions, protected types, and tagged types :)

Re: fyi, GNAT and SPARK GPL 2016 are out

[Jeffrey R. Carter]

On 06/05/2016 07:07 AM, Alejandro R. Mosteo wrote:
> 
> And I'm not suppressing any checks (but then I think my problem comes by way of
> interfaces, I always hit bugs with those, it's my curse).

"IMHO, Interfaces are worthless."
Randy Brukardt

-- 
Jeff Carter
"Gentlemen, you can't fight in here. This is the War Room!"
Dr. Strangelove
30