search

opprop / checker-framework-inference

Inference of pluggable types for Java
6 stars 13 forks source link

Lack of testcases for LogiQL and Z3BitVector backend #99

Open topnessman opened 6 years ago

topnessman commented 6 years ago

There is currently only Dataflow type system that enforces the soundness of MaxSAT solver engine. LogiQL and Z3BitVector backend don't have any tests that use them. It's easy to break the correctness during refactoring.

CharlesZ-Chen commented 6 years ago

I've set up a test suite that using Z3BitVector backend in Ontology. Will add this test suite as a downstream test of CFI, so that at least we will cover Z3BitVector backend in downstream.

I will add Z3BitVector test suite inside CFI when I integrated Dataflow Z3 BitVector backend into CFI.