package jkind.analysis;

import jkind.lustre.BinaryExpr;
import jkind.lustre.BinaryOp;
import jkind.lustre.Equation;
import jkind.lustre.Expr;
import jkind.lustre.Node;
import jkind.lustre.Program;
import jkind.lustre.UnaryExpr;
import jkind.lustre.UnaryOp;
import jkind.lustre.visitors.ExprIterVisitor;

public class WarnUnguardedPreVisitor extends ExprIterVisitor {
	public static void check(Program program) {
		for (Node node : program.nodes) {
			for (Equation eq : node.equations) {
				eq.expr.accept(UNGUARDED);
			}
			for (Expr e : node.assertions) {
				e.accept(UNGUARDED);
			}
		}
	}
	
	final public static WarnUnguardedPreVisitor GUARDED = new WarnUnguardedPreVisitor();
	final public static WarnUnguardedPreVisitor UNGUARDED = new WarnUnguardedPreVisitor();

	@Override
	public Void visit(UnaryExpr e) {
		if (e.op == UnaryOp.PRE) {
			if (this == GUARDED) {
				e.expr.accept(UNGUARDED);
			} else {
				System.out.println("Warning at line " + e.location + " unguarded pre expression");
			}
		} else {
			super.visit(e);
		}
		
		return null;
	}
	
	@Override
	public Void visit(BinaryExpr e) {
		if (e.op == BinaryOp.ARROW) {
			e.left.accept(this);
			e.right.accept(GUARDED);
		} else {
			super.visit(e);
		}
		
		return null;
	}
}

@@ -162,16 +162,50 @@
 e.Node;%0A
+import jkind.lustre.NodeCallExpr;%0A
 import j
@@ -1278,10 +1278,110 @@
 ull;%0A%09%7D%0A
+%09%0A%09@Override%0A%09public Void visit(NodeCallExpr e) %7B%0A%09%09UNGUARDED.visitExprs(e.args);%0A%09%09return null;%0A%09%7D%0A
 %7D%0A

Fix unguarded pre check to treat all node calls as unguarded