diff options
| author | Yannick Moy <moy@adacore.com> | 2022-09-02 10:40:56 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-12 10:16:51 +0200 |
| commit | 5ca1d6a4a544f3357fdf0594ddd6096d68405bf3 (patch) | |
| tree | c83db939db7608a5d07879be21cb9e1380ae1523 /gcc/ada/debug.adb | |
| parent | da4824bb3aa76f87ebcc4c583df1a7e163d489a8 (diff) | |
| download | gcc-5ca1d6a4a544f3357fdf0594ddd6096d68405bf3.zip gcc-5ca1d6a4a544f3357fdf0594ddd6096d68405bf3.tar.gz gcc-5ca1d6a4a544f3357fdf0594ddd6096d68405bf3.tar.bz2 | |
[Ada] Reject use in SPARK of Asm intrinsics for code insertions
SPARK does not allow code insertions. This applies also to
calls to Asm intrinsics defined in System.Machine_Code.
gcc/ada/
* libgnat/s-maccod.ads: Mark package as SPARK_Mode Off.
Diffstat (limited to 'gcc/ada/debug.adb')
0 files changed, 0 insertions, 0 deletions