Future versions of SPARK will retire `Overflow_Mode` / `-gnato??` in favor of `Ada.Numerics.Big_Numbers.Big_Integers` whjich is more flexible. Unless we plan to execute contracts in the runtime, adding the specification should suffice to use big numbers in contracts.
Future versions of SPARK will retire
Overflow_Mode/-gnato??in favor ofAda.Numerics.Big_Numbers.Big_Integerswhjich is more flexible.Unless we plan to execute contracts in the runtime, adding the specification should suffice to use big numbers in contracts.