src/tests/gov/nasa/jpf/test/mc/basic/RestorerTest.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.test.mc.basic;
  19
  20 import org.junit.Test;
  21
  22 import gov.nasa.jpf.util.test.TestJPF;
  23 import gov.nasa.jpf.vm.Verify;
  24
  25 /**
  26  * regression test for on-demand state restoration by means of
  27  * ClosedMementos
  28  */
  29 public class RestorerTest extends TestJPF {
  30
  31   static class X {
  32     int id;
  33     public void whoami() {
  34       System.out.print("I am X #");
  35       System.out.println(id);
  36     }
  37   }
  38
  39   @Test
  40   public void testRestoredInsnCount (){
  41     if (verifyNoPropertyViolation()){
  42
  43       boolean b = Verify.getBoolean();
  44       System.out.println( "--- 1. CG: " + b);
  45
  46       for (int i=1; i<=5; i++){
  47         X x = new X();
  48         x.whoami();
  49         assert x.id == i;
  50       }
  51
  52       b = Verify.getBoolean();
  53       System.out.println( "--- 2. CG: " + b);
  54
  55       X x = new X();
  56       x.whoami();
  57       assert x.id == 1; // different location, so we restart with 1
  58     }
  59   }
  60
  61   @Test
  62   public void testRestoredInsnCountBFS (){
  63     if (verifyNoPropertyViolation("+search.class=.search.heuristic.BFSHeuristic")){
  64
  65       boolean b = Verify.getBoolean();
  66       System.out.println( "--- 1. CG: " + b);
  67
  68       for (int i=1; i<=5; i++){
  69         X x = new X();
  70         x.whoami();
  71         assert x.id == i;
  72       }
  73
  74       b = Verify.getBoolean();
  75       System.out.println( "--- 2. CG: " + b);
  76
  77       X x = new X();
  78       x.whoami();
  79       assert x.id == 1; // different location, so we restart with 1
  80     }
  81   }
  82 }