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;