I made a mapped table of function pointers in SPARK.
I’ve noticed that the prover understands some aspects applied to a subprogram access type. I can take this basic type:
type Op_Procedure is access procedure (Target : in out Machine);
and then apply preconditions I want maintained, and the prover correctly understands these preconditions:
type Op_Procedure is access procedure (Target : in out Machine)
with Pre => Is_Running (Target);
I get this error if I use a subprogram access in an Always_Terminates
subprogram:
machines.adb:44:34: medium: aspect Always_Terminates on "Execute" could be incorrect, call via access-to-subprogram might be nonterminating
44 | Builtin_Procedures (Op).all (Self);
| ~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~
However, I am not allowed to apply Always_Terminates
to an access to subprogram the way that I can apply Pre
.
machines.ads:100:35: error: incorrect placement of aspect "Always_Terminates"
100 | with Pre => Is_Running (Target), Always_Terminates;
| ^~~~~~~~~~~~~~~~~
What is the reason for that?