Mercurial > hg > Members > kono > jpf-core

comparison 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
comparison
equal deleted inserted replaced
21:caa0924e093d 22:cd7880ab73c7
135 if (Verify.getCounter(0) != 3) { 135 if (Verify.getCounter(0) != 3) {
136 fail("wrong number of backtracks"); 136 fail("wrong number of backtracks");
137 } 137 }
138 } 138 }
139 } 139 }
140
141
142
143 @Test
144 public void testTypedObjectChoice() {
145
146 if (!isJPFRun()) {
147 Verify.resetCounter(0);
148 }
149
150 if (verifyNoPropertyViolation("+my_typed_object.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
151 "+my_typed_object.type=" + MyType.class.getName())) {
152
153 MyType o1 = new MyType("one");
154 MyType o2 = new MyType("two");
155
156 Object o = Verify.getObject("my_typed_object");
157 Verify.incrementCounter(0);
158 System.out.println(o);
159 }
160
161 if (!isJPFRun()) { // this is only executed outside JPF
162 if (Verify.getCounter(0) != 2) {
163 fail("wrong number of backtracks");
164 }
165 }
166
167 }
168 } 140 }