Robust/src/Tests/ssJava/written/test.java

   1 @LATTICE("L<M,M<H")
   2 @METHODDEFAULT("L<M,M<H,H<C,THISLOC=M,C*,H*")
   3 public class test{
   4
   5     @LOC("H") int fieldH;
   6     @LOC("M") int fieldM;
   7     @LOC("L") int fieldL;
   8
   9     public static void main(@LOC("H") String args[]){
  10         @LOC("M") test test=new test();
  11
  12         @LOC("M") int localM;
  13         @LOC("L") int localL;
  14         @LOC("M") Foo foo=new Foo();
  15         @LOC("C") int count=0;
  16         SSJAVA:
  17         while(count<50){
  18             count++;
  19             test.doit();
  20             if(true){
  21                 // read followed by write: problem!
  22                 localL=test.fieldH;
  23                 //test.fieldH=50;
  24             }
  25         }
  26     }
  27
  28     public void doit(){
  29         @LOC("L") int local=fieldH;
  30         fieldH=50;
  31     }
  32
  33 }
  34
  35 @LATTICE("L<M,M<H")
  36 @METHODDEFAULT("L<M,M<H,H<C,THISLOC=M,C*,H*")
  37 class test2 extends test{
  38
  39     public void doit(){
  40         if(true){
  41             fieldH=50;
  42         }else{
  43             fieldL=50;
  44         }
  45     }
  46
  47 }
  48
  49 @LATTICE("L<M,M<H")
  50 class Foo{
  51     @LOC("H") int a;
  52 }