issues
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
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
GB_Matrix_clear assigns clause not proving correctly
#25
jennalwise
opened
6 years ago
0
All free methods should be able to handle non valid matrices
#24
jennalwise
opened
6 years ago
0
Need extra requires statements for callee's preconditions (WP)
#23
jennalwise
opened
6 years ago
1
Null pointers alias to eachother in EVA memory model; fix use of separated predicates
#22
jennalwise
opened
6 years ago
0
Annot matrix multiply
#21
jennalwise
closed
6 years ago
0
Annot matrix nrows & ncols
#20
jennalwise
closed
6 years ago
0
Added extra requires clauses for RTE gaurds where behaviors exist
#19
jennalwise
closed
6 years ago
0
Move assigns/frees/allocates clauses out of behaviors
#18
jennalwise
closed
6 years ago
0
GB_Matrix_free does not ensure anything about internal aliased objects: GrB_Type, GrB_BinaryOp, etc.
#17
jennalwise
opened
6 years ago
0
EVA crashing on shallow_cast annotation
#16
jennalwise
closed
6 years ago
1
Annotation for GrB_Matrix_new & dependencies should include matrix_storage_init pred
#15
jennalwise
closed
6 years ago
1
Change \pow(2,60) to (GrB_Index) (1ULL << 60) everywhere in annotations
#14
jennalwise
closed
6 years ago
0
Possible bug in identity_is_zero_bool_valid predicate for monoid validation
#13
jennalwise
opened
6 years ago
0
Refactor the logic function name matrix_nvals to matrix_nzmax
#12
jennalwise
opened
6 years ago
0
Verify global and local thread storage
#11
jennalwise
opened
6 years ago
0
Change (0..size-1) to (0 .. size-1) to ensure always parsed/interpreted correctly
#10
jennalwise
closed
6 years ago
1
Refactor annotlib.acsl preds & logic functions to ensure sound casting of ptrs (void ptrs in particular)
#9
jennalwise
closed
6 years ago
1
Annotated the verification of valid graphblas structs
#8
jennalwise
closed
6 years ago
1
GraphBLAS struct memory footprints may be incorrect and need refactored
#7
jennalwise
opened
6 years ago
0
A valid semiring should have a valid commutative monoid
#6
jennalwise
opened
6 years ago
1
Try refactoring predicate/logic functions in annotlib.acsl for increased elegance and encapsulation
#5
jennalwise
opened
6 years ago
0
Valid matrices should have correct number of zombies
#4
jennalwise
opened
6 years ago
0
Verify the matrix queue linked list internal to matrix structs
#3
jennalwise
opened
6 years ago
1
Verify algebraic properties of monoids in monoid_valid predicate
#2
jennalwise
opened
6 years ago
1
Equality of specified objects
#1
jennalwise
opened
6 years ago
0