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

EVA crashing on shallow_cast annotation #16

Closed jennalwise closed 6 years ago

jennalwise commented 6 years ago

Annotations for shallow_cast and cast_array written with minimal testing for matrix multiply. WP can parse the annotations fine, but EVA is crashing when being run on shallow_cast + its dependencies. Does not crash on cast_array. Need to fix this.

Something in matrix_valid predicate is crashing it.

jennalwise commented 6 years ago

Turns out EVA just needs a top level main function to initialize values, before it can verify shallow_cast and its dependencies; otherwise, it will crash on matrix_valid.