KTH Demo: Proof Generation

READING CLASS AND POLICY FILES
==============================

Class file: wizard_workdir/preverifiedclasses/s3mstest/wormgame/WormScore.class
Policy file: /home/landreas/work/kth/s3ms/wormtest/policy.txt

Identified ghost  state variable: haveRead
Identified actual state variable: sf_{35}


GENERATING ASSERTIONS
=====================

*** Processing method:  ***

Initial annotations generated.
    Step 1, Updating instruction: invokespecial 9
    Step 2, Updating instruction: aload_0
Algorithm stabilized after 2 steps
Saving annotations to file.

*** Processing method: openHighScoreStore ***

Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.openRecordStore
    Relevant event clause found, annotating...done
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.toString
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Initial annotations generated.
    Step 1, Updating instruction: aload_0
    Step 2, Updating instruction: goto 57
    Step 3, Updating instruction: invokevirtual 27
    Step 4, Updating instruction: astore_0
    Step 5, Updating instruction: invokevirtual 68
    Step 6, Updating instruction: invokestatic 52
    Step 7, Updating instruction: invokevirtual 64
    Step 8, Updating instruction:  haveRead = true>
    Step 9, Updating instruction: aload_1
    Step 10, Updating instruction: iload_3
    Step 11, Updating instruction: invokevirtual 61
    Step 12, Updating instruction: aload_2
    Step 13, Updating instruction: ldc 57
    Step 14, Updating instruction: goto 22
    Step 15, Updating instruction: invokespecial 55
    Step 16, Updating instruction: putstatic 35
    Step 17, Updating instruction: dup
    Step 18, Updating instruction: iconst_1
    Step 19, Updating instruction: new 54
    Step 20, Updating instruction: getstatic 19
    Step 21, Updating instruction: astore_1
Algorithm stabilized after 21 steps
Saving annotations to file.

*** Processing method: getHighScoreName ***

Found invoke. Method: s3mstest/wormgame/WormScore.openHighScoreStore
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.getNumRecords
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.getRecord
    No relevant event clauses found.
Found invoke. Method: java/io/DataInputStream.readShort
    No relevant event clauses found.
Found invoke. Method: java/io/DataInputStream.readUTF
    No relevant event clauses found.
Found invoke. Method: java/io/DataInputStream.close
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.closeRecordStore
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.toString
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Initial annotations generated.
    Step 1, Updating instruction: aload_1
    Step 2, Updating instruction: goto 92
    Step 3, Updating instruction: invokevirtual 27
    Step 4, Updating instruction: invokevirtual 105
    Step 5, Updating instruction: invokevirtual 68
    Step 6, Updating instruction: aload_2
    Step 7, Updating instruction: invokevirtual 64
    Step 8, Updating instruction: ifle 59
    Step 9, Updating instruction: ifnull 59
    Step 10, Updating instruction: invokevirtual 102
    Step 11, Updating instruction: aload_2
    Step 12, Updating instruction: invokevirtual 78
    Step 13, Updating instruction: aload_3
    Step 14, Updating instruction: aload 4
    Step 15, Updating instruction: invokevirtual 61
    Step 16, Updating instruction: aload_2
    Step 17, Updating instruction: astore_3
    Step 18, Updating instruction: astore_1
    Step 19, Updating instruction: ldc 107
    Step 20, Updating instruction: astore_2
    Step 21, Updating instruction: invokevirtual 82
    Step 22, Updating instruction: invokevirtual 99
    Step 23, Updating instruction: invokespecial 55
    Step 24, Updating instruction: invokestatic 74
    Step 25, Updating instruction: iload_0
    Step 26, Updating instruction: aload 4
    Step 27, Updating instruction: dup
    Step 28, Updating instruction: astore_1
    Step 29, Updating instruction: aload_2
    Step 30, Updating instruction: istore 5
    Step 31, Updating instruction: new 54
    Step 32, Updating instruction: ldc 72
    Step 33, Updating instruction: ifle 59
    Step 34, Updating instruction: invokevirtual 96
    Step 35, Updating instruction: getstatic 19
    Step 36, Updating instruction: invokevirtual 78
    Step 37, Updating instruction: aload 4
    Step 38, Updating instruction: astore_2
    Step 39, Updating instruction: aload_2
    Step 40, Updating instruction: astore 4
    Step 41, Updating instruction: invokespecial 92
    Step 42, Updating instruction: invokespecial 89
    Step 43, Updating instruction: aload_3
    Step 44, Updating instruction: dup
    Step 45, Updating instruction: new 86
    Step 46, Updating instruction: dup
    Step 47, Updating instruction: new 84
    Step 48, Updating instruction: ifnull 59
    Step 49, Updating instruction: aload_3
