system .|Deadlock|.
{
record (|java.lang.ArithmeticException|) extends (|java.lang.RuntimeException|) {}
function {|java.lang.ArithmeticException.()|}((|java.lang.ArithmeticException|) [|r0|])
{
loc loc1: live {}
do
{
}
return;
}
function {|java.lang.ArithmeticException.(java.lang.String)|}((|java.lang.ArithmeticException|) [|r0|], (|java.lang.String|) [|r1|])
{
loc loc2: live {}
do
{
}
return;
}
record (|java.lang.RuntimeException|) extends (|java.lang.Exception|) {}
function {|java.lang.RuntimeException.()|}((|java.lang.RuntimeException|) [|r0|])
{
loc loc1: live {}
invoke {|java.lang.Exception.()|}([|r0|]) goto loc2;
loc loc2: live {}
do
{
}
return;
}
function {|java.lang.RuntimeException.(java.lang.String)|}((|java.lang.RuntimeException|) [|r0|], (|java.lang.String|) [|r1|])
{
loc loc2: live {}
do
{
}
return;
}
record (|java.lang.String|) extends (|java.lang.Object|) {}
record (|java.lang.Exception|) extends (|java.lang.Throwable|) {}
function {|java.lang.Exception.()|}((|java.lang.Exception|) [|r0|])
{
loc loc1: live {}
invoke {|java.lang.Throwable.()|}([|r0|]) goto loc2;
loc loc2: live {}
do
{
}
return;
}
function {|java.lang.Exception.(java.lang.String)|}((|java.lang.Exception|) [|r0|], (|java.lang.String|) [|r1|])
{
loc loc2: live {}
do
{
}
return;
}
record (|java.lang.Throwable|) extends (|java.lang.Object|) {}
function {|java.lang.Throwable.()|}((|java.lang.Throwable|) [|r0|])
{
loc loc1: live {}
do
{
}
return;
}
function {|java.lang.Throwable.(java.lang.String)|}((|java.lang.Throwable|) [|r0|], (|java.lang.String|) [|r1|])
{
loc loc2: live {}
do
{
}
return;
}
top throwable record (|java.lang.Object|) { lock objectLock; }
function {|java.lang.Object.()|}((|java.lang.Object|) [|r0|])
{
loc loc1: live {}
do
{
}
return;
}
record (|java.lang.IllegalArgumentException|) extends (|java.lang.RuntimeException|) {}
function {|java.lang.IllegalArgumentException.()|}((|java.lang.IllegalArgumentException|) [|r0|])
{
loc loc1: live {}
do
{
}
return;
}
function {|java.lang.IllegalArgumentException.(java.lang.String)|}((|java.lang.IllegalArgumentException|) [|r0|], (|java.lang.String|) [|r1|])
{
loc loc2: live {}
invoke {|java.lang.RuntimeException.()|}([|r0|]) goto loc3;
loc loc3: live {}
do
{
}
return;
}
record (|java.lang.NumberFormatException|) extends (|java.lang.IllegalArgumentException|) {}
function {|java.lang.NumberFormatException.()|}((|java.lang.NumberFormatException|) [|r0|])
{
loc loc1: live {}
do
{
}
return;
}
function {|java.lang.NumberFormatException.(java.lang.String)|}((|java.lang.NumberFormatException|) [|r0|], (|java.lang.String|) [|r1|])
{
loc loc2: live {}
do
{
}
return;
}
record (|java.lang.Thread|) extends (|java.lang.Object|) { boolean /|java.lang.Thread.started|\;tid threadID;boolean isThreadInitialized; }
function {|java.lang.Thread.()|}((|java.lang.Thread|) [|r0|])
{
loc loc1: live {}
invoke {|java.lang.Object.()|}([|r0|]) goto loc2;
loc loc2: live {}
do
{
[|r0|]./|java.lang.Thread.started|\ := false;
}
goto loc3;
loc loc3: live {}
do
{
}
return;
}
function {|java.lang.Thread.start()|}((|java.lang.Thread|) [|r0|])
{
boolean [|$z0|];
(|java.lang.IllegalThreadStateException|) [|$r1|];
(|java.lang.Throwable|) throwLocal;
loc sync: live { [|r0|], [|$z0|] }
when [|r0|] == null || lockAvailable([|r0|].objectLock) do
{
lock([|r0|].objectLock);
}
goto loc1;
loc loc1: live { [|r0|], [|$z0|] }
do
{
[|$z0|] := [|r0|]./|java.lang.Thread.started|\;
}
goto loc2;
loc loc2: live { [|r0|] }
when !(([|$z0|])) do
{
}
goto loc6;
when !((!(([|$z0|])))) do
{
}
goto loc3;
loc loc3: live { [|r0|], [|$r1|] }
when !((BogorJava.isInitialized(isi, "(|java.lang.IllegalThreadStateException|)"))) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|java.lang.IllegalThreadStateException|)")) goto loc3;
when BogorJava.isInitialized(isi, "(|java.lang.IllegalThreadStateException|)") do invisible
{
[|$r1|] := new (|java.lang.IllegalThreadStateException|);
}
goto loc4;
loc loc4: live { [|r0|], [|$r1|], [|$r1|] }
when !((BogorJava.isInitialized(isi, "(|java.lang.String|)"))) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|java.lang.String|)")) goto loc4;
when BogorJava.isInitialized(isi, "(|java.lang.String|)") invoke {|java.lang.IllegalThreadStateException.(java.lang.String)|}([|$r1|], BogorJava.toString("This thread has already been started.")) goto loc5;
loc loc5: live { [|r0|] }
do
{
throw [|$r1|];
}
goto loc5;
loc loc6: live { [|r0|] }
do
{
[|r0|]./|java.lang.Thread.started|\ := true;
}
goto loc7;
loc loc7: live { [|r0|] }
do
{
[|r0|].threadID := start (|java.lang.Thread|) ([|r0|]);
}
goto loc8;
loc loc8: live { [|r0|] }
do
{
}
goto unsync;
loc unsync: live {}
do
{
unlock([|r0|].objectLock);
}
return;
loc unsyncEx: live { throwLocal }
do
{
unlock([|r0|].objectLock);
}
goto throwEx;
loc throwEx: live {}
do
{
throw throwLocal;
}
goto throwEx;
catch (|java.lang.Throwable|) throwLocal except at sync, unsync, unsyncEx, throwEx goto unsyncEx;
}
function {|java.lang.Thread.run()|}((|java.lang.Thread|) [|r0|])
{
loc loc1: live {}
do
{
}
return;
}
record (|java.lang.IllegalThreadStateException|) extends (|java.lang.IllegalArgumentException|) {}
function {|java.lang.IllegalThreadStateException.()|}((|java.lang.IllegalThreadStateException|) [|r0|])
{
loc loc1: live {}
do
{
}
return;
}
function {|java.lang.IllegalThreadStateException.(java.lang.String)|}((|java.lang.IllegalThreadStateException|) [|r0|], (|java.lang.String|) [|r1|])
{
loc loc2: live {}
invoke {|java.lang.IllegalArgumentException.(java.lang.String)|}([|r0|], null) goto loc3;
loc loc3: live {}
do
{
}
return;
}
(|Lock|) /|Deadlock.lock1|\;
(|Lock|) /|Deadlock.lock2|\;
int /|Deadlock.state|\;
record (|Deadlock|) extends (|java.lang.Object|) {}
virtual +|java.lang.Thread.start()|+ { (|java.lang.Thread|) -> {|java.lang.Thread.start()|} (|Process1|) -> {|java.lang.Thread.start()|} (|Process2|) -> {|java.lang.Thread.start()|} }
function {|Deadlock.main(java.lang.String[])|}((|java.lang.String|)[] [|r0|])
{
(|Lock|) [|$r1|];
(|Process1|) [|r2|];
(|Process2|) [|r3|];
(|Lock|) [|$r4|];
(|Process1|) [|$r5|];
(|Process2|) [|$r6|];
loc loc1: live { [|$r1|] }
when !(BogorJava.isInitialized(isi, "(|Lock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Lock|)")) goto loc1;
when BogorJava.isInitialized(isi, "(|Lock|)") do
{
[|$r1|] := BogorJava.nwR<(|Lock|)>();
}
goto loc2;
loc loc2: live { [|$r1|] }
invoke {|Lock.()|}([|$r1|]) goto loc3;
loc loc3: live {}
do
{
/|Deadlock.lock1|\ := [|$r1|];
}
goto loc4;
loc loc4: live { [|$r4|] }
when !(BogorJava.isInitialized(isi, "(|Lock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Lock|)")) goto loc4;
when BogorJava.isInitialized(isi, "(|Lock|)") do
{
[|$r4|] := BogorJava.nwR<(|Lock|)>();
}
goto loc5;
loc loc5: live { [|$r4|] }
invoke {|Lock.()|}([|$r4|]) goto loc6;
loc loc6: live {}
do
{
/|Deadlock.lock2|\ := [|$r4|];
}
goto loc7;
loc loc7: live { [|$r5|] }
when !(BogorJava.isInitialized(isi, "(|Process1|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Process1|)")) goto loc7;
when BogorJava.isInitialized(isi, "(|Process1|)") do
{
[|$r5|] := BogorJava.nwR<(|Process1|)>();
}
goto loc8;
loc loc8: live { [|$r5|] }
invoke {|Process1.()|}([|$r5|]) goto loc9;
loc loc9: live { [|r2|] }
do
{
[|r2|] := [|$r5|];
}
goto loc10;
loc loc10: live { [|r2|], [|$r6|], [|r2|] }
when !(BogorJava.isInitialized(isi, "(|Process2|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Process2|)")) goto loc10;
when BogorJava.isInitialized(isi, "(|Process2|)") do
{
[|$r6|] := BogorJava.nwR<(|Process2|)>();
}
goto loc11;
loc loc11: live { [|r2|], [|$r6|] }
invoke {|Process2.()|}([|$r6|]) goto loc12;
loc loc12: live { [|r3|], [|r2|] }
do
{
[|r3|] := [|$r6|];
}
goto loc13;
loc loc13: live { [|r3|] }
invoke virtual +|java.lang.Thread.start()|+([|r2|]) goto loc14;
loc loc14: live {}
invoke virtual +|java.lang.Thread.start()|+([|r3|]) goto loc15;
loc loc15: live {}
do
{
}
return;
}
record (|Lock|) extends (|java.lang.Object|) {}
function {|Lock.()|}((|Lock|) [|r0|])
{
loc loc1: live {}
invoke {|java.lang.Object.()|}([|r0|]) goto loc2;
loc loc2: live {}
do
{
}
return;
}
record (|Process1|) extends (|java.lang.Thread|) {}
function {|Process1.()|}((|Process1|) [|r0|])
{
loc loc1: live {}
invoke {|java.lang.Thread.()|}([|r0|]) goto loc2;
loc loc2: live {}
do
{
}
return;
}
function {|Process1.run()|}((|Process1|) [|r0|])
{
int [|$i0|];
(|Lock|) [|r1|];
(|Lock|) [|r2|];
(|java.lang.Throwable|) [|r3|];
(|java.lang.Throwable|) [|r4|];
int [|$i1|];
(|Lock|) [|$r5|];
(|Lock|) [|$r6|];
int [|$i2|];
int [|$i3|];
(|java.lang.Throwable|) [|$r7|];
(|java.lang.Throwable|) [|$r8|];
loc loc1: live { [|$i0|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc1;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
[|$i0|] := /|Deadlock.state|\;
}
goto loc2;
loc loc2: live { [|$i1|] }
do
{
[|$i1|] := [|$i0|] + 1;
}
goto loc3;
loc loc3: live { [|$i1|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc3;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
/|Deadlock.state|\ := [|$i1|];
}
goto loc4;
loc loc4: live { [|$r5|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc4;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
[|$r5|] := /|Deadlock.lock1|\;
}
goto loc5;
loc loc5: live { [|$r5|], [|r1|] }
do
{
[|r1|] := [|$r5|];
}
goto loc6;
loc loc6: live { [|r1|] }
when [|$r5|] == null || lockAvailable([|$r5|].objectLock) do
{
lock([|$r5|].objectLock);
}
goto loc7;
loc loc7: live { [|r1|], [|$r6|], [|r1|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc7;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
[|$r6|] := /|Deadlock.lock2|\;
}
goto loc8;
loc loc8: live { [|r2|], [|r1|], [|$r6|] }
do
{
[|r2|] := [|$r6|];
}
goto loc9;
loc loc9: live { [|r2|], [|r1|] }
when [|$r6|] == null || lockAvailable([|$r6|].objectLock) do
{
lock([|$r6|].objectLock);
}
goto loc10;
loc loc10: live { [|r2|], [|r1|], [|$i2|], [|r2|], [|r1|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc10;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
[|$i2|] := /|Deadlock.state|\;
}
goto loc11;
loc loc11: live { [|r2|], [|$i3|], [|r1|] }
do
{
[|$i3|] := [|$i2|] + 1;
}
goto loc12;
loc loc12: live { [|r2|], [|r1|], [|r2|], [|$i3|], [|r1|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc12;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
/|Deadlock.state|\ := [|$i3|];
}
goto loc13;
loc loc13: live { [|r2|], [|r1|] }
when [|r2|] == null || hasLock([|r2|].objectLock) do
{
unlock([|r2|].objectLock);
}
goto loc14;
loc loc14: live { [|r1|] }
do
{
}
goto loc19;
loc loc16: live { [|r2|], [|r1|], [|r3|] }
do
{
[|r3|] := [|$r7|];
}
goto loc17;
loc loc17: live { [|r2|], [|r1|], [|r3|] }
when [|r2|] == null || hasLock([|r2|].objectLock) do
{
unlock([|r2|].objectLock);
}
goto loc18;
loc loc18: live { [|r1|] }
do
{
throw [|r3|];
}
goto loc18;
loc loc19: live { [|r1|] }
when [|r1|] == null || hasLock([|r1|].objectLock) do
{
unlock([|r1|].objectLock);
}
goto loc20;
loc loc20: live {}
do
{
}
goto loc25;
loc loc22: live { [|r1|], [|r4|] }
do
{
[|r4|] := [|$r8|];
}
goto loc23;
loc loc23: live { [|r1|], [|r4|] }
when [|r1|] == null || hasLock([|r1|].objectLock) do
{
unlock([|r1|].objectLock);
}
goto loc24;
loc loc24: live {}
do
{
throw [|r4|];
}
goto loc24;
loc loc25: live {}
do
{
}
return;
catch (|java.lang.Throwable|) [|$r7|] at loc10, loc11, loc12, loc13 goto loc16;
catch (|java.lang.Throwable|) [|$r7|] at loc16, loc17 goto loc16;
catch (|java.lang.Throwable|) [|$r8|] at loc7, loc8, loc9, loc10, loc11, loc12, loc13, loc14, loc16, loc17, loc18, loc19 goto loc22;
catch (|java.lang.Throwable|) [|$r8|] at loc22, loc23 goto loc22;
}
record (|Process2|) extends (|java.lang.Thread|) {}
function {|Process2.()|}((|Process2|) [|r0|])
{
loc loc1: live {}
invoke {|java.lang.Thread.()|}([|r0|]) goto loc2;
loc loc2: live {}
do
{
}
return;
}
function {|Process2.run()|}((|Process2|) [|r0|])
{
int [|$i0|];
(|Lock|) [|r1|];
(|Lock|) [|r2|];
(|java.lang.Throwable|) [|r3|];
(|java.lang.Throwable|) [|r4|];
int [|$i1|];
(|Lock|) [|$r5|];
(|Lock|) [|$r6|];
int [|$i2|];
int [|$i3|];
(|java.lang.Throwable|) [|$r7|];
(|java.lang.Throwable|) [|$r8|];
loc loc1: live { [|$i0|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc1;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
[|$i0|] := /|Deadlock.state|\;
}
goto loc2;
loc loc2: live { [|$i1|] }
do
{
[|$i1|] := [|$i0|] + 1;
}
goto loc3;
loc loc3: live { [|$i1|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc3;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
/|Deadlock.state|\ := [|$i1|];
}
goto loc4;
loc loc4: live { [|$r5|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc4;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
[|$r5|] := /|Deadlock.lock2|\;
}
goto loc5;
loc loc5: live { [|$r5|], [|r1|] }
do
{
[|r1|] := [|$r5|];
}
goto loc6;
loc loc6: live { [|r1|] }
when [|$r5|] == null || lockAvailable([|$r5|].objectLock) do
{
lock([|$r5|].objectLock);
}
goto loc7;
loc loc7: live { [|r1|], [|$r6|], [|r1|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc7;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
[|$r6|] := /|Deadlock.lock1|\;
}
goto loc8;
loc loc8: live { [|r2|], [|r1|], [|$r6|] }
do
{
[|r2|] := [|$r6|];
}
goto loc9;
loc loc9: live { [|r2|], [|r1|] }
when [|$r6|] == null || lockAvailable([|$r6|].objectLock) do
{
lock([|$r6|].objectLock);
}
goto loc10;
loc loc10: live { [|r2|], [|r1|], [|$i2|], [|r2|], [|r1|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc10;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
[|$i2|] := /|Deadlock.state|\;
}
goto loc11;
loc loc11: live { [|r2|], [|$i3|], [|r1|] }
do
{
[|$i3|] := [|$i2|] + 1;
}
goto loc12;
loc loc12: live { [|r2|], [|r1|], [|r2|], [|$i3|], [|r1|] }
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc12;
when BogorJava.isInitialized(isi, "(|Deadlock|)") do
{
/|Deadlock.state|\ := [|$i3|];
}
goto loc13;
loc loc13: live { [|r2|], [|r1|] }
when [|r2|] == null || hasLock([|r2|].objectLock) do
{
unlock([|r2|].objectLock);
}
goto loc14;
loc loc14: live { [|r1|] }
do
{
}
goto loc19;
loc loc16: live { [|r2|], [|r1|], [|r3|] }
do
{
[|r3|] := [|$r7|];
}
goto loc17;
loc loc17: live { [|r2|], [|r1|], [|r3|] }
when [|r2|] == null || hasLock([|r2|].objectLock) do
{
unlock([|r2|].objectLock);
}
goto loc18;
loc loc18: live { [|r1|] }
do
{
throw [|r3|];
}
goto loc18;
loc loc19: live { [|r1|] }
when [|r1|] == null || hasLock([|r1|].objectLock) do
{
unlock([|r1|].objectLock);
}
goto loc20;
loc loc20: live {}
do
{
}
goto loc25;
loc loc22: live { [|r1|], [|r4|] }
do
{
[|r4|] := [|$r8|];
}
goto loc23;
loc loc23: live { [|r1|], [|r4|] }
when [|r1|] == null || hasLock([|r1|].objectLock) do
{
unlock([|r1|].objectLock);
}
goto loc24;
loc loc24: live {}
do
{
throw [|r4|];
}
goto loc24;
loc loc25: live {}
do
{
}
return;
catch (|java.lang.Throwable|) [|$r7|] at loc10, loc11, loc12, loc13 goto loc16;
catch (|java.lang.Throwable|) [|$r7|] at loc16, loc17 goto loc16;
catch (|java.lang.Throwable|) [|$r8|] at loc7, loc8, loc9, loc10, loc11, loc12, loc13, loc14, loc16, loc17, loc18, loc19 goto loc22;
catch (|java.lang.Throwable|) [|$r8|] at loc22, loc23 goto loc22;
}
extension JavaLangThread for edu.ksu.cis.projects.bogor.module.bandera.javalib.JavaLangThread
{
expdef tid getThreadIdForRecord ((|java.lang.Thread|) t);
expdef (|java.lang.Thread|) getThreadRecordForId (tid id);
actiondef associateThreadIdAndRecord (tid id, (|java.lang.Thread|) r);
}
extension JavaLangInteger for edu.ksu.cis.projects.bogor.module.bandera.javalib.JavaLangInteger
{
expdef int parseInt (string, int);
}
extension JavaLangFloat for edu.ksu.cis.projects.bogor.module.bandera.javalib.JavaLangFloat
{
expdef float parseFloat (string);
expdef int floatToIntBits (float);
expdef int floatToRawIntBits (float);
expdef float intBitsToFloat (int);
}
extension JavaLangDouble for edu.ksu.cis.projects.bogor.module.bandera.javalib.JavaLangDouble
{
expdef double parseDouble (string);
expdef long doubleToLongBits (double);
expdef long doubleToRawLongBits (double);
expdef double longBitsToDouble (long);
}
extension JavaLangMath for edu.ksu.cis.projects.bogor.module.bandera.javalib.JavaLangMath
{
expdef double acos (double);
expdef double asin (double);
expdef double atan (double);
expdef double atan2 (double, double);
expdef double cos (double);
expdef double exp (double);
expdef double log (double);
expdef double pow (double, double);
expdef double rint (double);
expdef double sin (double);
expdef double sqrt (double);
expdef double tan (double);
}
extension Choose for edu.ksu.cis.projects.bogor.module.ext.choice.ChooseModule
{
expdef boolean chooseBool ();
expdef int chooseInt (int, int);
expdef (|java.lang.Object|) chooseJavaObject (boolean, (|java.lang.String|));
expdef (|java.lang.Object|) chooseJavaReachable ((|java.lang.Object|), boolean, (|java.lang.String|));
}
thread (|java.lang.Thread|)((|java.lang.Thread|) [|this|])
{
loc loc0: live {}
invoke virtual +|java.lang.Runnable.run()|+([|this|]) return;
}
boolean[] isi;
int wrap (-32768, 32767) charTypeField;
int wrap (-32768, 32767)[] charArrayTypeField;
int wrap (-128, 127) byteTypeField;
int wrap (-128, 127)[] byteArrayTypeField;
extension BogorJava for edu.ksu.cis.projects.bogor.ext.java.BogorJavaModule
{
expdef (|java.lang.String|) toString (string);
expdef string fromString ((|java.lang.String|));
expdef StaticInitializers[] getStaticInitializers (boolean[], string, string...);
expdef boolean isInitialized (boolean[], string, string...);
expdef boolean isInitializedByEnumValue (boolean[], StaticInitializers);
expdef int getEnumConstantCount <'a$enum>();
expdef int enumToZeroIndexedInt <'a$enum>('a$enum);
expdef 'a$enum zeroIndexedIntToEnum <'a$enum>(int);
expdef 'a$record nwR <'a$record>();
expdef 'a$array nwA <'a$array>(int...);
expdef int wrap (0, 255) lcmp (long, long);
expdef int wrap (0, 255) dcmpg (double, double);
expdef int wrap (0, 255) dcmpl (double, double);
expdef int wrap (0, 255) fcmpg (float, float);
expdef int wrap (0, 255) fcmpl (float, float);
expdef float fpInfinity ();
expdef float fnInfinity ();
expdef float fNaN ();
expdef double dpInfinity ();
expdef double dnInfinity ();
expdef double dNaN ();
}
enum StaticInitializers { dummyStaticInitializer }
virtual +|staticInitializer|+ on StaticInitializers { dummyStaticInitializer -> dummyStaticInitializer }
function dummyStaticInitializer(StaticInitializers si)
{
loc loc0: live {}
do
{
}
return;
}
function runStaticInitializers(StaticInitializers[] sil)
{
StaticInitializers temp;
int offset := 0;
loc loc0:
when offset >= sil.length do
{
}
return;
when offset < sil.length do
{
temp := sil[offset];
assert isi[BogorJava.enumToZeroIndexedInt(temp)] != true;
isi[BogorJava.enumToZeroIndexedInt(temp)] := true;
offset := offset + 1;
}
goto loc1;
loc loc1:
invoke virtual +|staticInitializer|+(temp) goto loc0;
}
active main thread MAIN()
{
loc loc0: live {}
do invisible
{
isi := new boolean[BogorJava.getEnumConstantCount()];
}
goto loc1;
loc loc1: live {}
when !(BogorJava.isInitialized(isi, "(|Deadlock|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|Deadlock|)")) goto loc1;
when BogorJava.isInitialized(isi, "(|Deadlock|)") invoke {|Deadlock.main(java.lang.String[])|}((null)) return;
}
virtual +|java.lang.Runnable.run()|+ { (|java.lang.Thread|) -> {|java.lang.Thread.run()|} (|Process1|) -> {|Process1.run()|} (|Process2|) -> {|Process2.run()|} }
}
|
