Merge branch 'master' into highprecision

nickbattle · Jan 13, 2024 · 9fc8ad2 · 9fc8ad2
2 parents b4e62d3 + 2b3dfdd
commit 9fc8ad2
Show file tree

Hide file tree

Showing 3 changed files with 41 additions and 2 deletions.
diff --git a/annotations/src/main/java/annotations/tc/TCOnFailAnnotation.java b/annotations/src/main/java/annotations/tc/TCOnFailAnnotation.java
@@ -48,7 +48,6 @@ public class TCOnFailAnnotation extends TCAnnotation
 {
 	private static final long serialVersionUID = 1L;
 	private String format = null;
-	@SuppressWarnings("unused")
 	private TCAnnotationList doclinks = null;
 
 	public TCOnFailAnnotation(TCIdentifierToken name, TCExpressionList args)

diff --git a/annotations/src/main/java/annotations/tc/TCWarningAnnotation.java b/annotations/src/main/java/annotations/tc/TCWarningAnnotation.java
@@ -24,6 +24,7 @@
 
 package annotations.tc;
 
+import java.io.File;
 import java.util.HashSet;
 import java.util.Iterator;
 import java.util.Set;
@@ -177,4 +178,35 @@ private void postCheck()
 			}
 		}
 	}
+
+	/**
+	 * We have to use a doClose because the final stage of unusedChecks in the
+	 * module typechecker are called after all the modules have been processed,
+	 * so warnings may be raised after all of the tcAfter cases above.
+	 */
+	@Override
+	public void doClose()
+	{
+		Iterator<VDMWarning> witer = TypeChecker.getWarnings().iterator();
+		int myLine  = name.getLocation().startLine;
+		File myFile = name.getLocation().file;
+
+		while (witer.hasNext())
+		{
+			VDMWarning w = witer.next();
+
+			if (moduleName != null && !w.location.module.equals(moduleName))
+			{
+				continue;
+			}
+
+			if (w.location.startLine == myLine + 1 &&
+				w.location.file.equals(myFile) &&
+				suppressed.contains((long)w.number))
+			{
+				// Warning is on the line after the one we annotated, so remove it
+				witer.remove();
+			}
+		}
+	}
 }
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/Environment.java b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/Environment.java
@@ -210,7 +210,15 @@ public void listAlternatives(TCNameToken name)
 		{
 			if (possible.isFunctionOrOperation())
 			{
-				TypeChecker.detail("Possible", possible.name);
+				boolean accessible = TCClassDefinition.isAccessible(this, possible, false);
+				String tag = "Possible";
+
+				if (!accessible)
+				{
+					tag = tag + " (but " + possible.accessSpecifier + ")";
+				}
+
+				TypeChecker.detail(tag, possible.name);
 			}
 		}
 	}