Flag all shows both context and the debug info

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java

@@ -22,8 +22,8 @@ public class CommandLineArgs {
     @Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output")
     public boolean debugMode;
 
-    @Option(names = { "-a", "--all-context" }, description = "Print the full context after every checked element")
-    public boolean printContext;
+    @Option(names = { "-a", "--all" }, description = "Print the full context plus the debug trace (implies -d)")
+    public boolean all;
 
     @Option(names = { "-lsp", "--language-server" }, description = "Enable language server mode for editor support")
     public boolean lspMode;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java

@@ -4,8 +4,6 @@
 import java.util.List;
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.processor.VCImplication;
-import liquidjava.processor.context.Context;
-import liquidjava.processor.context.ContextHistory;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
@@ -38,12 +36,12 @@ private DebugLog() {
     }
 
     public static boolean enabled() {
-        return CommandLineLauncher.cmdArgs.debugMode;
+        return CommandLineLauncher.cmdArgs.debugMode || CommandLineLauncher.cmdArgs.all;
     }
 
-    /** Gate for the full-context dump, driven by the {@code -a} / {@code --all-context} flag (independent of debug). */
+    /** Gate for the full-context dump, driven by the {@code -a} / {@code --all} flag (the verbose tier of debug). */
     public static boolean contextEnabled() {
-        return CommandLineLauncher.cmdArgs.printContext;
+        return CommandLineLauncher.cmdArgs.all;
     }
 
     /**
@@ -473,12 +471,4 @@ public static void contextAtElement(CtElement element, String contextInfo) {
         System.out.println(header);
         System.out.println(contextInfo);
     }
-
-    public static void log(String string) {
-        if (!enabled()) {
-            return;
-        }
-        System.out.println(string);
-
-    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java

@@ -46,8 +46,7 @@ public void clearHistory() {
     }
 
     public void saveContext(CtElement element, Context context) {
-        if (!CommandLineLauncher.cmdArgs.lspMode && !CommandLineLauncher.cmdArgs.debugMode
-                && !CommandLineLauncher.cmdArgs.printContext)
+        if (!CommandLineLauncher.cmdArgs.lspMode && !CommandLineLauncher.cmdArgs.all)
             return;
 
         String file = Utils.getFile(element);
@@ -67,7 +66,7 @@ public void saveContext(CtElement element, Context context) {
         aliases.addAll(context.getAliases());
         methods.addAll(context.getCtxFunctions());
 
-        // Gate lives inside DebugLog.contextAtElement (-a / --all-context); no-op unless that flag is set.
+        // Gate lives inside DebugLog.contextAtElement (-a / --all); no-op unless that flag is set.
         DebugLog.contextAtElement(element, prettyPrint());
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -75,10 +75,10 @@ public RefinementTypeChecker(Context context, Factory factory) {
     // --------------------- Visitors -----------------------------------
 
     /**
-     * Under {@code -a} / {@code --all-context}, dump the context after every top-level statement. {@code super.scan}
-     * runs the full {@code visitCtXxx} override first, so the statement's refinement effect is already applied to the
-     * context by the time we save it. The {@code STATEMENT} role filter keeps this to actual statements (direct block /
-     * case children), skipping sub-expressions like the {@code g(x)} in {@code f(g(x))}.
+     * Under {@code -a} / {@code --all}, dump the context after every top-level statement. {@code super.scan} runs the
+     * full {@code visitCtXxx} override first, so the statement's refinement effect is already applied to the context by
+     * the time we save it. The {@code STATEMENT} role filter keeps this to actual statements (direct block / case
+     * children), skipping sub-expressions like the {@code g(x)} in {@code f(g(x))}.
      */
     @Override
     public void scan(CtElement element) {