./jayhorn -j tmp


--------------------------------------------------------------------------------


[root] - 		 ---   JAYHORN : Static Analayzer for Java Programs ---- 
[root] - 	 Verification : safety
[root] - 	 Solver : eldarica
[root] - Building CFG  ... 
Unable to validate method body. Possible NullPointerException?
(<Main: void main(java.lang.String[])>) local type not allowed in final code: null_type local: n0
	at soot.jimple.validation.TypesValidator.validate(TypesValidator.java:44)
	at soot.jimple.JimpleBody.validate(JimpleBody.java:125)
	at soot.jimple.JimpleBody.validate(JimpleBody.java:110)
	at soottocfg.soot.SootToCfg.performBehaviorPreservingTransformations(SootToCfg.java:342)
	at soottocfg.soot.SootToCfg.run(SootToCfg.java:118)
	at jayhorn.Main.safetyAnalysis(Main.java:52)
	at jayhorn.Main.main(Main.java:100)
2018-07-29 02:54:29,261 ERROR (main) [root] - (<Main: void main(java.lang.String[])>) local type not allowed in final code: null_type local: n0
Exception in thread "main" (<Main: void main(java.lang.String[])>) local type not allowed in final code: null_type local: n0
	at soot.jimple.validation.TypesValidator.validate(TypesValidator.java:44)
	at soot.jimple.JimpleBody.validate(JimpleBody.java:125)
	at soot.jimple.JimpleBody.validate(JimpleBody.java:110)
	at soottocfg.soot.transformers.AssertionReconstruction.reconstructJavaAssertions(AssertionReconstruction.java:290)
	at soottocfg.soot.transformers.AssertionReconstruction.transform(AssertionReconstruction.java:56)
	at soottocfg.soot.transformers.AssertionReconstruction.applyTransformation(AssertionReconstruction.java:48)
	at soottocfg.soot.SootToCfg.performBehaviorPreservingTransformations(SootToCfg.java:371)
	at soottocfg.soot.SootToCfg.run(SootToCfg.java:118)
	at jayhorn.Main.safetyAnalysis(Main.java:52)
	at jayhorn.Main.main(Main.java:100)