Mercurial > hg > Members > kono > jpf-core

diff src/tests/gov/nasa/jpf/test/mc/data/DataChoiceTest.java @ 22:cd7880ab73c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed JPF_.._Verify.registerChoiceGenerator() to not break and ignore the transition if there are no choices, but to just return the provided default value. Thanks to Pascal Kessell for reporting added a .include_null option for the TypedObjectChoice CG. If it is set (default) 'null' is included in the choice set added a dedicated reg test for TypedObjectChoice, removed the one in DataChoiceTest
author Peter Mehlitz <pcmehlitz@gmail.com>
date Tue, 14 Apr 2015 15:01:25 -0700
parents 61d41facf527
children
line wrap: on
line diff
--- a/src/tests/gov/nasa/jpf/test/mc/data/DataChoiceTest.java	Fri Apr 10 20:53:11 2015 -0700
+++ b/src/tests/gov/nasa/jpf/test/mc/data/DataChoiceTest.java	Tue Apr 14 15:01:25 2015 -0700
@@ -137,32 +137,4 @@
       }
     }
   }
-
-
-
-  @Test
-  public void testTypedObjectChoice() {
-
-    if (!isJPFRun()) {
-      Verify.resetCounter(0);
-    }
-
-    if (verifyNoPropertyViolation("+my_typed_object.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
-            "+my_typed_object.type=" + MyType.class.getName())) {
-
-      MyType o1 = new MyType("one");
-      MyType o2 = new MyType("two");
-
-      Object o = Verify.getObject("my_typed_object");
-      Verify.incrementCounter(0);
-      System.out.println(o);
-    }
-
-    if (!isJPFRun()) { // this is only executed outside JPF
-      if (Verify.getCounter(0) != 2) {
-        fail("wrong number of backtracks");
-      }
-    }
-
-  }
 }