Skip to content
Snippets Groups Projects
Select Git revision
  • 9658b39544947d6a0c6155a920d4adaa11f5970f
  • master default protected
  • release/1.1.4
  • release/1.1.3
  • release/1.1.1
  • 1.4.2
  • 1.4.1
  • 1.4.0
  • 1.3.0
  • 1.2.1
  • 1.2.0
  • 1.1.5
  • 1.1.4
  • 1.1.3
  • 1.1.1
  • 1.1.0
  • 1.0.9
  • 1.0.8
  • 1.0.7
  • v1.0.5
  • 1.0.5
21 results

UsedExternalFunctions.java

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    UsedExternalFunctions.java 1.40 KiB
    package de.tla2b.analysis;
    
    import java.util.HashSet;
    import java.util.Set;
    
    import tla2sany.semantic.ExprNode;
    import tla2sany.semantic.ExprOrOpArgNode;
    import tla2sany.semantic.ModuleNode;
    import tla2sany.semantic.OpApplNode;
    import tla2sany.semantic.OpDefNode;
    
    public class UsedExternalFunctions extends AbstractASTVisitor {
    
    	public enum EXTERNAL_FUNCTIONS {
    		CHOOSE
    	}
    
    	private final Set<EXTERNAL_FUNCTIONS> usedExternalFunctions;
    
    	public Set<EXTERNAL_FUNCTIONS> getUsedExternalFunctions() {
    		return usedExternalFunctions;
    	}
    
    	public UsedExternalFunctions(ModuleNode moduleNode,
    			SpecAnalyser specAnalyser) {
    		usedExternalFunctions = new HashSet<UsedExternalFunctions.EXTERNAL_FUNCTIONS>();
    
    		visitAssumptions(moduleNode.getAssumptions());
    
    		for (OpDefNode def : specAnalyser.getUsedDefinitions()) {
    			visitDefinition(def);
    		}
    
    	}
    
    	@Override
    	public void visitBuiltInNode(OpApplNode n) {
    		switch (getOpCode(n.getOperator().getName())) {
    		case OPCODE_case:
    		case OPCODE_uc:
    		case OPCODE_bc: {
    			usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
    		}
    		}
    
    		ExprNode[] in = n.getBdedQuantBounds();
    		for (ExprNode exprNode : in) {
    			visitExprNode(exprNode);
    		}
    
    		ExprOrOpArgNode[] arguments = n.getArgs();
    		for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
    			// exprOrOpArgNode == null in case the OTHER construct
    			if (exprOrOpArgNode != null) {
    				visitExprOrOpArgNode(exprOrOpArgNode);
    			}
    		}
    	}
    
    }