projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e75d06f) | patch
ada: Annotate GNAT.Source_Info with an abstract state
authorClaire Dross <dross@adacore.com>
Fri, 25 Nov 2022 15:28:47 +0000 (16:28 +0100)
committerMarc Poulhiès <poulhies@adacore.com>
Mon, 28 Nov 2022 12:02:31 +0000 (13:02 +0100)
commit80ad275cf1e6f308d3bbafc34635eb56851d6862
treeaef0bfd981f8d5a95f09000254fcc64948a386f6tree | snapshot
parente75d06f9bfad341aea3565f95fffb8937de5f142commit | diff
ada: Annotate GNAT.Source_Info with an abstract state

So it can be used safely from SPARK code. The abstract state represents
the source code information that is accessed by the functions defined
in Source_Info. It is volatile as it is updated asyncronously when
moving in the code.

gcc/ada/

* libgnat/g-souinf.ads (Source_Code_Information): Add a new
volatile abstract state and add it in the global contract of all
functions defined in Source_Info.
gcc/ada/libgnat/g-souinf.ads diff | blob | history
Domain: System / Toolchain;