CVS difference for acats/new/c611a032.am

Differences between 1.1 and version 1.2
Log of other versions for file acats/new/c611a032.am

--- acats/new/c611a032.am	2016/04/01 03:12:40	1.1
+++ acats/new/c611a032.am	2016/04/01 04:15:03	1.2
@@ -381,6 +381,141 @@
      end;
    end Test_Get_Distance2;
 
+
+   procedure Test_Get_Distance3 (O    : in C611A030.Child.Triangle;
+                                 Code : in Character) is
+      -- Test a statically bound call of Distance (where the real tag
+      -- might differ from the statically determined tag).
+
+      function TC_Eval_Object (O    : in C611A030.Object'Class)
+         return C611A030.Object'Class is
+         -- Called when the parameter of Distance is evaluated. Better
+         -- be before the precondition is evaluated.
+
+         -- Note: If we had this return the specific type (which is what
+         -- we really want), this would change the tag to that specific
+         -- type (which is definitely NOT what we really want). Thus the
+         -- silly call below.
+      begin
+         -- Check the objective:
+         --    Check that an enabled class-wide precondition of a subprogram S
+         --    is evaluated after evaluating the parameters of a call on S.
+
+         if F611A00.TC_Object_Distance_Pre_Class_Called or
+            F611A00.TC_Triangle_Distance_Pre_Class_Called then
+            Report.Failed
+               ("Class-wide precondition evaluated before the parameter was " &
+                "evaluated (statically bound call) - " & Code);
+            F611A00.TC_Output;
+         end if;
+         return O;
+      end TC_Eval_Object;
+
+
+      function Call_Get_Distance (O : in C611A030.Child.Triangle)
+         return Float is
+         Inner_Distance : Float;
+      begin
+         -- Statically bound call:
+         --Inner_Distance := O.Distance;
+         Inner_Distance :=
+            C611A030.Child.Triangle(TC_Eval_Object (O)).Distance;
+
+         -- Check the objective:
+         --    Check that an enabled class-wide postcondition of a subprogram S
+         --    is evaluated after completing the subprogram body but before
+         --    continuing execution after the call of S.
+         if not F611A00.TC_Object_Distance_Post_Class_Called then
+            Report.Failed
+             ("Post'Class should have been called before " &
+              "resuming after calling the subprogram body (statically " &
+              "bound call)- " & Code);
+            F611A00.TC_Output;
+         end if;
+
+         return Inner_Distance;
+      end Call_Get_Distance;
+   begin
+      declare
+      begin
+         Assertion_Error_Raised := False;
+         Order_Error_Raised := False;
+         Outer_Distance := Call_Get_Distance (O);
+
+         -- The following checks assume that the precondition and postcondition
+         -- of Distance both pass, but of course if either doesn't pass we
+         -- don't get here as an exception is raised.
+
+         -- In the following, the tag of O doesn't matter.
+
+         -- Check the following objective:
+         --    For a nonabstract tagged type T and a primitive subprogram S
+         --    of T and that has a class-wide postcondition expression E,
+         --    check that for a dynamically tagged dispatching call of S,
+         --    calls to primitive operations of T within E invoke the
+         --    bodies appropriate for the controlling tag, even if it is not
+         --    T.
+         if F611A00.TC_Object_Distance_Is_Positive_Called or
+            F611A00.TC_Object_Not_Too_Far_Called or
+            (not F611A00.TC_Triangle_Distance_Is_Positive_Called) or
+            (not F611A00.TC_Triangle_Not_Too_Far_Called) then
+            Report.Failed
+              ("Postcondition expressions should only have called " &
+               "primitives appropriate for the tag, and should have " &
+               "called all of them (statically bound call) - " & Code);
+            F611A00.TC_Output;
+         end if;
+
+         -- Check the following objective:
+         --    Check that if multiple enabled class-wide postconditions
+         --    apply to a subprogram S, check that they are all evaluated
+         --    if they all evaluate to True.
+         if not (F611A00.TC_Object_Distance_Post_Class_Called and
+                 F611A00.TC_Triangle_Distance_Post_Class_Called) then
+            Report.Failed
+              ("Hasn't called all classwide postconditions for a " &
+               "statically bound call - " & Code);
+            F611A00.TC_Output;
+         end if;
+
+         -- Check the following objective:
+         --    For a nonabstract tagged type T and a primitive subprogram S
+         --    of T and that has a class-wide precondition expression E,
+         --    check that for a dynamically tagged dispatching call of S,
+         --    calls to primitive operations of T within E invoke the
+         --    bodies appropriate for the controlling tag, even if it is not
+         --    T.
+         -- Note that we don't assume that both preconditions are evaluated
+         -- (if either are True, the other doesn't have to be evaluated),
+         -- but if a precondition is evaluated, make sure that the correct
+         -- routines are called.
+         if (F611A00.TC_Object_Distance_Pre_Class_Called and then
+               (F611A00.TC_Object_X_Coord_Called or
+                (not F611A00.TC_Triangle_X_Coord_Called))) or else
+            (F611A00.TC_Triangle_Distance_Pre_Class_Called and then
+               (F611A00.TC_Object_Y_Coord_Called or
+                (not F611A00.TC_Triangle_Y_Coord_Called))) then
+            Report.Failed
+              ("Precondition expressions should only have called " &
+               "primitives appropriate for the tag, and should have " &
+               "called all of them that were evaluated for a statically " &
+               "bound call - " & Code);
+            F611A00.TC_Output;
+         end if;
+
+         if Outer_Distance < 0.0 then -- Provide a sink so the whole
+                                      -- routine can't get optimized away:
+            Report.Failed
+               ("Result doesn't meet the postcondition - " & Code);
+         end if;
+      exception
+         when Ada.Assertions.Assertion_Error =>
+            Assertion_Error_Raised := True;
+         when F611A00.TC_Order_Error =>
+            Order_Error_Raised := True;
+     end;
+   end Test_Get_Distance3;
+
 begin
 
    Report.Test
@@ -595,6 +730,59 @@
       Report.Failed ("Postcondition should only have been called after the" &
         " subprogram body - E");
    end if;
+
+   -- Finally, check the objective:
+   --   If a subprogram S has multiple applicable class-wide preconditions,
+   --   that all such expressions evaluate to False before Assertion_Error
+   --   is raised.
+   -- To check this properly, we need a statically bound call for type
+   -- Triangle.
+
+   -- Should pass all of the preconditions and postconditions:
+
+   F611A00.TC_Clear;
+
+   My_Triangle.Move (X => 3.0, Y => 4.0);
+
+   Test_Get_Distance3 (My_Triangle, Code => 'K');
+
+   if Assertion_Error_Raised then
+      Report.Failed ("Assertion_Error raised - K");
+   elsif Order_Error_Raised then
+      Report.Failed ("Postcondition should only have been called after the" &
+        " subprogram body - K");
+   end if;
+
+   -- Should pass Object's Pre'Class but fail Triangle's Pre'Class.
+   -- This means that the precondition passes.
+
+   F611A00.TC_Clear;
+
+   My_Triangle.Move (X => 3.0, Y => -4.0);
+
+   Test_Get_Distance3 (My_Triangle, Code => 'L');
+
+   if Assertion_Error_Raised then
+      Report.Failed ("Assertion_Error raised - L");
+      -- Recall that a class-wide precondition passes if ANY of the expressions
+      -- evaluate to True (meaning the other can fail).
+   elsif Order_Error_Raised then
+      Report.Failed ("Postcondition should only have been called after the" &
+        " subprogram body - L");
+   end if;
+
+   -- Should fail Object's and Triangle's Pre'Class
+
+   F611A00.TC_Clear;
+
+   My_Triangle.Move (X => -3.0, Y => -4.0);
+
+   Test_Get_Distance3 (My_Triangle, Code => 'M');
+
+   if not Assertion_Error_Raised then
+      Report.Failed ("Assertion_Error not raised - M");
+   end if;
+   -- Don't care about the order of the postcondition.
 
    Report.Result;
 

Questions? Ask the ACAA Technical Agent