Fix match teaclet tests

Author: unp1

key.core/src/test/java/de/uka/ilkd/key/rule/TacletForTests.java

@@ -198,6 +198,22 @@ public static Sort sortLookup(String name) {
         return getSorts().lookup(new Name(name));
     }
 
+    public static JTerm parseTerm(String termstr, Services services, NamespaceSet nss) {
+        if (termstr.isEmpty()) {
+            return null;
+        }
+
+        try {
+            KeyIO io = new KeyIO(services, nss);
+            // TacletForTests.getAbbrevs()
+            return io.parseExpression(termstr);
+        } catch (Exception e) {
+            fail("Exception occurred while parsing of " + termstr, e);
+            return null;
+        }
+
+    }
+
     public static JTerm parseTerm(String termstr, Services services) {
         if (termstr.isEmpty()) {
             return null;

key.core/src/test/java/de/uka/ilkd/key/rule/TestMatchTaclet.java

@@ -68,6 +68,10 @@ public void setUp() {
         TacletForTests.parse();
 
         services = TacletForTests.services();
+        LocationVariable i = new LocationVariable(new ProgramElementName("i"),
+            services.getJavaInfo().getKeYJavaType("int"));
+        services.getNamespaces().programVariables().add(i);
+
         TB = services.getTermBuilder();
 
         all_left = (FindTaclet) TacletForTests.getTaclet("TestMatchTaclet_for_all").taclet();
@@ -282,18 +286,17 @@ public void testConflict() {
     // test match of update terms
     @Test
     public void testUpdateMatch() {
-        LocationVariable i = new LocationVariable(new ProgramElementName("i"),
-            services.getJavaInfo().getKeYJavaType("int"));
-        services.getNamespaces().programVariables().add(i);
-        JTerm match = TacletForTests.parseTerm("\\<{}\\>{i:=2}(\\forall nat z; (q1(z)))");
+        JTerm match = TacletForTests.parseTerm("\\<{}\\>{i:=2}(\\forall nat z; (q1(z)))", services,
+            services.getNamespaces());
         match = match.sub(0);
         assertNotNull(
             all_left.getMatcher().matchFind(match, EMPTY_MATCHCONDITIONS, services),
             "Instantiations should be found as updates can be ignored if "
                 + "only the term that is matched has an update and the "
                 + "template it is matched to has none.");
 
-        JTerm match2 = TacletForTests.parseTerm("\\<{int i;}\\>{i:=Z(2(#))} true");
+        JTerm match2 = TacletForTests.parseTerm("\\<{int i;}\\>{i:=Z(2(#))} true", services,
+            services.getNamespaces());
         match2 = match2.sub(0);
         assertNotNull(assign_n.getMatcher().matchFind(match2, EMPTY_MATCHCONDITIONS,
             services), "Instantiations should be found.");
@@ -302,7 +305,7 @@ public void testUpdateMatch() {
 
     @Test
     public void testProgramMatchEmptyBlock() {
-        JTerm match = TacletForTests.parseTerm("\\<{ }\\>true ");
+        JTerm match = TacletForTests.parseTerm("\\<{ }\\>true ", services);
         FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet("empty_diamond").taclet();
         MatchResultInfo mc =
             (taclet.getMatcher().matchFind(match, EMPTY_MATCHCONDITIONS, services));
@@ -317,7 +320,7 @@ public void testProgramMatchEmptyBlock() {
 
         assertNotNull(mc);
 
-        match = TacletForTests.parseTerm("\\<{ {int i = 0;} }\\>true ");
+        match = TacletForTests.parseTerm("\\<{ {int i = 0;} }\\>true ", services);
         mc = (taclet.getMatcher().matchFind(match, EMPTY_MATCHCONDITIONS,
             services));
 
@@ -388,7 +391,8 @@ null, new LocationVariable(new ProgramElementName("testVar"),
             (taclet.getMatcher().matchFind(match, EMPTY_MATCHCONDITIONS, services));
         assertNotNull(mc, "Method-Frame should match");
 
-        JTerm termWithPV = TacletForTests.parseTerm("\\<{int i;}\\>i=0");
+        JTerm termWithPV =
+            TacletForTests.parseTerm("\\<{int i;}\\>i=0", services, services.getNamespaces());
         match = TacletForTests.parseTerm("\\<{return 2;}\\>true ");
         prg = (StatementBlock) match.javaBlock().program();
         mframe = new MethodFrame((IProgramVariable) termWithPV.sub(0).sub(0).op(), ec, prg);
@@ -468,7 +472,8 @@ public void testInsequentStateRestriction() {
         FindTaclet unrestrictedTaclet =
             (FindTaclet) TacletForTests.getTaclet("testInsequentState_2").taclet();
 
-        JTerm match = TacletForTests.parseTerm("{ i := 0 } (i = 0)");
+        JTerm match =
+            TacletForTests.parseTerm("{ i := 0 } (i = 0)", services, services.getNamespaces());
         MatchResultInfo mc = (restrictedTaclet.getMatcher().matchFind(match,
             EMPTY_MATCHCONDITIONS, services));
         assertNull(mc, "Test inSequentState failed: matched on term with update prefix");
@@ -477,7 +482,7 @@ public void testInsequentStateRestriction() {
             EMPTY_MATCHCONDITIONS, services));
         assertNotNull(mc, "Test inSequentState failed: did not match on term with update prefix");
 
-        match = TacletForTests.parseTerm("i = 0");
+        match = TacletForTests.parseTerm("i = 0", services, services.getNamespaces());
         mc = (restrictedTaclet.getMatcher().matchFind(match, EMPTY_MATCHCONDITIONS,
             services));
         assertNotNull(mc,