Open wmdietl opened 6 months ago
In particular, for the test case from #692, the empty block for the loop body should have two predecessors: the condition and the loop body. It appears that the condition has the loop body as successor, but the loop body does not have the condition as predecessor.
The CFG invariants are encoded here:
https://github.com/eisop/checker-framework/blob/811e15dfd208ef5f0e5b1d6ed19e62c604045a0b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java#L151
At the moment they only run on one test:
https://github.com/eisop/checker-framework/blob/master/dataflow/src/test/java/cfgconstruction/CFGConstruction.java
Add a command-line option to check the invariants on a normal run and add a CI build that checks the invariants in all tests.
Look through the invariants and expand them if necessary.