]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: da4824b) | patch
[Ada] Reject use in SPARK of Asm intrinsics for code insertions
authorYannick Moy <moy@adacore.com>
Fri, 2 Sep 2022 08:40:56 +0000 (10:40 +0200)
committerMarc Poulhiès <poulhies@adacore.com>
Mon, 12 Sep 2022 08:16:51 +0000 (10:16 +0200)
commit5ca1d6a4a544f3357fdf0594ddd6096d68405bf3
treec83db939db7608a5d07879be21cb9e1380ae1523tree | snapshot
parentda4824bb3aa76f87ebcc4c583df1a7e163d489a8commit | diff
[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.
gcc/ada/libgnat/s-maccod.ads diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git