Algorithm stabilized after 49 steps
Saving annotations to file.

*** Processing method: getHighScore ***

Found invoke. Method: s3mstest/wormgame/WormScore.openHighScoreStore
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.getNumRecords
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.getRecord
    No relevant event clauses found.
Found invoke. Method: java/io/DataInputStream.readShort
    No relevant event clauses found.
Found invoke. Method: java/io/DataInputStream.close
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.closeRecordStore
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.toString
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Initial annotations generated.
    Step 1, Updating instruction: iload_1
    Step 2, Updating instruction: goto 84
    Step 3, Updating instruction: invokevirtual 27
    Step 4, Updating instruction: invokevirtual 105
    Step 5, Updating instruction: invokevirtual 68
    Step 6, Updating instruction: aload_2
    Step 7, Updating instruction: invokevirtual 64
    Step 8, Updating instruction: ifle 51
    Step 9, Updating instruction: ifnull 51
    Step 10, Updating instruction: invokevirtual 102
    Step 11, Updating instruction: aload_2
    Step 12, Updating instruction: invokevirtual 78
    Step 13, Updating instruction: aload_3
    Step 14, Updating instruction: aload 4
    Step 15, Updating instruction: invokevirtual 61
    Step 16, Updating instruction: aload_2
    Step 17, Updating instruction: astore_3
    Step 18, Updating instruction: istore_1
    Step 19, Updating instruction: ldc 107
    Step 20, Updating instruction: astore_2
    Step 21, Updating instruction: invokevirtual 82
    Step 22, Updating instruction: invokevirtual 96
    Step 23, Updating instruction: invokespecial 55
    Step 24, Updating instruction: invokestatic 74
    Step 25, Updating instruction: iload_0
    Step 26, Updating instruction: aload 4
    Step 27, Updating instruction: dup
    Step 28, Updating instruction: istore_1
    Step 29, Updating instruction: aload_2
    Step 30, Updating instruction: astore 4
    Step 31, Updating instruction: new 54
    Step 32, Updating instruction: iconst_0
    Step 33, Updating instruction: ifle 51
    Step 34, Updating instruction: invokespecial 92
    Step 35, Updating instruction: getstatic 19
    Step 36, Updating instruction: invokevirtual 78
    Step 37, Updating instruction: invokespecial 89
    Step 38, Updating instruction: astore_2
    Step 39, Updating instruction: aload_2
    Step 40, Updating instruction: aload_3
    Step 41, Updating instruction: dup
    Step 42, Updating instruction: new 86
    Step 43, Updating instruction: dup
    Step 44, Updating instruction: new 84
    Step 45, Updating instruction: ifnull 51
    Step 46, Updating instruction: aload_3
Algorithm stabilized after 46 steps
Saving annotations to file.

*** Processing method: setHighScore ***

Found invoke. Method: java/io/DataOutputStream.writeShort
    No relevant event clauses found.
Found invoke. Method: java/io/DataOutputStream.writeUTF
    No relevant event clauses found.
Found invoke. Method: java/io/ByteArrayOutputStream.toByteArray
    No relevant event clauses found.
Found invoke. Method: java/io/DataOutputStream.close
    No relevant event clauses found.
