Installing Korat on Windows

While installing Korat make sure that you add an environment variableKORAT_CPand set it to

C:\...\korat\build;C:\...\korat\lib\alloy4viz.jar;C:\...\korat\lib\commons-cli-1.0.jar;C:\...\korat\lib\javassist.jar;C:\...\korat\lib\junit.jar

Moreover, while running Korat examples from command line use a command similar to the one below:

c:\...\korat>java -noverify -classpath %KORAT_CP% korat.Korat --class korat.examples.binarytree.BinaryTree --args 3

-noverify  is necessary otherwise you shall get the following error:

Exception in thread "main" java.lang.VerifyError: StackMapTable error: bad offset
Exception Details:
Location:
korat/examples/binarytree/BinaryTree.repOK()Z @0: aload_0
Reason:
Invalid stackmap specification.
Current Frame:
bci: @16
flags: { }
locals: { 'korat/examples/binarytree/BinaryTree' }
stack: { }
Bytecode:
0x0000000: 2a3a 0401 3a05 1904 b600 a73a 0519 05c7
0x0000010: 0019 2a3a 0403 3605 1904 b600 a936 0515
0x0000020: 059a 0005 04ac 03ac bb00 1859 b700 1a4c
0x0000030: 2b2a 3a04 013a 0519 04b6 00ab 3a05 1905
0x0000040: b900 1b02 0057 bb00 2159 b700 234d 2c2a
0x0000050: 3a04 013a 0519 04b6 00ad 3a05 1905 b600
0x0000060: 2457 a700 8b2c b600 25c0 0029 4e2d 3a04
0x0000070: 013a 0519 04b6 00b0 3a05 1905 c600 312b
0x0000080: 2d3a 0401 3a05 1904 b600 b23a 0519 05b9
0x0000090: 001b 0200 9a00 0503 ac2c 2d3a 0401 3a05
0x00000a0: 1904 b600 b43a 0519 05b6 0024 572d 3a04
0x00000b0: 013a 0519 04b6 00b7 3a05 1905 c600 312b
0x00000c0: 2d3a 0401 3a05 1904 b600 b93a 0519 05b9
0x00000d0: 001b 0200 9a00 0503 ac2c 2d3a 0401 3a05
0x00000e0: 1904 b600 bb3a 0519 05b6 0024 572c b600
0x00000f0: 3199 ff74 2bb9 0034 0100 2a3a 0403 3605
0x0000100: 1904 b600 bd36 0515 05a0 0005 04ac 03ac
0x0000110:
Stackmap Table:
same_frame(@16)
same_frame(@18)
append_frame(@57,Object[#28],Object[#33])
append_frame(@87,Object[#41])
same_frame(@96)
same_frame(@118)
chop_frame(@127,1)
same_frame(@149)

at java.lang.Class.getDeclaredMethods0(Native Method)
at java.lang.Class.privateGetDeclaredMethods(Unknown Source)
at java.lang.Class.getDeclaredMethods(Unknown Source)
at korat.testing.impl.TestCradle.getFinMethod(TestCradle.java:186)
at korat.testing.impl.TestCradle.start(TestCradle.java:176)
at korat.testing.impl.TestCradle.start(TestCradle.java:144)
at korat.Korat.main(Korat.java:188)

If you are using Eclipse add -noverify  to VM arguments of Debug/Run configuration.

Categories: Dev