Hi,

I am trying to build my Spec# project but an internal error with the following message raised:

Error 1 Internal Compiler Error: System.ApplicationException: unimplemented   at System.Compiler.EmptyVisitor.VisitNameBinding(NameBinding nameBinding) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\EmptyVisitor.cs:line 733   at System.Compiler.EmptyVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\EmptyVisitor.cs:line 251   at System.Compiler.CodeFlattener.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 713   at System.Compiler.EmptyVisitor.VisitExpression(Expression expression) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\EmptyVisitor.cs:line 581   at System.Compiler.CodeFlattener.simplify(Expression expression, Boolean leaveVars) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 498   at System.Compiler.CodeFlattener.simplify(Expression expression) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 487   at System.Compiler.CodeFlattener.VisitMethodCall(MethodCall call) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 1041   at System.Compiler.EmptyVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\EmptyVisitor.cs:line 169   at System.Compiler.CodeFlattener.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 713   at System.Compiler.EmptyVisitor.VisitExpression(Expression expression) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\EmptyVisitor.cs:line 581   at System.Compiler.CodeFlattener.simplify(Expression expression, Boolean leaveVars) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 498   at System.Compiler.CodeFlattener.simplify(Expression expression) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 487   at System.Compiler.CodeFlattener.VisitUnaryExpression(UnaryExpression expression) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 1116   at System.Compiler.EmptyVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\EmptyVisitor.cs:line 424   at System.Compiler.CodeFlattener.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 713   at System.Compiler.EmptyVisitor.VisitExpression(Expression expression) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\EmptyVisitor.cs:line 581   at System.Compiler.CodeFlattener.simplify(Expression expression, Boolean leaveVars) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 498   at System.Compiler.CodeFlattener.simplify(Expression expression) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 487   at System.Compiler.CodeFlattener.VisitBranch(Branch branch) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 841   at System.Compiler.EmptyVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\EmptyVisitor.cs:line 155   at System.Compiler.CodeFlattener.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 718   at System.Compiler.CodeFlattener.FlattenBlock(Block block) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 343   at System.Compiler.CodeFlattener.FlattenBlock(Block block) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 338   at System.Compiler.CodeFlattener.FlattenBlock(Block block) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 338   at System.Compiler.CodeFlattener.FlattenBlock(Block block) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 338   at System.Compiler.CodeFlattener.FlattenBlock(Block block) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 338   at System.Compiler.CodeFlattener.FlattenBlock(Block block) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 338   at System.Compiler.CodeFlattener.MakeFlat(Method method, Boolean expandAllocations, Boolean constantFold, CodeMap& codeMap) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\CodeFlattener.cs:line 161   at System.Compiler.ControlFlowGraph..ctor(Method method, Boolean duplicateFinallyBlocks, Boolean eliminateEvaluationStack, Boolean expandAllocations, Boolean constantFoldBranches) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\ControlFlow.cs:line 504   at System.Compiler.ControlFlowGraph..ctor(Method method, Boolean constantFoldBranches) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\ControlFlow.cs:line 619   at System.Compiler.ControlFlowGraph.For(Method method, Boolean ConstantFoldBranches) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\ControlFlow.cs:line 629   at System.Compiler.ControlFlowGraph.For(Method method) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\ControlFlow.cs:line 624   at System.Compiler.Analyzer.GetCFG(Method method) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\Analyzer.cs:line 101   at System.Compiler.MethodReachingDefNNArrayChecker.Check(TypeSystem t, Method method, Analyzer analyzer) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\DefiniteAssignmentAnalysis.cs:line 1733   at System.Compiler.Analyzer.GeneralAnalysis(Method method) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\Analyzer.cs:line 261   at System.Compiler.Analyzer.Analyze(Method method) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\Analyzer.cs:line 196   at System.Compiler.Analyzer.VisitMethod(Method method) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\Analyzer.cs:line 301   at System.Compiler.StandardVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 293   at System.Compiler.StandardVisitor.VisitMemberList(MemberList members) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 1246   at System.Compiler.StandardVisitor.VisitTypeNode(TypeNode typeNode) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 1644   at System.Compiler.StandardVisitor.VisitClass(Class Class) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 807   at System.Compiler.Analyzer.VisitClass(Class Class) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\Analyzer.cs:line 284   at System.Compiler.StandardVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 194   at System.Compiler.StandardVisitor.VisitTypeNodeList(TypeNodeList types) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 1658   at System.Compiler.StandardVisitor.VisitNamespace(Namespace nspace) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 1330   at System.Compiler.StandardVisitor.VisitNamespaceList(NamespaceList namespaces) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 1337   at System.Compiler.StandardVisitor.VisitNamespace(Namespace nspace) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 1331   at System.Compiler.StandardVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 338   at System.Compiler.StandardVisitor.VisitNodeList(NodeList nodes) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 839   at System.Compiler.StandardVisitor.VisitCompilationUnit(CompilationUnit cUnit) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 833   at System.Compiler.Analyzer.VisitCompilationUnit(CompilationUnit cUnit) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Analysis\Analyzer.cs:line 289   at Microsoft.SpecSharp.Analyzer.VisitCompilationUnit(CompilationUnit cUnit) in c:\codeplex_current_build\specsharp\SpecSharp\Microsoft.SpecSharp\Analyzer.cs:line 129   at System.Compiler.StandardVisitor.VisitCompilationUnitSnippet(CompilationUnitSnippet snippet) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 849   at System.Compiler.StandardVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 167   at System.Compiler.StandardVisitor.VisitCompilationUnitList(CompilationUnitList compilationUnits) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 845   at System.Compiler.StandardVisitor.VisitCompilation(Compilation compilation) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 828   at System.Compiler.StandardVisitor.Visit(Node node) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 163   at Microsoft.SpecSharp.Compiler.CompileParseTree(Compilation compilation, ErrorNodeList errorNodes) in c:\codeplex_current_build\specsharp\SpecSharp\Microsoft.SpecSharp\Compiler.cs:line 257   at System.Compiler.Compiler.CompileAssemblyFromIR(Compilation compilation, ErrorNodeList errorNodes) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Compiler\Compiler.cs:line 194   at Microsoft.VisualStudio.IntegrationHelper.ProjectManager.CompileProject(Project project, ErrorNodeList errors) in c:\codeplex_current_build\specsharp\SpecSharp\Microsoft.VisualStudio.IntegrationHelper\Helpers.cs:line 589 d:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\SpecSharp2010 1 1 SpecSharp2010

