Files
why3/lib/pvs/floating_point/SingleFormat.pvs
2012-08-03 15:36:28 +02:00

16 lines
256 B
Plaintext

SingleFormat: THEORY
BEGIN
% do not edit above this line
% Why3 single
single: TYPE+
% Why3 max_single
max_single: real = (33554430 * 10141204801825835211973625643008)
% Why3 max_int
max_int: int = 16777216
END SingleFormat