gnattest supports pragmas Precondition, Postcondition, and Test_Case, as well as corresponding aspects. Test routines are generated, one per each Test_Case associated with a tested subprogram. Those test routines have special wrappers for tested functions that have composition of pre- and postcondition of the subprogram with "requires" and "ensures" of the Test_Case (depending on the mode, pre and post either count for Nominal mode or do not count for Robustness mode).
The third example demonstrates how this works:
cd <install_prefix>/share/examples/gnattest/contracts gnattest --harness-dir=driver -Pcontracts.gpr
Putting actual checks within the range of the contract does not cause any error reports. For example, for the test routine which corresponds to test case 1:
Assert (Sqrt (9.0) = 3.0, "wrong sqrt");
and for the test routine corresponding to test case 2:
Assert (Sqrt (-5.0) = -1.0, "wrong error indication");
cd driver gprbuild -Ptest_driver test_runner
However, by changing 9.0 to 25.0 and 3.0 to 5.0, for example, you can get a precondition violation for test case one. Also, by using any otherwise correct but positive pair of numbers in the second test routine, you can also get a precondition violation. Postconditions are checked and reported the same way.