nishanttotla/cpachecker-crowdprover

An oracle-guided heap invariant synthesizer built using CPAchecker (v1.4)

cpachecker-crowdprover's Issues

Changes to Universal/Empty heap need to be handled specially

Implement equals() and hashCode() functions for Graph components

Without this, they will result in unpredictable behavior in Maps and Sets. Check this: http://stackoverflow.com/questions/16069106/how-to-compare-two-java-objects

NULL pointers not defined by parser

Check GlobalScope.java. Either hack it to accept NULL, or ensure that each example has a global constant called NULL. The latter is easy for now.

Add more comments for classes in algorithm.impact package

The package contains several functions that are used for managing heap graphs which are missing good documentation.

Create separate predVarLabeling class for graph

This is required to keep track of how predicates evolve in our graph. The set of predicates that the graph deals with is fixed (and pre-decided), so we need to have a way to keep track of their values.

Graph does not deal with NULL pointers

Store/Alloc/Load functions have been defined without considering the NULL case. This must be fixed when NULL definitions exist in the program.

Node isRoot field isn't being updated

Whenever a node gets a new incoming pointer, update the isRoot field to reflect the fact.

If edge is removed, then all incoming edges need to searched for updating isRoot. Alternative is to maintain count of incoming/outgoing edges to optimize this.