src/tests/gov/nasa/jpf/test/basic/InstructionFactoryTest.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
  19 package gov.nasa.jpf.test.basic;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.util.test.TestJPF;
  23 import gov.nasa.jpf.vm.Instruction;
  24 import gov.nasa.jpf.vm.StackFrame;
  25 import gov.nasa.jpf.vm.ThreadInfo;
  26
  27 import org.junit.Test;
  28
  29 /**
  30  * basic test for InstructionFactories
  31  */
  32 public class InstructionFactoryTest extends TestJPF {
  33
  34   /**
  35    * Add double
  36    * ..., value1, value2 => ..., result
  37    */
  38   public static class DADD extends gov.nasa.jpf.jvm.bytecode.DADD {
  39     @Override
  40     public Instruction execute (ThreadInfo ti) {
  41       StackFrame frame = ti.getModifiableTopFrame();
  42
  43       double v1 = frame.popDouble();
  44       double v2 = frame.popDouble();
  45
  46       double r = v1 + v2;
  47       System.out.printf("DADD %f + %f => %f\n", v1, v2, r);
  48
  49       System.out.println(" ..but we negate it just for kicks..");
  50       r = -r;
  51
  52       frame.pushDouble(r);
  53
  54       return getNext(ti);
  55     }
  56   }
  57
  58   public static class MyInsnFactory extends gov.nasa.jpf.jvm.bytecode.InstructionFactory {
  59     public  MyInsnFactory (Config conf){
  60       // nothing here
  61     }
  62
  63     @Override
  64     public Instruction dadd() {
  65       return new DADD();
  66     }
  67   }
  68
  69   @Test
  70   public void testDadd() {
  71     if (verifyNoPropertyViolation("+jvm.insn_factory.class=.test.basic.InstructionFactoryTest$MyInsnFactory")) {
  72       double a = 41.0;
  73       double b = a + 1.0;
  74       System.out.print("b=");
  75       System.out.println(b);
  76       assertTrue( b < 0); // since we used our own (twisted) DADD
  77     }
  78   }
  79 }