KTH Demo: Proof Generation
This is the final step of the producer-side tool. It packages the inlined class files, policy and annotations in a .jad/.jar file pair. These files can be downloaded to the cell-pone or executed in the WTK emulator as shown in the next step.
Tool output:
CREATING JAR FILE... EXECUTING: /usr/lib/jvm/java-1.5.0-sun/bin/jar cvfm ../WormTest.jar Manifest.mf ScoreSender_annotations.txt WormScore_annotations.txt SecState.class s3mstest EXECUTION WD: wizard_workdir/preverifiedclasses added manifest adding: ScoreSender_annotations.txt(in = 4187) (out= 183)(deflated 95%) adding: WormScore_annotations.txt(in = 7193) (out= 248)(deflated 96%) adding: SecState.class(in = 148) (out= 131)(deflated 11%) adding: s3mstest/(in = 0) (out= 0)(stored 0%) adding: s3mstest/wormgame/(in = 0) (out= 0)(stored 0%) adding: s3mstest/wormgame/WormLink.class(in = 2392) (out= 1212)(deflated 49%) adding: s3mstest/wormgame/Worm.class(in = 4191) (out= 2233)(deflated 46%) adding: s3mstest/wormgame/ScoreSender.class(in = 1880) (out= 1050)(deflated 44%) adding: s3mstest/wormgame/WormPit.class(in = 8659) (out= 4497)(deflated 48%) adding: s3mstest/wormgame/WormScore.class(in = 2615) (out= 1414)(deflated 45%) adding: s3mstest/wormgame/WormMain.class(in = 4389) (out= 2156)(deflated 50%) adding: s3mstest/wormgame/WormFood.class(in = 1228) (out= 757)(deflated 38%) adding: s3mstest/wormgame/WormException.class(in = 244) (out= 193)(deflated 20%) EXECUTION SUCCESSFUL. DONE
Download WormTest.jad and WormTest.jar.
To execute the worm game in the WTK-emulator you invoke it in the following way
wtk2.5.1/bin/emulator -Xdescriptor WormTest.jad