1 @LATTICE("testL<testM,testM<testH")
2 @METHODDEFAULT("methodL<methodH,methodH<methodT,THISLOC=methodT")
5 @LOC("testH") int fieldH;
6 @LOC("testM") int fieldM;
7 @LOC("testL") int fieldL;
8 @LOC("testM") Foo fooM;
10 public static void main (@LOC("methodH") String args[]){
11 @LOC("methodH") test t=new test();
16 @LOC("methodH") int localH; // LOC=[local.methodH]
17 fooM=new Foo(); // LOC=[local.methodT, field.testM]
20 // here, callee expects that arg1 is higher than arg2
21 // so caller should respects callee's constraints
22 fooM.doSomethingArgs(fieldH,fieldM);
30 @LOC("methodH,testL") int localVarL;
31 // value flows from the field [local.methodH,field.testH]
32 // to the local variable [local.methodL]
37 @LOC("methodT,testL")int localVar=fooM.a+fooM.b;
38 // GLB(fooM.a,fooM.b)=LOC[methodT,testM,FB]
39 // LOC[lovalVar]=[methodT,testL] < GLB(fooM.a,fooM.b)
42 // creating composite location by object references
44 @LOC("methodT,testM,FC,BB") int localVar=fooM.bar.a;
45 //LOC(fooM.bar.a)=[methodT,testM,FC,BA]
46 //localVar can flow into lower location of fooM.bar.a
47 fooM.bar.c=localVar; //[methodT,testM,FC,BB] < [methodT,testM,FC,BA]
50 // method has its own local variable lattice
51 @LATTICE("mL<mH,THISLOC=mH")
52 public void doOwnLattice(){
59 @LATTICE("mL<mH,THISLOC=mH")
60 public void doDelta(){
61 @LOC("DELTA(mH,testH)") int varDelta;
62 // LOC(varDelta) is slightly lower than [mH, testH]
64 @LOC("DELTA(DELTA(mH,testH))") int varDeltax2;
65 // applying double delta to [mH,testH]
67 varDelta=fieldH; // [mH,testH] -> DELTA[mh,testH]
68 varDeltax2=varDelta; //DELTA[mh,testH] -> DELTA[DELTA[mh,testH]]
70 fieldM=varDeltax2; // DELTA[DELTA[mh,testH]] -> [mH,testM]
73 @LATTICE("mL<mSpin,mSpin<mH,mSpin*")
74 public void doSpinLoc(){
75 // if loc is defined with the suffix *,
76 //value can be flowing around the same location
79 @LOC("mSpin") int varSpin;
84 // value can be flowing back to the varSpin
85 // since 'varSpin' is location allowing value to move within
86 // the same abstract location
92 @LATTICE("mL<mH,THISLOC=mL")
93 public void doSpinField(){
94 //only last element of the composite location can be the spinning loc
99 @LOC("mH") Bar localBar=new Bar();
101 localBar.b2=localBar.b1;
102 // LOC(localBar.b1)=[mH,BB]
103 // LOC(localBar.b2)=[mH,BB]
104 // b1 and b2 share the same abstract loc BB
105 // howerver, location BB allows values to be moving within itself
107 localBar.b1++; // value can be moving among the same location
113 @LATTICE("FC<FB,FB<FA")
114 @METHODDEFAULT("fm_L<fm_M1,fm_L<fm_M2,fm_M1<fm_H,fm_M2<fm_H,THISLOC=fm_H")
125 public void doSomething(){
126 b=a; // value flows from [fm_H,FA] to [fm_H,FB]
129 // callee has a constraint that arg1 is higher than arg2
130 public int doSomethingArgs(@LOC("fm_H")int argH,
131 @LOC("fm_M1")int argL){
136 public int doSomethingRtn(){
137 return a+b; // going to return LOC[local.t,field.FB]
142 @LATTICE("BC<BB,BB<BA,BB*")
143 @METHODDEFAULT("BARMD_L<BARMD_H,THISLOC=BARMD_H")