search

jennalwise / graphblas-verif

Formal verification of the GraphBLAS C API implementation by Tim Davis using Frama-C/WP.
Other
5 stars 1 forks source link

Change (0..size-1) to (0 .. size-1) to ensure always parsed/interpreted correctly #10

Closed jennalwise closed 6 years ago

jennalwise commented 6 years ago

Quirk of the specification language is that (0..size-1) has to contain spaces around .., ie. (0 .. size-1). Need to make sure annotated code reflects this.

jennalwise commented 6 years ago

May have been fixed, since annotations in the frama-c libs don't always ensure spaces around .. . I will check and fix this as I verify different methods.