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

Null pointers alias to eachother in EVA memory model; fix use of separated predicates #22

Open jennalwise opened 6 years ago

jennalwise commented 6 years ago

Use of separation predicates should involve checking for null pointers as EVA's memory model ensures null pointers alias, ie. \separated(null,null) == false.