From 5ca1d6a4a544f3357fdf0594ddd6096d68405bf3 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 2 Sep 2022 10:40:56 +0200 Subject: [PATCH] [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 | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/gcc/ada/libgnat/s-maccod.ads b/gcc/ada/libgnat/s-maccod.ads index c3abf07a9e78..df7c7df17b28 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; -- 2.47.2