We tried the jar and apk you provided as the examples. The commands we used are "java -jar jar2bpl.jar -j ../lib/log4j-1.2.16.jar -b out.bpl" and "java -jar ./dist/jar2bpl.jar -j ../jar2bpl_test/regression/android_input/snake.apk -android-jars ../jar2bpl_test/data/ -b ./test.bpl". We also tried our java files and apks. But they all throw the similar errors.
We also tried the generated bpl to all available boogie releases.
The errors are as follows.
Boogie and Dafny, 22 Oct 2012 Oct 22, 2012
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\boogie-nightly\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2.2.41003.0703, Copyright (c) 2003-2012, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(2824,30): Error: cannot refer to a global variable in this context: $heap
C:\Users\qiwang\Desktop\bpl\log4j.bpl(2825,72): Error: undeclared identifier: $obj
2 name resolution errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl
Nightly builds Nov 7, 2011
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\boogie-nightly\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2.2.41003.0703, Copyright (c) 2003-2012, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(2824,30): Error: cannot refer to a global variable in this context: $heap
C:\Users\qiwang\Desktop\bpl\log4j.bpl(2825,72): Error: undeclared identifier: $obj
2 name resolution errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie-2011-08-03 Aug 3, 2011
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\boogie-2011-08-03\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2.2.30803.0706, Copyright (c) 2003-2011, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(66565,23): error: ";" expected
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie update 2011-03-09 Mar 9, 2011
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\Boogie-2011-03-09\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2.0.0.0, Copyright (c) 2003-2010, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(66565,23): error: ";" expected
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie update 2010-07-13 Jul 13, 2010
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\Boogie-2010-07-13\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2, Copyright (c) 2003-2010, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(9084,12): syntax error: invalid UnaryExpression
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl
2010-05-16 May 16, 2010
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\Boogie-2010-05-16\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2, Copyright (c) 2003-2010, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(9084,12): syntax error: invalid UnaryExpression
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl
1.0.21125.0 Jul 15, 2009
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\Boogie-1.0.21125.0\Boogie.exe" C:\Users\qiwang\Desktop\bpl\snake.bpl
Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
C:\Users\qiwang\Desktop\bpl\snake.bpl(158,51): syntax error: invalid AtomExpression
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\snake.bpl