Diagnostics · limit

limit[float-range]

A float literal that is not finite, or whose magnitude exceeds 2^53−1.

Floats are limited to the same magnitude as integers, so every literal compares exactly the same in every implementation.

Example

Through compileSource
CONTRACT Claim {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Request {
      count: int
      region: string
      ready: bool
      ratio: float
    }
    CONSTANTS {
      zero: int == 0 [SOURCE:POLICY]
      cap: int == 25 [SOURCE:POLICY]
    }
  }
  TRIGGER {
    grant()
  }
  GUARANTEE {
    ENSURE grant() WHEN Request.ready == true [SOURCE:must_be_ready]
  }
  PROHIBITION {
    FORBID grant WHEN Request.ratio > 1e300 [SOURCE:ratio]
  }
}

rejected limit[float-range] at 22:39 float literal outside supported finite domain

Fix

Through compileSource
CONTRACT Claim {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Request {
      count: int
      region: string
      ready: bool
      ratio: float
    }
    CONSTANTS {
      zero: int == 0 [SOURCE:POLICY]
      cap: int == 25 [SOURCE:POLICY]
    }
  }
  TRIGGER {
    grant()
  }
  GUARANTEE {
    ENSURE grant() WHEN Request.ready == true [SOURCE:must_be_ready]
  }
  PROHIBITION {
    FORBID grant WHEN Request.ratio > 1e15 [SOURCE:ratio]
  }
}

accepted

See also: the specification.