Repository navigation
NullPointerExceptions when running SmartPulse on benchmarks #3
Description
I'm on Ubuntu 20.04, using the pre-built binaries for Ubuntu. Running SmartPulse on some of the examples from the benchmark folder, I have been getting NullPointerExceptions instead of proofs:
smartpulse GasDos.sol GasDos GasDos.spec
[2022-10-27 10:49:28,734 FATAL L292 ToolchainWalker]: The Plugin edu.utexas.cs.utopia.specLang has thrown an exception:
java.lang.NullPointerException
at edu.utexas.cs.utopia.specLang.UtopiaSpecLangObserver.instrument2(UtopiaSpecLangObserver.java:570)
at edu.utexas.cs.utopia.specLang.UtopiaSpecLangObserver.finish(UtopiaSpecLangObserver.java:1212)
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:317)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)
smartpulse IntegerOverflowFixed.sol IntOF IntegerOverflowFixed.spec
[2022-10-27 10:54:06,508 FATAL L292 ToolchainWalker]: The Plugin edu.utexas.cs.utopia.specLang has thrown an exception:
java.lang.NullPointerException
at edu.utexas.cs.utopia.specLang.UtopiaSpecLangObserver.fetchCorralChoice(UtopiaSpecLangObserver.java:318)
at edu.utexas.cs.utopia.specLang.UtopiaSpecLangObserver.instrument2(UtopiaSpecLangObserver.java:451)
at edu.utexas.cs.utopia.specLang.UtopiaSpecLangObserver.finish(UtopiaSpecLangObserver.java:1212)
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:317)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)
Activity