Found invoke. Method: s3mstest/wormgame/WormScore.openHighScoreStore
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.setRecord
    No relevant event clauses found.
Found invoke. Method: javax/microedition/rms/RecordStore.closeRecordStore
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.toString
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Initial annotations generated.
    Step 1, Updating instruction: goto 95
    Step 2, Updating instruction: invokevirtual 27
    Step 3, Updating instruction: invokevirtual 105
    Step 4, Updating instruction: invokevirtual 68
    Step 5, Updating instruction: aload 6
    Step 6, Updating instruction: invokevirtual 64
    Step 7, Updating instruction: invokevirtual 134
    Step 8, Updating instruction: aload 6
    Step 9, Updating instruction: arraylength
    Step 10, Updating instruction: invokevirtual 61
    Step 11, Updating instruction: aload 5
    Step 12, Updating instruction: ldc 136
    Step 13, Updating instruction: iconst_0
    Step 14, Updating instruction: invokespecial 55
    Step 15, Updating instruction: aload 5
    Step 16, Updating instruction: dup
    Step 17, Updating instruction: iload_0
    Step 18, Updating instruction: new 54
    Step 19, Updating instruction: aload 6
    Step 20, Updating instruction: getstatic 19
    Step 21, Updating instruction: astore 6
    Step 22, Updating instruction: astore 6
    Step 23, Updating instruction: invokestatic 74
    Step 24, Updating instruction: invokevirtual 130
    Step 25, Updating instruction: aload 4
    Step 26, Updating instruction: astore 5
    Step 27, Updating instruction: invokevirtual 129
    Step 28, Updating instruction: aload_3
    Step 29, Updating instruction: invokevirtual 125
    Step 30, Updating instruction: aload_2
    Step 31, Updating instruction: aload 4
    Step 32, Updating instruction: invokevirtual 122
    Step 33, Updating instruction: i2s
    Step 34, Updating instruction: iload_1
    Step 35, Updating instruction: aload 4
    Step 36, Updating instruction: astore 4
    Step 37, Updating instruction: invokespecial 119
    Step 38, Updating instruction: aload_3
    Step 39, Updating instruction: dup
    Step 40, Updating instruction: new 116
    Step 41, Updating instruction: astore_3
    Step 42, Updating instruction: invokespecial 114
    Step 43, Updating instruction: dup
    Step 44, Updating instruction: new 113
Algorithm stabilized after 44 steps
Saving annotations to file.

Final annotations saved in WormScore_annotations.txt
Course of actions logged in annotation_output/log.tex
latex \\nonstopmode\\input annotation_output.tex && xdvi annotation_output.dvi

READING CLASS AND POLICY FILES
==============================

Class file: wizard_workdir/preverifiedclasses/s3mstest/wormgame/ScoreSender.class
Policy file: /home/landreas/work/kth/s3ms/wormtest/policy.txt

Identified ghost  state variable: haveRead
Identified actual state variable: sf_{61}


GENERATING ASSERTIONS
=====================

*** Processing method:  ***

Initial annotations generated.
    Step 1, Updating instruction: putfield 18
    Step 2, Updating instruction: iload_2
    Step 3, Updating instruction: aload_0
    Step 4, Updating instruction: putfield 16
    Step 5, Updating instruction: aload_1
    Step 6, Updating instruction: aload_0
    Step 7, Updating instruction: invokespecial 14
    Step 8, Updating instruction: aload_0
Algorithm stabilized after 8 steps
Saving annotations to file.

*** Processing method: run ***

Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.toString
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Found invoke. Method: java/lang/System.exit
    No relevant event clauses found.
Found invoke. Method: javax/microedition/io/Connector.openDataOutputStream
    Relevant event clause found, annotating...done
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.toString
    No relevant event clauses found.
Found invoke. Method: java/lang/String.getBytes
    No relevant event clauses found.
Found invoke. Method: java/io/DataOutputStream.write
    No relevant event clauses found.
