diff options
Diffstat (limited to 'gcc/ada/a-extiin.ads')
| -rw-r--r-- | gcc/ada/a-extiin.ads | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/gcc/ada/a-extiin.ads b/gcc/ada/a-extiin.ads index 0105a4c88ff..8e8563dcdf1 100644 --- a/gcc/ada/a-extiin.ads +++ b/gcc/ada/a-extiin.ads @@ -14,12 +14,18 @@ ------------------------------------------------------------------------------ with Ada.Interrupts; +with Ada.Real_Time; -package Ada.Execution_Time.Interrupts is +package Ada.Execution_Time.Interrupts with + SPARK_Mode +is pragma Unimplemented_Unit; - function Clock (Interrupt : Ada.Interrupts.Interrupt_ID) return CPU_Time; + function Clock (Interrupt : Ada.Interrupts.Interrupt_ID) return CPU_Time + with + Volatile_Function, + Global => Ada.Real_Time.Clock_Time; function Supported (Interrupt : Ada.Interrupts.Interrupt_ID) return Boolean; |