Skip to content

Commit c66ff83

Browse files
committed
Fix tests
1 parent e50c794 commit c66ff83

3 files changed

Lines changed: 4 additions & 7 deletions

File tree

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Throwable.java

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,9 @@ public class Throwable extends java.lang.Object implements java.io.Serializable
1212

1313
//@ protected nullable ghost String message = null;
1414
//@ protected nullable ghost Throwable cause = null;
15-
//@ protected model \seq suppressedExceptions;
16-
//@ protected model \locset suppressedListFootprint;
17-
//@ accessible suppressedListFootprint: suppressedListFootprint;
18-
//@ accessible suppressedExceptions: suppressedListFootprint;
19-
//@ protected invariant \intersect(suppressedListFootprint,\set_union(this.message, this.cause))==\empty;
15+
16+
//@ protected ghost \seq suppressedExceptions;
17+
//@ protected ghost \locset suppressedListFootprint;
2018

2119

2220
/*@ public normal_behavior
@@ -90,7 +88,6 @@ public Throwable(java.lang.Throwable arg0) {
9088
/// throwable invariant
9189
/*@ public normal_behavior
9290
@ assignable suppressedListFootprint;
93-
@ accessible suppressedListFootprint;
9491
@ ensures suppressedExceptions == \seq_concat(suppressedExceptions, \seq_singleton(exception));
9592
*/
9693
public /*@ helper @*/ final synchronized void addSuppressed(Throwable exception);

key.core/src/test/java/TranslationTest.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ static void setup() {
3636
sorts.add(new SortImpl(new Name("double"), ImmutableSet.empty(), false));
3737
sorts.add(new SortImpl(new Name("float"), ImmutableSet.empty(), false));
3838
sorts.add(new SortImpl(new Name("Seq"), ImmutableSet.empty(), false));
39+
sorts.add(new SortImpl(new Name("LocSet"), ImmutableSet.empty(), false));
3940
services.activateJava(null);
4041
converter = services.getJavaService().getConverter(null);
4142
services.getJavaService().parseSpecialClasses();

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/README.md

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ the feature under test (verified by loading each and inspecting the error):
3030
| `local-class` | `Unsupported element: LocalClassDeclarationStmt` |
3131
| `static-import` | `Unsupported element: ImportDeclaration` (the `static` import) |
3232
| `annotation-declaration` | `Unsupported element: AnnotationDeclaration` (the `@interface`) |
33-
| `multi-catch` | `Unsupported element: UnionType` |
3433
| `lambda` | `Unsupported element: LambdaExpr` |
3534
| `method-reference` | `Unsupported element: MethodReferenceExpr` |
3635
| `instanceof-pattern` | `Unsupported element: TypePatternExpr` (the bound pattern) |

0 commit comments

Comments
 (0)