Found invoke. Method: java/io/DataOutputStream.write
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Found invoke. Method: javax/microedition/midlet/MIDlet.notifyDestroyed
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.append
    No relevant event clauses found.
Found invoke. Method: java/lang/StringBuffer.toString
    No relevant event clauses found.
Found invoke. Method: java/io/PrintStream.println
    No relevant event clauses found.
Initial annotations generated.
    Step 1, Updating instruction: goto 169
    Step 2, Updating instruction: goto 169
    Step 3, Updating instruction: invokevirtual 55
    Step 4, Updating instruction: invokevirtual 94
    Step 5, Updating instruction: invokevirtual 104
    Step 6, Updating instruction: invokevirtual 49
    Step 7, Updating instruction: bipush 10
    Step 8, Updating instruction: getfield 16
    Step 9, Updating instruction: invokevirtual 109
    Step 10, Updating instruction: aload_2
    Step 11, Updating instruction: aload_0
    Step 12, Updating instruction: aload_1
    Step 13, Updating instruction: invokevirtual 92
    Step 14, Updating instruction: invokevirtual 55
    Step 15, Updating instruction: invokevirtual 40
    Step 16, Updating instruction: invokevirtual 86
    Step 17, Updating instruction: ldc 99
    Step 18, Updating instruction: ldc 106
    Step 19, Updating instruction: invokevirtual 49
    Step 20, Updating instruction: getstatic 31
    Step 21, Updating instruction: invokespecial 34
    Step 22, Updating instruction: invokevirtual 43
    Step 23, Updating instruction: invokevirtual 97
    Step 24, Updating instruction: dup
    Step 25, Updating instruction: getfield 18
    Step 26, Updating instruction: aload_1
    Step 27, Updating instruction: new 33
    Step 28, Updating instruction: aload_0
    Step 29, Updating instruction: getstatic 31
    Step 30, Updating instruction: getstatic 31
    Step 31, Updating instruction: invokevirtual 40
    Step 32, Updating instruction: astore_1
    Step 33, Updating instruction: astore_1
    Step 34, Updating instruction: ldc 80
    Step 35, Updating instruction: invokespecial 34
    Step 36, Updating instruction: dup
    Step 37, Updating instruction: new 33
    Step 38, Updating instruction: aload_2
    Step 39, Updating instruction: astore_2
    Step 40, Updating instruction: invokestatic 78
    Step 41, Updating instruction:  haveRead = true>
    Step 42, Updating instruction: aload_3
    Step 43, Updating instruction: goto 74
    Step 44, Updating instruction: invokestatic 72
    Step 45, Updating instruction: putstatic 61
    Step 46, Updating instruction: iconst_1
    Step 47, Updating instruction: if_icmpne 56
    Step 48, Updating instruction: iconst_0
    Step 49, Updating instruction: getstatic 61
    Step 50, Updating instruction: astore_3
    Step 51, Updating instruction: aload_1
    Step 52, Updating instruction: invokevirtual 55
    Step 53, Updating instruction: invokevirtual 49
    Step 54, Updating instruction: invokevirtual 40
    Step 55, Updating instruction: aload_1
    Step 56, Updating instruction: invokevirtual 40
    Step 57, Updating instruction: ldc 45
    Step 58, Updating instruction: invokevirtual 43
    Step 59, Updating instruction: getfield 18
    Step 60, Updating instruction: aload_0
    Step 61, Updating instruction: invokevirtual 40
    Step 62, Updating instruction: ldc 36
    Step 63, Updating instruction: invokespecial 34
    Step 64, Updating instruction: dup
    Step 65, Updating instruction: new 33
    Step 66, Updating instruction: getstatic 31
    Step 67, Updating instruction: astore_1
    Step 68, Updating instruction: ldc 25
Algorithm stabilized after 68 steps
Saving annotations to file.

Final annotations saved in ScoreSender_annotations.txt
Course of actions logged in annotation_output/log.tex
latex \\nonstopmode\\input annotation_output.tex && xdvi annotation_output.dvi