-
Notifications
You must be signed in to change notification settings - Fork 41
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
see #568: example program that triggers UnsupportedOperationException…
…: State has more than one call successor
- Loading branch information
1 parent
efc03c0
commit f6c5600
Showing
1 changed file
with
66 additions
and
0 deletions.
There are no files selected for viewing
66 changes: 66 additions & 0 deletions
66
trunk/examples/programs/regression/bpl/multipleCallSuccessors-01.bpl
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,66 @@ | ||
| //#Safe | ||
| /* | ||
| 20021-06-21 Daniel Dietsch | ||
| Necessary setting: | ||
| --traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg=true | ||
| java.lang.UnsupportedOperationException: State has more than one call successor | ||
| at de.uni_freiburg.informatik.ultimate.automata.nestedword.reachablestates.NestedWordAutomatonReachableStates$AncestorComputation$1.next(NestedWordAutomatonReachableStates.java:1771) | ||
| at de.uni_freiburg.informatik.ultimate.automata.nestedword.reachablestates.NestedWordAutomatonReachableStates$AncestorComputation$1.next(NestedWordAutomatonReachableStates.java:1) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.HoareAnnotationFragments.addDeadEndDoubleDeckers(HoareAnnotationFragments.java:288) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.BasicCegarLoop.computeAutomataDifference(BasicCegarLoop.java:908) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.BasicCegarLoop.refineAbstraction(BasicCegarLoop.java:771) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.iterateInternal(AbstractCegarLoop.java:468) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.iterate(AbstractCegarLoop.java:372) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.CegarLoopUtils.getCegarLoopResult(CegarLoopUtils.java:69) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.CegarLoopUtils.getCegarLoopResult(CegarLoopUtils.java:63) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.executeCegarLoop(TraceAbstractionStarter.java:383) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.analyseProgram(TraceAbstractionStarter.java:317) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.analyseSequentialProgram(TraceAbstractionStarter.java:277) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.runCegarLoops(TraceAbstractionStarter.java:175) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.<init>(TraceAbstractionStarter.java:154) | ||
| at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver.finish(TraceAbstractionObserver.java:124) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:168) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:151) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:128) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:232) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:226) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:142) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:104) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:320) | ||
| at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.RerunFreshToolchainJob.run(RerunFreshToolchainJob.java:91) | ||
| at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63) | ||
| */ | ||
|
|
||
| var x : int; | ||
|
|
||
| procedure main() | ||
| modifies x; | ||
| { | ||
| x:=0; | ||
| if(*){ | ||
| call foo1(); | ||
| } else if (*){ | ||
| call foo2(); | ||
| } else { | ||
| assume false; | ||
| } | ||
| assert x == 1; | ||
| } | ||
|
|
||
| procedure foo1() | ||
| modifies x; | ||
| { | ||
| x:=x+1; | ||
| } | ||
|
|
||
| procedure foo2() | ||
| modifies x; | ||
| { | ||
| x:=x+1; | ||
| } | ||
|
|
||
|
|
||
|
|
||
|
|