GNAT was evaluating the right part of an AND-THEN pre- or postcondition before
the left part, which could cause a wrong exception to be raised in case of a
failing pre- or postcondition.
On the code attached, compiling and executing now raises a precondition
failure instead of a division by zero:
$ gcc -c -gnat2012 -gnata main.adb
$ gnatbind -x main.ali
$ gnatlink main.ali
$ ./main
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from check.ads:3
---
package Check is
function Div (X : Integer) return Integer
with Pre => (X /= 0 and then 1/X > 0),
Post => (Div'Result > 0);
end Check;
---
package body Check is
function Div (X : Integer) return Integer is
begin
return X;
end Div;
end Check;
---
with Check;
procedure Main is
X : Integer;
begin
X := Check.Div (0);
end Main;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-04 Yannick Moy <m...@adacore.com>
* sem_ch13.adb (Analyze_Aspect_Specifications): correct order in which
the left-hand-side and right-hand-side of a conjunct are inserted when
translating a pre- or postcondition
* sem_ch6.adb: Correct typo in comment
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 177353)
+++ sem_ch6.adb (working copy)
@@ -9189,8 +9189,8 @@
-- will be executed at the start of the procedure. Note that
-- this processing reverses the order of the list, which is
-- what we want since new entries were chained to the head of
- -- the list. There can be more then one precondition when we
- -- use pragma Precondition
+ -- the list. There can be more than one precondition when we
+ -- use pragma Precondition.
if not Class_Present (Prag) then
Prepend (Grab_PPC, Declarations (N));
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 177344)
+++ sem_ch13.adb (working copy)
@@ -1086,6 +1086,12 @@
-- we generate separate Pre/Post aspects for the separate
-- clauses. Since we allow multiple pragmas, there is no
-- problem in allowing multiple Pre/Post aspects internally.
+ -- These should be treated in reverse order (B first and
+ -- A second) since they are later inserted just after N in
+ -- the order they are treated. This way, the pragma for A
+ -- ends up preceding the pragma for B, which may have an
+ -- importance for the error raised (either constraint error
+ -- or precondition error).
-- We do not do this for Pre'Class, since we have to put
-- these conditions together in a complex OR expression
@@ -1095,12 +1101,12 @@
then
while Nkind (Expr) = N_And_Then loop
Insert_After (Aspect,
- Make_Aspect_Specification (Sloc (Right_Opnd (Expr)),
+ Make_Aspect_Specification (Sloc (Left_Opnd (Expr)),
Identifier => Identifier (Aspect),
- Expression => Relocate_Node (Right_Opnd (Expr)),
+ Expression => Relocate_Node (Left_Opnd (Expr)),
Class_Present => Class_Present (Aspect),
Split_PPC => True));
- Rewrite (Expr, Relocate_Node (Left_Opnd (Expr)));
+ Rewrite (Expr, Relocate_Node (Right_Opnd (Expr)));
Eloc := Sloc (Expr);
end loop;
end if;
