mhatzl / vaton Goto Github PK

View Code? Open in Web Editor NEW

0.0 0.0 0.0 50 KB

Formally verified ASCII to number conversion written in Ada/SPARK.

License: MIT License

Ada 100.00%

vaton's People

Contributors

Watchers

vaton's Issues

[REQ] Prove floating point operations

Describe your feature request

Describe the solution you'd like

Proving floating point operations is needed to fully prove Vaton to be free of runtime errors.

Additional context

Floating point operations are difficult to prove (see https://www.adacore.com/uploads/techPapers/floats_spark.pdf), and the problem
is the generic setup not really allowing to narrow down the allowed range.

Not sure how to tell SPARK that the condition checks before guarantee that nothing can overflow without using pragma Assume().

[REQ] Prove `Long_Long_Integer`

Describe your feature request

Describe the solution you'd like

Prove all integer conversions to be free of runtime errors.

Additional context

At the moment, pragma Assume is used for one operation that is needed to pass gnatprove.
When switching it to pragma Assert, gnatprove fails to prove Long_Long_Integer conversions, but does not give any counterexample.

Really hard to find the cause.

Recommend Projects