Потому что у тебя опилки в голове.Читаем https://sites.radford.edu/~nokie/classes/320/std_lib_html/sy...:
procedure Asm (
Template : String;
Outputs : Asm_Output_Operand_List;
Inputs : Asm_Input_Operand_List;
Clobber : String := "";
Volatile : Boolean := False);
procedure Asm (
Template : String;
Outputs : Asm_Output_Operand := No_Output_Operands;
Inputs : Asm_Input_Operand_List;
Clobber : String := "";
Volatile : Boolean := False);
procedure Asm (
Template : String;
Outputs : Asm_Output_Operand_List;
Inputs : Asm_Input_Operand := No_Input_Operands;
Clobber : String := "";
Volatile : Boolean := False);
procedure Asm (
Template : String;
Outputs : Asm_Output_Operand := No_Output_Operands;
Inputs : Asm_Input_Operand := No_Input_Operands;
Clobber : String := "";
Volatile : Boolean := False);
function Asm (
Template : String;
Outputs : Asm_Output_Operand_List;
Inputs : Asm_Input_Operand_List;
Clobber : String := "";
Volatile : Boolean := False)
return Asm_Insn;
function Asm (
Template : String;
Outputs : Asm_Output_Operand := No_Output_Operands;
Inputs : Asm_Input_Operand_List;
Clobber : String := "";
Volatile : Boolean := False)
return Asm_Insn;
function Asm (
Template : String;
Outputs : Asm_Output_Operand_List;
Inputs : Asm_Input_Operand := No_Input_Operands;
Clobber : String := "";
Volatile : Boolean := False)
return Asm_Insn;
function Asm (
Template : String;
Outputs : Asm_Output_Operand := No_Output_Operands;
Inputs : Asm_Input_Operand := No_Input_Operands;
Clobber : String := "";
Volatile : Boolean := False)
return Asm_Insn;
Ты здесь видишь какие-нибудь контракты? А здесь?
procedure Cli
38 with
39 SPARK_Mode => Off
40 is
41 begin
42 System.Machine_Code.Asm
43 (Template => "cli",
44 Volatile => True);
45 end Cli;
А здесь они откуда-то взялись, хотя функция System.Machine_Code.Asm контрактов не имеет:
27 procedure Cli
28 with
29 Global => (In_Out => X86_64.State),
30 Depends => (X86_64.State =>+ null),
31 Inline_Always;
Ну, и откуда они взялись? А их приписал разработчик. Но мог написать другие, некорректные, или вовсе не писать. Получается "мамой клянусь". А ведь верификация на контрактах держится, без них тебе компилятор ничего за пределами Ada 2012 не гарантирует.