Robust/src/Tests/OwnershipAnalysisTest/testMethodContexts/testMethodContexts.java

   1 public class Foo { flag f; Foo x; public Foo(){} }
   2
   3 public class Plane {
   4   public Plane(){}
   5
   6   public void fly( Foo p0, Foo p1 ) {
   7     p0.x = new Foo(){f};
   8   }
   9 }
  10
  11 public class SpitFire extends Plane {
  12   public SpitFire(){}
  13
  14   public void fly( Foo p0, Foo p1 ) {
  15     p1.x = new Foo(){f};
  16   }
  17 }
  18
  19 public class Jet extends Plane {
  20   public Jet(){}
  21
  22   public void fly( Foo p0, Foo p1 ) {
  23     Foo jet = new Foo(){f};
  24     jet.x = p0;
  25   }
  26 }
  27
  28 public class F14 extends Jet {
  29   public F14(){}
  30
  31   public void fly( Foo p0, Foo p1 ) {
  32     Foo f14 = new Foo(){f};
  33     f14.x = p1;
  34   }
  35 }
  36
  37 task Startup( StartupObject s{ initialstate } ) {
  38
  39   Foo a0 = new Foo(){f};
  40   Foo a1 = new Foo(){f};
  41
  42   Plane p;
  43
  44   if( false ) {
  45     p = new Plane();
  46   } else if( false ) {
  47     p = new SpitFire();
  48   } else if( false ) {
  49     p = new Jet();
  50   } else {
  51     p = new F14();
  52   }
  53
  54   p.fly( a0, a1 );
  55
  56   taskexit( s{ !initialstate } );
  57 }
  58
  59
  60 task SomeOtherTask( Foo foo{f} ) {
  61
  62   Foo a0 = new Foo(){f};
  63   Foo a1 = new Foo(){f};
  64
  65   Plane p;
  66
  67   if( false ) {
  68     p = new Plane();
  69   } else if( false ) {
  70     p = new SpitFire();
  71   } else if( false ) {
  72     p = new Jet();
  73   } else {
  74     p = new F14();
  75   }
  76
  77   a0.x = a1;
  78   p.fly( a0, a1 );
  79
  80   taskexit( foo{!f} );
  81 }