src/tests/gov/nasa/jpf/test/mc/data/TypedObjectChoiceTest.java

   1 /*
   2  * Copyright (C) 2015, 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.data;
  19
  20 import gov.nasa.jpf.util.test.TestJPF;
  21 import gov.nasa.jpf.vm.Verify;
  22 import org.junit.Test;
  23
  24 /**
  25  * regression test for TypedObjectChoice CGs
  26  */
  27 public class TypedObjectChoiceTest extends TestJPF {
  28
  29   static class A {
  30     int id;
  31     A (int i){
  32       id = i;
  33     }
  34     public String toString(){ return String.format("A(%d)", id); }
  35   }
  36
  37   @Test
  38   public void testNoCG (){
  39     if (verifyNoPropertyViolation("+mycg.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
  40             "+mycg.include_null=false",
  41             "+mycg.type=" + getClass().getName() + "$A")){
  42       Object o = Verify.getObject("mycg");
  43       System.out.print("got object: ");
  44       System.out.println(o);
  45
  46       assertTrue( o == null);
  47     }
  48   }
  49
  50   @Test
  51   public void testNoObject (){
  52     if (verifyNoPropertyViolation("+mycg.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
  53                                   "+mycg.include_null=true",
  54                                   "+mycg.type=" + getClass().getName() + "$A")){
  55       Object o = Verify.getObject("mycg");
  56       System.out.print("got object: ");
  57       System.out.println(o);
  58
  59       assertTrue( o == null);
  60     }
  61   }
  62
  63   @Test
  64   public void testObject (){
  65     if (verifyNoPropertyViolation("+mycg.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
  66             "+mycg.include_null=false",
  67             "+mycg.type=" + getClass().getName() + "$A")) {
  68       A a = new A(42);
  69
  70       Object o = Verify.getObject("mycg");
  71       System.out.print("got object: ");
  72       System.out.println(o);
  73
  74       assertTrue(o instanceof A);
  75       a = (A) o;
  76       assertTrue(a.id == 42);
  77     }
  78   }
  79
  80   @Test
  81   public void testMultipleObjects(){
  82     if (verifyNoPropertyViolation("+mycg.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
  83             "+mycg.include_null=false",
  84             "+mycg.type=" + getClass().getName() + "$A")) {
  85       A a1 = new A(1);
  86       A a2 = new A(2);
  87
  88       Object o = Verify.getObject("mycg");
  89       System.out.print("got object: ");
  90       System.out.println(o);
  91
  92       assertTrue(o instanceof A);
  93       A a = (A) o;
  94       Verify.setBitInBitSet(0, a.id, true);
  95       Verify.incrementCounter(0);
  96     }
  97
  98     if (!isJPFRun()){
  99       assertTrue( Verify.getCounter(0) == 2);
 100       assertTrue( Verify.getBitInBitSet(0, 1));
 101       assertTrue( Verify.getBitInBitSet(0, 2));
 102     }
 103   }
 104
 105 }