Opened 17 years ago
Closed 17 years ago
#16 closed defect (fixed)
symbolic exception: arrayloop_2
| Reported by: | Stephen Siegel | Owned by: | ywei |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | symbolic | Version: | 1.0 |
| Keywords: | Cc: | ywei@… |
Description
frederic:arrayloop siegel$ tass compare arrayloopSpec_2.mmp arrayloopImpl_2.mmp
MiniMP version 1.0
URL: http://vsl.cis.udel.edu
Minimp initialized with 1 process
Program runs in compare mode.
Program parsed succesfully.
IR generated succesfully.
java.lang.RuntimeException: Unknown symbolic expression: Undefined
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:170)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processWriteExpr(CVC3TheoremProver.java:252)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:166)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processWriteExpr(CVC3TheoremProver.java:252)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:166)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processWriteExpr(CVC3TheoremProver.java:252)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:166)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processWriteExpr(CVC3TheoremProver.java:252)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:166)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processSubscriptExpr(CVC3TheoremProver.java:239)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:162)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processSubscriptExpr(CVC3TheoremProver.java:239)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:162)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:142)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:420)
at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.plusExpression(SymUniverse.java:244)
at edu.udel.cis.vsl.minimp.value.impl.ValueFactory.add(ValueFactory.java:174)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateAdd(Evaluator.java:237)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:166)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:130)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeAssignment(Executor.java:139)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.execute(Executor.java:67)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:74)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:1)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:141)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:102)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
at edu.udel.cis.vsl.minimp.verify.Verification.compare(Verification.java:138)
at edu.udel.cis.vsl.minimp.Minimp.compareEquivalence(Minimp.java:356)
at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:375)
Trace from P1:
P1 Trace summary:
Step 1: State 0 -> arrayloopSpec_2.mmp line 11 proc 0 [main@0->main@1] "i = 0;" -> State 1
Step 2: State 1 -> arrayloopSpec_2.mmp line 12 proc 0 [main@1->main@2] "j = 0;" -> State 2
.
.
.
Change History (2)
comment:1 by , 17 years ago
| Cc: | added |
|---|---|
| Status: | new → assigned |
comment:2 by , 17 years ago
| Resolution: | → fixed |
|---|---|
| Status: | assigned → closed |
Fixed. The theorem prover will take care of the type issue.
I have replaced undefined initialization with symbolic constant initialization, but now I am getting a new exception in symbolic package when it encounters a 0 which should be treated as a float but it thinks is an integer....
R generated succesfully.
java.lang.RuntimeException: Type mismatch: Array entry has type SymRational but value has type SymInteger
Trace from P1:
P1 Trace summary:
Step 1: State 0 -> arrayloopSpec_2.mmp line 11 proc 0 [main@0->main@1] "i = 0;" -> State 1
Step 2: State 1 -> arrayloopSpec_2.mmp line 12 proc 0 [main@1->main@2] "j = 0;" -> State 2
Step 3: State 2 -> arrayloopSpec_2.mmp line 14 proc 0 [main@2->main@3] "while(i < N) " [true] -> State 3
Step 4: State 3 -> arrayloopSpec_2.mmp line 15 proc 0 [main@3->main@4] "while(j < N) " [true] -> State 4
Step 5: State 4 -> arrayloopSpec_2.mmp line 16 proc 0 [main@4->main@5] "D[i][j] = 0.0;"