diff options
| author | Claire Dross <dross@adacore.com> | 2022-11-25 16:28:47 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2022-11-28 13:02:31 +0100 |
| commit | 80ad275cf1e6f308d3bbafc34635eb56851d6862 (patch) | |
| tree | aef0bfd981f8d5a95f09000254fcc64948a386f6 /libgcc | |
| parent | e75d06f9bfad341aea3565f95fffb8937de5f142 (diff) | |
| download | gcc-80ad275cf1e6f308d3bbafc34635eb56851d6862.zip gcc-80ad275cf1e6f308d3bbafc34635eb56851d6862.tar.gz gcc-80ad275cf1e6f308d3bbafc34635eb56851d6862.tar.bz2 | |
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.
Diffstat (limited to 'libgcc')
0 files changed, 0 insertions, 0 deletions