nestedLoops: RuntimeException: Undefined value found.

[zirkel]

Running compare on nestedLoopsSpec_2.mmp and nestedLoopsImpl_2.mmp gives the following:

java.lang.RuntimeException: Undefined value found.

at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:115)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:164)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:164)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:176)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.valid(CVC3TheoremProver.java:341)
at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.valid(SymUniverse.java:1552)
at edu.udel.cis.vsl.minimp.value.impl.ValueFactory.valid(ValueFactory.java:299)
at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:124)
at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:1)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:100)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:252)
at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:1)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:100)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
at edu.udel.cis.vsl.minimp.verify.Verification.compare(Verification.java:160)
at edu.udel.cis.vsl.minimp.test.NestedLoopsTest.testCompare(NestedLoopsTest.java:91)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.junit.internal.runners.TestMethodRunner.executeMethodBody(TestMethodRunner.java:99)
at org.junit.internal.runners.TestMethodRunner.runUnprotected(TestMethodRunner.java:81)
at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
at org.junit.internal.runners.TestMethodRunner.runMethod(TestMethodRunner.java:75)
at org.junit.internal.runners.TestMethodRunner.run(TestMethodRunner.java:45)
at org.junit.internal.runners.TestClassMethodsRunner.invokeTestMethod(TestClassMethodsRunner.java:66)
at org.junit.internal.runners.TestClassMethodsRunner.run(TestClassMethodsRunner.java:35)
at org.junit.internal.runners.TestClassRunner$1.runUnprotected(TestClassRunner.java:42)
at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
at org.junit.internal.runners.TestClassRunner.run(TestClassRunner.java:52)
at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:45)
at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:460)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:673)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:386)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:196)

[Stephen Siegel]

Steve & Yi fixed: problem was that k had undefined value. Modified value factory so that it checks if a variable has undefined value whenever a variable is evaluated. If value is undefined, execution exception is thrown and reported to user.