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 \pow(2,60) to (GrB_Index) (1ULL << 60) everywhere in annotations #14

Closed jennalwise closed 6 years ago

jennalwise commented 6 years ago

EVA and WP cannot discharge proofs with \pow(2,60), but can with 1ULL << 60; representing 2^60 which is the GB_INDEX_MAX.