Mercurial > hg > Members > kono > jpf-core
diff src/tests/gov/nasa/jpf/test/mc/basic/VerifyTest.java @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/tests/gov/nasa/jpf/test/mc/basic/VerifyTest.java Fri Jan 23 10:14:01 2015 -0800 @@ -0,0 +1,161 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package gov.nasa.jpf.test.mc.basic; + + +import gov.nasa.jpf.ListenerAdapter; +import gov.nasa.jpf.search.Search; +import gov.nasa.jpf.util.test.TestJPF; +import gov.nasa.jpf.vm.Verify; + +import org.junit.Test; + + +/** + * test various Verify APIs + */ +public class VerifyTest extends TestJPF { + + @Test public void testBreak () { + + if (verifyNoPropertyViolation()) { + int y = 4; + int x = 0; + + while (x != y) { // JPF should state match on the backjump + x = x + 1; + if (x > 3) { + x = 0; + } + + Verify.breakTransition("testBreakTransition"); // this should eventually state match + } + + assert false : "we should never get here"; + } + } + + @Test public void testProperties () { + + if (verifyNoPropertyViolation("+hum=didum")) { + String target = Verify.getProperty("hum"); + System.out.println("got hum=" + target); + assert target.equals("didum"); + + Verify.setProperties("foo=bar"); + String p = Verify.getProperty("foo"); + System.out.println("got foo=" + p); + assert "bar".equals(p); + } + } + + @Test public void testChangeListener () { + + if (verifyNoPropertyViolation()) { + Verify.setProperties("listener=gov.nasa.jpf.listener.StateSpaceAnalyzer"); // This used to cause a NullPointerException + } + } + + @Test public void testGetBoolean () { + + Verify.resetCounter(0); + Verify.resetCounter(1); + + if (verifyNoPropertyViolation()) { + Verify.incrementCounter(Verify.getBoolean() ? 1 : 0); + } else { + assert Verify.getCounter(0) == 1; + assert Verify.getCounter(1) == 1; + } + } + + @Test public void testGetBooleanFalseFirst () { + boolean falseFirst, value; + + Verify.resetCounter(0); + + if (verifyNoPropertyViolation()) { + + falseFirst = Verify.getBoolean(); + + Verify.resetCounter(0); + + value = Verify.getBoolean(falseFirst); + + Verify.ignoreIf(Verify.getCounter(0) != 0); + + Verify.incrementCounter(0); + + assert value == !falseFirst; + } + } + + /** + * This test ensures that stateBacktracked() is called even if the transistion + * is ignored. This is important for listeners that keep a state that must + * match the VM's state exactly and the state is updated in the middle of + * transitions. This is not possible if a backtrack happens on an ignored + * transition and the stateBacktracked is not called. + */ + @Test + public void backtrackNotificationAfterIgnore() { + if (verifyNoPropertyViolation("+listener+=,gov.nasa.jpf.test.mc.basic.VerifyTest$CountBacktrack", + "+vm.max_transition_length=MAX")) { + if (Verify.getBoolean(false)) { + Verify.ignoreIf(true); + } + } else { + // 2 for the Verify.getBoolean, 1 for <root> + assertEquals(3, CountBacktrack.getBacktrackedCount()); + } + } + + public static class CountBacktrack extends ListenerAdapter { + + private static int m_backtrackedCount; + + @Override + public void stateBacktracked(Search search) { + m_backtrackedCount++; + } + + public static int getBacktrackedCount() { + return (m_backtrackedCount); + } + } + + // <2do>... and many more to come + + + @Test + public void testBitSet() { + int id = 2; + + if (verifyNoPropertyViolation()) { + // JPF execution only + Verify.setBitInBitSet(id, 3, true); + Verify.setBitInBitSet(id, 1, true); + + } else { + // host VM execution only + assert Verify.getBitInBitSet(id, 1) == true; + assert Verify.getBitInBitSet(id, 2) == false; + assert Verify.getBitInBitSet(id, 3) == true; + } + } +}