[feature] Ghost blocks

[clairedross]

Summary

We would like to annotate a declare block as ghost, so all the statements and declarations it contains are considered to be ghost.

Motivation

Ghost statements in GNAT are severely limited. Only assignments into ghost variables and calls to ghost procedures are considered to be ghost. It would be interesting to be able to do a ghost conditional, or a ghost loop, without having to create a nested subprogram.

Caveats and alternatives

I am not sure where the annotation could be located, as blocks are not entities. Maybe we could write:

declare
  ...
begin
  ...
end with Ghost;

[sttaft]

Seems weird to find out you are looking at a ghost block only when you reach the end.
I would add syntax to allow aspects on “declare” and “begin”. Hence:

    declare 
        with ghost 
         ….
    begin
        …
    end;

[clairedross]

I am happy with the annotation being on the begin or declare too.