search

kframework / c-semantics

Semantics of C in K
Other
305 stars 40 forks source link

Handling floating point #161

Open edgar-pek opened 8 years ago

edgar-pek commented 8 years ago

1.0f translates to Float(#"1e+00") instead of Float(#"1e+00f") Generally, account for both float and double constants.

dwightguth commented 8 years ago

To summarize, basically all three floating types are represented internally by 64-bit floats. What we need is:

  1. configuration settings for the mantissa and exponent size of each of the three floating point types (in settings.k)
  2. Updated fmin, fmax, etc based on the configuration settings
  3. Updated code representing floating point expressions to handle the correct precision of all values of floating type.
  4. Code to treat floating-point underflow as undefined behavior (ie if the result of computation is smaller than the smallest subnormal number)

Maybe some other stuff too, I'm not sure.