|
15 | 15 | import de.uka.ilkd.key.control.DefaultUserInterfaceControl; |
16 | 16 | import de.uka.ilkd.key.control.KeYEnvironment; |
17 | 17 | import de.uka.ilkd.key.nparser.ParsingFacade; |
18 | | -import de.uka.ilkd.key.java.Position; |
19 | | -import de.uka.ilkd.key.parser.Location; |
20 | 18 | import de.uka.ilkd.key.proof.Goal; |
21 | 19 | import de.uka.ilkd.key.proof.Proof; |
22 | 20 | import de.uka.ilkd.key.smt.newsmt2.MasterHandlerTest; |
|
25 | 23 |
|
26 | 24 | import com.fasterxml.jackson.databind.ObjectMapper; |
27 | 25 | import com.fasterxml.jackson.dataformat.yaml.YAMLFactory; |
| 26 | +import org.jspecify.annotations.Nullable; |
28 | 27 | import org.junit.jupiter.api.Assertions; |
29 | 28 | import org.junit.jupiter.params.ParameterizedTest; |
30 | 29 | import org.junit.jupiter.params.provider.Arguments; |
|
37 | 36 | * see {@link MasterHandlerTest} from where I copied quite a bit. |
38 | 37 | */ |
39 | 38 | public class TestProofScriptCommand { |
40 | | - public record TestInstance(String key, String script, String exception, |
| 39 | + public record TestInstance(String key, String script, @Nullable String exception, |
41 | 40 | String[] goals, Integer selectedGoal) { |
42 | 41 | } |
43 | 42 |
|
@@ -83,13 +82,13 @@ void testProofScript(File file, TestInstance data) throws Exception { |
83 | 82 | try { |
84 | 83 | pse.execute(env.getUi(), proof); |
85 | 84 | } catch (ScriptException ex) { |
86 | | - assertTrue(props.containsKey("exception"), |
| 85 | + assertTrue(data.exception != null && !data.exception.isEmpty(), |
87 | 86 | "An exception was not expected, but got " + ex.getMessage()); |
88 | 87 | // weigl: fix spurious error on Windows machine due to different file endings. |
89 | 88 | String msg = ex.getMessage().trim().replaceAll("\r\n", "\n"); |
90 | | - Assertions.assertTrue(msg.startsWith(props.get("exception").trim()), |
| 89 | + Assertions.assertTrue(msg.startsWith(data.exception.trim()), |
91 | 90 | "Unexpected exception: " + ex.getMessage() + "\n expected: " |
92 | | - + props.get("exception").trim()); |
| 91 | + + data.exception.trim()); |
93 | 92 | return; |
94 | 93 | } |
95 | 94 |
|
|
0 commit comments