marcoeilers / nagini

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
Mozilla Public License 2.0
233 stars 8 forks source link

Optional modes for interpreted floats #160

Closed marcoeilers closed 10 months ago

marcoeilers commented 11 months ago

Adds the command line option --float-encoding=e, where e can be either real or ieee32. The current mode with uninterpreted floats remains the default, since both modes have disadvantages (reals are not a sound representation of floats, and ieee floating point reasoning is incredibly slow). When floating point operations are used in the default uninterpreted mode, a warning is issued.

This addresses issue #158.


This change is Reviewable