[interpreter.tests] Adapt test for #61

team-worthwhile · Feb 17, 2012 · a88d989 · a88d989
1 parent 3085bba
commit a88d989
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git a/...ests/src/edu/kit/iti/formal/pse/worthwhile/interpreter/InterpreterASTNodeVisitorTest.java b/...ests/src/edu/kit/iti/formal/pse/worthwhile/interpreter/InterpreterASTNodeVisitorTest.java
@@ -14,6 +14,7 @@
 import edu.kit.iti.formal.pse.worthwhile.model.BooleanValue;
 import edu.kit.iti.formal.pse.worthwhile.model.IntegerValue;
 import edu.kit.iti.formal.pse.worthwhile.model.Value;
+import edu.kit.iti.formal.pse.worthwhile.model.ast.Annotation;
 import edu.kit.iti.formal.pse.worthwhile.model.ast.Program;
 import edu.kit.iti.formal.pse.worthwhile.model.ast.Statement;
 import edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker;
@@ -211,6 +212,14 @@ public void testVisitReturnStatement() {
 	public void testIndexedReturnVariableReference() throws IOException {
 		Program program = TestASTProvider.getRootASTNode(TestUtils.loadTestProgram(this.getClass(), "indexed_returnvarref.ww"));
 		Interpreter interpreter = new Interpreter(program, new SpecificationChecker());
+		interpreter.addExecutionEventHandler(new AbstractExecutionEventListener() {
+
+			@Override
+                        public void annotationFailed(Annotation annotation) {
+	                        Assert.fail("Annotation failed although it shouldn’t have");
+                        }
+
+		});
 		interpreter.execute();
 		assertTrue(true);
 	}

diff --git a/implementierung/src/worthwhile.interpreter.tests/src/test/resources/indexed_returnvarref.ww b/implementierung/src/worthwhile.interpreter.tests/src/test/resources/indexed_returnvarref.ww
@@ -1,8 +1,7 @@
 function Integer[] test2(Integer N, Integer[] a)
-  _ensures _return[0] ≥ 0
+  _ensures forall Integer i, 0 <= i && i < N : _return[i] ≥ 0
 {
   return a
 }
 
 Integer[] test := test2(6, {6, 4, 2, 3, 5, 1})
-_assert test = {6, 4, 2, 3, 5, 1}