It may be interesting to see what the annotation overhead of checking only memory safety, in particular array bounds is in practice.
So, it would be good to include a working version of
https://github.com/epfl-lara/verified-qoi/blob/fe22c0ff5f775ff65dc154e42f2c060ca635bedb/QOI.scala
It may be interesting to see what the annotation overhead of checking only memory safety, in particular array bounds is in practice.
So, it would be good to include a working version of
https://github.com/epfl-lara/verified-qoi/blob/fe22c0ff5f775ff65dc154e42f2c060ca635bedb/QOI.scala