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

GB_Matrix_free does not ensure anything about internal aliased objects: GrB_Type, GrB_BinaryOp, etc. #17

Open jennalwise opened 6 years ago

jennalwise commented 6 years ago

GB_Matrix_free should probably ensure that internal graphblas objects are still valid, since they may alias with other objects which have not been freed or may be used in following program statements.

Matrix queue pointers will be handled when verifying the Matrix queue.