From dc974a13c117c1bb8dc6a20f5f3cabeaeb0df5b5 Mon Sep 17 00:00:00 2001
From: Wolfram Pfeifer <wolfram.pfeifer@kit.edu>
Date: Thu, 24 Oct 2024 16:35:28 +0200
Subject: [PATCH 1/4] added some annotations such that debug output with
 System.out.println typechecks

---
 src/main/java/universe/jdk.astub | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/main/java/universe/jdk.astub b/src/main/java/universe/jdk.astub
index 53eed64..7541079 100644
--- a/src/main/java/universe/jdk.astub
+++ b/src/main/java/universe/jdk.astub
@@ -1,5 +1,16 @@
 import universe.qual.Any;
 
+package java.io;
+
+class PrintStream {
+  public void print(@Any char[] s);
+  public void print(@Any String s);
+  public void print(@Any Object obj);
+  public void println(@Any char[] x);
+  public void println(@Any String s);
+  public void println(@Any Object x);
+}
+
 package java.lang;
 
 class Object {

From 1168ed28ac41266866aa77a79d7c87004fe303b1 Mon Sep 17 00:00:00 2001
From: Wolfram Pfeifer <94171076+WolframPfeifer@users.noreply.github.com>
Date: Sat, 2 Nov 2024 12:06:04 +0100
Subject: [PATCH 2/4] applied type annotation to array instead of component
 type

Co-authored-by: Werner Dietl <wdietl@gmail.com>
---
 src/main/java/universe/jdk.astub | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/java/universe/jdk.astub b/src/main/java/universe/jdk.astub
index 7541079..16f7a1e 100644
--- a/src/main/java/universe/jdk.astub
+++ b/src/main/java/universe/jdk.astub
@@ -3,10 +3,10 @@ import universe.qual.Any;
 package java.io;
 
 class PrintStream {
-  public void print(@Any char[] s);
+  public void print(char @Any [] s);
   public void print(@Any String s);
   public void print(@Any Object obj);
-  public void println(@Any char[] x);
+  public void println(char @Any [] x);
   public void println(@Any String s);
   public void println(@Any Object x);
 }

From 49f8c4b37607e298069ea81b57ed3e431a4b0865 Mon Sep 17 00:00:00 2001
From: Wolfram Pfeifer <wolfram.pfeifer@kit.edu>
Date: Thu, 28 Nov 2024 13:57:14 +0100
Subject: [PATCH 3/4] added remarks about checkOaM linter option

---
 README.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/README.md b/README.md
index ed9b137..ad92333 100644
--- a/README.md
+++ b/README.md
@@ -20,6 +20,14 @@ cd universe
 ./.ci-build.sh
 ````
 
+## Supported Options
+
+Linter options:
+* `checkOaM` Enables encapsulation checks (Owner-as-Modifier). Without this option, only topology checks are performed,
+  so make sure to enable set this option if it should be checked that `@Any` references are not used for writing.
+
+Linter options can be passed via `-Alint=<option>`. Note that everything except the last option given in that way is
+ignored (see https://checkerframework.org/manual/#alint for more details)!
 
 ## Type checking example
 

From f8da76c7589e8ec8dae9e6fce3bd7269e3416048 Mon Sep 17 00:00:00 2001
From: Wolfram Pfeifer <wolfram.pfeifer@kit.edu>
Date: Wed, 18 Dec 2024 12:03:04 +0100
Subject: [PATCH 4/4] fix bug in assignment check for OaM

---
 src/main/java/universe/UniverseVisitor.java | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/main/java/universe/UniverseVisitor.java b/src/main/java/universe/UniverseVisitor.java
index 807f9aa..50b3754 100644
--- a/src/main/java/universe/UniverseVisitor.java
+++ b/src/main/java/universe/UniverseVisitor.java
@@ -235,10 +235,9 @@ public Void visitAssignment(AssignmentTree node, Void p) {
                 AnnotatedTypeMirror receiverType = atypeFactory.getAnnotatedType(receiverTree);
 
                 if (receiverType != null) {
-                    // Still, I think receiver can still only be declared types, so
-                    // effectiveAnnotation
-                    // is not needed.
-                    if (receiverType.hasAnnotation(LOST) || receiverType.hasAnnotation(ANY)) {
+                    // We need to check effective annotations, since receiver type could be a type
+                    // variable of the class.
+                    if (receiverType.hasEffectiveAnnotation(LOST) || receiverType.hasEffectiveAnnotation(ANY)) {
                         checker.reportError(node, "oam.assignment.forbidden");
                     }
                 }