src/tests/gov/nasa/jpf/test/mc/basic/IdleLoopTest.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 gov.nasa.jpf.util.test.TestJPF;
  21
  22 import org.junit.Test;
  23
  24 /**
  25  * JPF test driver for the IdleFilter listener
  26  */
  27 public class IdleLoopTest extends TestJPF {
  28
  29   static final String LISTENER = "+listener=.listener.IdleFilter";
  30
  31   @Test public void testBreak () {
  32     if (verifyNoPropertyViolation(LISTENER, "+idle.action=break",
  33                                   "+log.warning=gov.nasa.jpf.listener.IdleFilter",
  34                                   "+vm.max_transition_length=MAX")) {
  35       int y = 4;
  36       int x = 0;
  37
  38       while (x != y) { // JPF should state match on the backjump
  39         x = x + 1;
  40         if (x > 3) {
  41           x = 0;
  42         }
  43       }
  44
  45       assert false : "we should never get here";
  46     }
  47   }
  48
  49   @Test public void testPrune () {
  50     if (verifyNoPropertyViolation(LISTENER, "+idle.action=prune",
  51                                   "+log.warning=gov.nasa.jpf.listener.IdleFilter",
  52                                   "+vm.max_transition_length=MAX")) {
  53       int y = 4;
  54       int x = 0;
  55
  56       int loopCount = 0;
  57
  58       while (x != y) { // JPF should prune on the backjump despite of changed 'loopCount'
  59         loopCount++;
  60         x = x + 1;
  61         if (x > 3) {
  62           x = 0;
  63         }
  64       }
  65
  66       assert false : "we should never get here";
  67     }
  68   }
  69
  70   @Test public void testJump () {
  71     if (verifyNoPropertyViolation(LISTENER, "+idle.action=jump",
  72                                   "+idle.max_backjumps=100",
  73                                   "+log.warning=gov.nasa.jpf.listener.IdleFilter",
  74                                   "+vm.max_transition_length=MAX")) {
  75
  76       for (int i=0; i<1000; i++){
  77         assert i < 500 : "JPF failed to jump past idle loop";
  78       }
  79
  80       System.out.println("Ok, jumped past loop");
  81     }
  82   }
  83
  84 }