Hi,
I set pragma Assertion_Policy(Check) and my fraction operator “/” is set up like this:
pragma Ada_2022;
pragma Extensions_Allowed(All);
pragma Assertion_Policy(Check);
generic
type TInteger is range <> or use Integer;
type TFloat is digits <> or use Float;
package Fractions_ADT is
type Fractions is private;
Null_Fraction: constant Fractions;
function "/" (A, B: TInteger) return Fractions with Pre => (B/= 0);
function "/" (A: Fractions; B: TInteger) return Fractions with Pre => (B/= 0);
function "/" (A, B: Fractions) return Fractions with Pre => (B/= Null_Fraction);
function "/" (A: TInteger; B: Fractions) return Fractions with Pre => (B /= Null_Fraction);
I would like the precondition to be checked at compile time when the operatnd B is statiscally known. Which is the case here:
with Ada.Text_IO, Fractions_ADT;
procedure Essai_Fractions is
type Newfloat is digits 3;
package FP is new Fractions_ADT (TFloat => Newfloat);
use FP, Ada.Text_IO;
begin
Put_line("To_Float(-5/0)'Image);
end Essai_Fractions;
In fact, the contract isn’t checked at runtime either, since I get the exception "Constraint_Error (the denominator’s subtype excludes 0) and not Predicate_Failure. I haven’t got the hang of contracts yet.
Huh, eventhough the contract is on the specification ? Ok. It works. On runtime. But can’t GNAT complain at compile time with this ? Since the expression is statically known ?
It’s hard to tell because your code uses a qualified express using a record type wrapped around an integer type. It doesn’t compile for me. However, if I try out something simpler like:
Put_line(Integer(1/0)'Image);
Then GNAT catches it:
gcc -c jdoodle.adb
jdoodle.adb:18:24: error: division by zero
jdoodle.adb:18:24: error: static expression fails Constraint_Check
gnatmake: "jdoodle.adb" compilation error
Compilers can only do so much of this kind of static analysis. The “GNATSAS” static analysis suite analyzes control and data flow more completely than the compiler, and can verify many preconditions and postconditions statically.
After a cursory research, I assume it is not free or opensource, unlike GNAT… But then that means people can’t leverage the full-extent of the language without paying ? Did I miss something ?
GNATSAS is open source, but there is currently no “community” edition available for it. On the other hand, there is an open-source community version of SPARK, which provides a number of tools that perform formal verification of programs that use Ada pre- and postconditions, and can go well beyond GNATSAS in its proof capability. Here is the github site for it, which includes a description of how you can use the “alire” tool to install it:
SPARK is a subset of Ada, and requires more work on the programmer’s part to get the full value of its formal verification (e.g. preconditions and postconditions are required for SPARK to be most effective). GNATSAS runs on any Ada code, and tries to identify as many potential problems as it can, but it isn’t “proving” the program is correct, though it can be used to “prove” that the program doesn’t have a certain class of errors. This is pretty much the usual distinction between formal verification tools and static analysis tools.
I might add that you need to give GNAT the “-gnata” switch if you want it to insert run-time checks for assertion-like things such as Preconditions and Postconditions. Furthermore, you will only get a “predicate failure” if you are using one of the Predicate aspects (Static_Predicate, Dynamic_Predicate, or GNAT’s Predicate aspect – see Ada RM 3.2.4).
Doesn’t this conflict not only with ARM 11.4.2(10) but also with GNAT Reference Manual 2.16, which says that “If the policy is CHECK , then assertions are enabled, i.e. the corresponding pragma or aspect is activated. … This pragma overrides the effect of the -gnata switch on the command line.”
Good point. Explicit use of pragma Assertion_Policy can accomplish what “-gnata” does. However, at least in my experience, usually you are in a mode where you want everything checked, or you are in a mode where you want none of the assertion-like things checked. Turning the checks on and off individually with Assertion_Policy is usually finer-grained than is useful.
One thing I didn’t understand from the RM:
If you put the assertion policy pragma in the API package spec, does it only apply to the innards of that API package or is it supposed to apply to callers of the API operations in outside packags/subprograms?
My initial reading of the RM makes me thing it only applies to the innards of the API package (only its own package spec and body), but wasn’t sure.
In the example at the start of this thread, the pragma had to be applied to the unit in which the generic containing the preconditions was instantiated.
What is the rationale ? Can you point us to the relevant RM paragraph perhaps ?
Although it might sound like Chinese to me, on second though I am not certain it would help
I don’t know the rationale offhand. You might check the Annotated ARM ( Ada 2022 Language Reference Manual ) at the same section that Simon linked above and see if it has any rationale. Alternately you can read the Ada 2012 rationale document on the same site ( Ada 2012 Language Reference Manual ).
Thanks!!
That’s what I expected based on the OP, but I also know GNAT has a lot of bugs, so I was just checking since I didn’t understand the RM section
The assertion policy is relevant at the point of the declaration of the entity to which the assertion-like thing applies. Whatever assertion policy is set at the point of the declaration applies to all uses of the entity. So if it is a precondition, it applies to all callers if the assertion policy says “check” at the point of the declaration of the subprogram. Similarly, if it is a subtype predicate, the predicate is checked on all uses of the subtype (or objects thereof), if the assertion policy is “check” at the point of the subtype declaration.
The rationale is that you can presume the check has been performed by all users if the policy was “check” at the point of the declaration. That is a much more useful statement than having, for example, some callers performing the precondition check, and some not. The body of the subprogram would have to assume the worst in that case, rather than being able to rely on the precondition having been checked.
