public void distributeNamedTypeInvs(List<IRStatus<PIR>> newAst)
	{
		// Collect all named type invariants
		List<ATypeDeclIR> allNamedTypeInvTypeDecls = new LinkedList<ATypeDeclIR>();
		for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(newAst, ADefaultClassDeclIR.class))
		{
			ADefaultClassDeclIR clazz = status.getIrNode();

			if (jmlGen.getJavaGen().getInfo().getDeclAssistant().isLibraryName(clazz.getName()))
			{
				continue;
			}

			for (ATypeDeclIR typeDecl : clazz.getTypeDecls())
			{
				if (typeDecl.getDecl() instanceof ANamedTypeDeclIR)
				{
					allNamedTypeInvTypeDecls.add(typeDecl);
				}
			}
		}

		for (IRStatus<ADefaultClassDeclIR> status : IRStatus.extract(newAst, ADefaultClassDeclIR.class))
		{
			ADefaultClassDeclIR clazz = status.getIrNode();

			if (jmlGen.getJavaGen().getInfo().getDeclAssistant().isLibraryName(clazz.getName()))
			{
				continue;
			}

			List<ATypeDeclIR> classTypeDecls = new LinkedList<ATypeDeclIR>(clazz.getTypeDecls());

			for (ATypeDeclIR namedTypeInv : allNamedTypeInvTypeDecls)
			{
				if (!classTypeDecls.contains(namedTypeInv))
				{
					classTypeDecls.add(namedTypeInv.clone());
				}
			}

			clazz.setTypeDecls(classTypeDecls);
		}
	}
public void distributeNamedTypeInvs ( List < IRStatus < PIR > > newAst ) { List < ATypeDeclIR > allNamedTypeInvTypeDecls = new LinkedList < ATypeDeclIR > ( ) ; for ( IRStatus < ADefaultClassDeclIR > status : IRStatus . extract ( newAst , ADefaultClassDeclIR . class ) ) { ADefaultClassDeclIR clazz = status . getIrNode ( ) ; if ( jmlGen . getJavaGen ( ) . getInfo ( ) . getDeclAssistant ( ) . isLibraryName ( clazz . getName ( ) ) ) { continue ; } for ( ATypeDeclIR typeDecl : clazz . getTypeDecls ( ) ) { if ( typeDecl . getDecl ( ) instanceof ANamedTypeDeclIR ) { allNamedTypeInvTypeDecls . add ( typeDecl ) ; } } } for ( IRStatus < ADefaultClassDeclIR > status : IRStatus . extract ( newAst , ADefaultClassDeclIR . class ) ) { ADefaultClassDeclIR clazz = status . getIrNode ( ) ; if ( jmlGen . getJavaGen ( ) . getInfo ( ) . getDeclAssistant ( ) . isLibraryName ( clazz . getName ( ) ) ) { continue ; } List < ATypeDeclIR > classTypeDecls = new LinkedList < ATypeDeclIR > ( clazz . getTypeDecls ( ) ) ; for ( ATypeDeclIR namedTypeInv : allNamedTypeInvTypeDecls ) { if ( ! classTypeDecls . contains ( namedTypeInv ) ) { classTypeDecls . add ( namedTypeInv . clone ( ) ) ; } } clazz . setTypeDecls ( classTypeDecls ) ; } }
There are problems with OpenJML when you invoke named type invariant methods across classes. Until these bugs are
fixed the workaround is simply to make sure that all generated classes have a local copy of a named invariant
method. TODO: Currently invariant method are named on the form "module_typename" although this does not truly
garuantee uniqueness. For example if module A defines type B_C the invariant method name is A_B_C. However if
module A_B defines type C then the invariant method will also be named A_B_C. So something needs to be done about
this.

@param newAst