Opened 17 years ago
Closed 17 years ago
#2 closed defect (fixed)
null pointer exception in Evaluator
| Reported by: | ywei | Owned by: | Stephen Siegel |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | semantics | Version: | 1.0 |
| Keywords: | Cc: |
Description
Revision 943, tile example:
java.lang.NullPointerException
java.lang.NullPointerException
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateVariable(Evaluator.java:371)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:144)
at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:105)
at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:35)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:90)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:78)
at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:153)
at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:42)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:90)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:78)
at edu.udel.cis.vsl.minimp.verify.Verification.compare(Verification.java:132)
at edu.udel.cis.vsl.minimp.Minimp.compareEquivalence(Minimp.java:241)
at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:260)
It seems that the Environment field in the Evaluator class is not set properly.
Fixed. There were some inputs variables in second model that were not input variables in first model---these needed to be assigned a new symbolic constant.