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 | |
| 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')
| -rw-r--r-- | gcc/ada/libgnat/s-maccod.ads | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/s-maccod.ads b/gcc/ada/libgnat/s-maccod.ads index c3abf07..df7c7df 100644 --- a/gcc/ada/libgnat/s-maccod.ads +++ b/gcc/ada/libgnat/s-maccod.ads @@ -33,7 +33,9 @@ -- operations, and also for machine code statements. See GNAT documentation -- for full details. -package System.Machine_Code is +package System.Machine_Code + with SPARK_Mode => Off +is pragma No_Elaboration_Code_All; pragma Pure; |