Re: fyi, GNAT and SPARK GPL 2016 are out

[Simon Wright <simon@pushface.org>]

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.