Could you please post the smallest version of your example that leads to the error. Then we can try to reproduce it.

  Peter

It happens when I am trying to extend and implement the following abstract class, I believe it is because of using the flexible arguments in some methods:

	public abstract class Transaction<T> where T: Schema {
		
		protected string filename;// = "Database.db4o";
		[SpecPublic] protected IObjectContainer? db;
		[SpecPublic] [Peer] protected T! schema;
		
		public Transaction(T! schema, string databaseName)
		{ 
			this.schema = schema;
			filename = databaseName;
		}
		
		public Transaction(string databaseName)
		{ 
			filename = databaseName;
		}
		
		public T! Schema{
			get { return schema;}
		}
		
		[Pure] public abstract bool precondition(params object[] arguments);
		
		[Pure] public abstract bool postcondition(params object[] arguments);

		public abstract bool excuteTransaction(params object[] arguments)
		requires precondition(arguments);
		ensures (result == true) ==> postcondition(arguments);


		public void start(ref IObjectContainer db)
		modifies this.db;
		ensures db != null;
		ensures schema != null;
		ensures schema.Invariants();
		{
				db = Db4oEmbedded.OpenFile(Db4oEmbedded.NewConfiguration(), filename);
				IObjectSet? set = db.QueryByExample(typeof(T!));
				assert set != null;
				schema = (T)set.Next();
		} // end of start method

		public bool commit()
		requires schema.Invariants();
		ensures result == true; // ensure that db is closed
		{ 
				bool dbIsClosed = false;
				db.Store(schema);
				dbIsClosed = db.Close(); // db.Close() calls db.Commit() implicitly and then closes the database container
				return dbIsClosed;
		} // end of commit method 

		public void abort()
		modifies schema;
		ensures schema.Invariants();
		{
				db.Rollback();
				db.Ext().Refresh(schema, int.MaxValue);				
	            db.Close();
		} // end of abort method 	
		
	} // end of class Transaction

Hi,

I am not able to compile your code, since it refers to various other classes (e.g., Schema, IObjectContainer). Please send us a a small example that compiles by itself.

Best regards,

Valentin

Hi,

I made it simple and contains all needed references, it wont have compile time errors:

using System;
using Microsoft.Contracts;

namespace Main {


	public abstract class AbstractClass<T> where T: Schema {

		[SpecPublic] [Peer] protected T! schema;
		
		public AbstractClass(T! schema)
		{ 
			this.schema = schema;
		}
		
		
		public T! Schema{
			get { return schema;}
		}
		
		[Pure] public abstract bool precondition(params object[] arguments);
		
		[Pure] public abstract bool postcondition(params object[] arguments);

		public abstract bool excuteTransaction(params object[] arguments)
		requires precondition(arguments);
		ensures (result == true) ==> postcondition(arguments);



	} // end of class AbstractClass

	interface Schema{
		
	}

	public class ExtendSchema: Schema{}

	public class ExtendAbstractClass: AbstractClass<ExtendSchema> {
		
		public ExtendAbstractClass(ExtendSchema! schema): base(schema) { }

		[Pure] public override bool precondition(params object[] arguments){
			return true;
		}
		
		[Pure] public override bool postcondition(params object[] arguments){
			return false;
		}

		public override bool excuteTransaction(params object[] arguments){
			
			return true; 
		}
	}
}

When I add the excuteTransaction method and then implement it, the internal error shows. In this method I am using two abstract pure methods

as precondition and poscondition.

Thanks,

Adnan

Hi Adnan,

the Spec# compiler's support for generics is somewhat limited and this seems to cause the error. The following code works just fine:

using System;
using Microsoft.Contracts;

namespace Main {
    public interface Schema {}

    public abstract class AbstractClass {

        [SpecPublic] [Peer] protected Schema! schema;

        public AbstractClass(Schema! schema)
        {
            this.schema = schema;
        }


        public Schema! Schema {
            get { return schema;}
        }

        [Pure] public abstract bool precondition(params object[] arguments);

        [Pure] public abstract bool postcondition(params object[] arguments);

        public abstract bool excuteTransaction(params object[] arguments)
            requires precondition(arguments);
            ensures (result == true) ==> postcondition(arguments);

    }

    public class ExtendSchema: Schema {}

    public class ExtendAbstractClass: AbstractClass {

        public ExtendAbstractClass(ExtendSchema! schema): base(schema) { }

        [Pure] public override bool precondition(params object[] arguments) {
            return true;
        }

        [Pure] public override bool postcondition(params object[] arguments) {
            return false;
        }

        public override bool excuteTransaction(params object[] arguments) {
            return true;
        }
    }
}

Best regards,

Valentin

Thanks Valentin,

In this example the problem has been solved but in my real application I did make the interface 'public'  and it is in a separate file but I still get the same error.

Hi Adnan,

the reason why my example works is that I didn't use generics. So, if you use generics in your real application it probably won't work.

Best regards,

Valentin

Thanks, I didn't notice that.