Fix test to also test the textual translator and not just the parser

KeYProject · Oct 20, 2023 · f2fc9fd · f2fc9fd
1 parent dde676b
commit f2fc9fd
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 5 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java
@@ -35,7 +35,7 @@ public String getParsableDeclaration() {
             } else {
                 JMLModifier jmlMod = JMLModifier.valueOf(it.name());
                 if (jmlMod == JMLModifier.NON_NULL || jmlMod == JMLModifier.NULLABLE) {
-                    return "/*@ " + jmlMod.toString() + " @*/";
+                    return "/*@ " + jmlMod + " @*/";
                 } else {
                     return StringUtil.repeat(" ", it.toString().length());
                 }

diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java
@@ -8,6 +8,8 @@
 import java.util.List;
 import java.util.stream.Stream;
 
+import de.uka.ilkd.key.speclang.jml.pretranslation.JMLModifier;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl;
 import org.antlr.v4.runtime.CommonTokenStream;
 import org.junit.jupiter.api.DynamicTest;
 import org.junit.jupiter.api.Test;
@@ -67,13 +69,25 @@ model nullable Object foo(nullable Nullable n) {
         }
         assertEquals(0, parser.getNumberOfSyntaxErrors());
 
+        // Test parser
         List<JmlParser.ModifierContext> modelMethodModifiers =
-            ctx.classlevel_comment(1).modifiers().modifier();
+                ctx.classlevel_comment(1).modifiers().modifier();
         assertTrue(modelMethodModifiers.stream().anyMatch(it -> it.NULLABLE() != null));
         JmlParser.Param_listContext modelMethodParameters =
-            ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list();
+                ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list();
         assertTrue(
-            modelMethodParameters.param_decl().stream().anyMatch(it -> it.NULLABLE() != null));
+                modelMethodParameters.param_decl().stream().anyMatch(it -> it.NULLABLE() != null));
+
+        // Test translation
+        final TextualTranslator translator = new TextualTranslator();
+        ctx.accept(translator);
+        final var translationOpt =
+                translator.constructs.stream().filter(c -> c instanceof TextualJMLMethodDecl).findFirst();
+
+        assertTrue(translationOpt.isPresent(), "No model method declaration found");
+        final var methodDecl = ((TextualJMLMethodDecl)translationOpt.get()).getParsableDeclaration();
+        assertTrue(methodDecl.contains("/*@ nullable @*/ Object"), "Return value is not nullable");
+        assertTrue(methodDecl.contains("/*@ nullable @*/ Nullable n"), "Parameter is not nullable");
     }
 
     @Test
@@ -97,17 +111,31 @@ model non_null Object foo(non_null Nullable n) {
             }
         } catch (Exception e) {
             debugLexer(modelMethodNullable);
-            System.out.println(e.getMessage());
         }
         assertEquals(0, parser.getNumberOfSyntaxErrors());
 
+        // Test parser
+
         List<JmlParser.ModifierContext> modelMethodModifiers =
             ctx.classlevel_comment(1).modifiers().modifier();
         assertTrue(modelMethodModifiers.stream().anyMatch(it -> it.NON_NULL() != null));
         JmlParser.Param_listContext modelMethodParameters =
             ctx.classlevel_comment(2).classlevel_element().method_declaration().param_list();
         assertTrue(
             modelMethodParameters.param_decl().stream().anyMatch(it -> it.NON_NULL() != null));
+
+        // Test translation
+
+        final TextualTranslator translator = new TextualTranslator();
+        ctx.accept(translator);
+        final var translationOpt =
+                translator.constructs.stream().filter(c -> c instanceof TextualJMLMethodDecl).findFirst();
+
+        assertTrue(translationOpt.isPresent(), "No model method declaration found");
+        final var methodDecl = ((TextualJMLMethodDecl)translationOpt.get()).getParsableDeclaration();
+        assertTrue(methodDecl.contains("/*@ non_null @*/ Object"), "Return value is not non_null");
+        assertTrue(methodDecl.contains("/*@ non_null @*/ Nullable n"), "Parameter is not non_null");
+
     }
 
     private void debugLexer(String expr) {