Static checker uncaught exception

Question

I found the strange situation in which static checker failed with details:

Failed with uncaught exception: Object reference not set to an instance of an object.
Stack trace:    at Microsoft.Contracts.Foxtrot.HelperMethods.CopiedMemberName(Member original)
   at Microsoft.Contracts.Foxtrot.HelperMethods.SafeAddMember(TypeNode targetType, Member duplicatedMember, Member original)
   at Microsoft.Contracts.Foxtrot.HelperMethods.DuplicateContractAndClosureParts(Duplicator dup, Method targetMethod, Method sourceMethod, ContractNodes contractNodes, Boolean copyValidations)
   at Microsoft.Contracts.Foxtrot.ExtractorVisitor.CopyAbbreviatorContracts(Method targetMethod, Method abbreviatorMethodInstance, Expression targetObject, ExpressionList actuals, RequiresList Preconditions, EnsuresList Postconditions, SourceContext useSite, RequiresList validations, Block contractInitializer)
   at Microsoft.Contracts.Foxtrot.ExtractorVisitor.ExtractFromClump(StatementList contractClump, Method method, GatherLocals gatherLocals, RequiresList Preconditions, EnsuresList Postconditions, RequiresList validations, EnsuresList modelPostconditions, SourceContext defaultContext, Method originalMethod, Block contractInitializer)
   at Microsoft.Contracts.Foxtrot.ExtractorVisitor.CheapAndDirty(Method method, RequiresList& Preconditions, EnsuresList& Postconditions, RequiresList& Validations, EnsuresList& modelPostConditions, Block contractInitializerBlock)
   at Microsoft.Contracts.Foxtrot.ExtractorVisitor.ExtractContractsForMethod(Method method, Object dummy)
   at System.Compiler.Method.MethodContractProvider.Invoke(Method method, Object handle)
   at System.Compiler.Method.get_Contract()
   at System.Compiler.Inspector.VisitMethod(Method method)
   at Microsoft.Contracts.Foxtrot.GenerateDocumentationFromPDB.VisitMethod(Method method)
   at System.Compiler.Inspector.VisitMemberList(MemberList members)
   at System.Compiler.Inspector.VisitTypeNode(TypeNode typeNode)
   at Microsoft.Contracts.Foxtrot.GenerateDocumentationFromPDB.VisitTypeNode(TypeNode typeNode)
   at System.Compiler.Inspector.VisitTypeNodeList(TypeNodeList types)
   at System.Compiler.Inspector.VisitAssembly(AssemblyNode assembly)
   at System.Compiler.Analysis.CCIMDDecoder.TryLoadAssembly(String fileName, IDictionary assemblyCache, Action`1 errorHandler, AssemblyNode& assem, Boolean legacyContractMode, List`1 referencedAssemblies)
   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.InternalAnalyze()
   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.Analyze()

1.4.50327.0, static checker options have no meaning.

Unfortunately I can't provide small repro for this error. I only can say that error occurs when I use 'SequenceNotNullNotEmptyNoNullElements' (but not 'SequenceNotNullNoNullElements') contract abbreviator:

[ContractAbbreviator]
public static void SequenceNotNullNoNullElements(IEnumerable<object> sequence)
{
    Contract.Requires(sequence != null);
    Contract.Requires(Contract.ForAll(sequence, e => e != null));
}

[ContractAbbreviator]
public static void SequenceNotNullNotEmptyNoNullElements(IEnumerable<object> sequence)
{
    SequenceNotNullNoNullElements(sequence);
    Contract.Requires(sequence.Any());
}

These abbreviators are in some 'ProjectA', and usage of abbreviators is in another 'ProjectB'. When I move abbreviators directly to 'ProjectB', or to another empty 'ProjectC' - error disappears.

Answer 1

Hmm. I found out that if I activate rewriter (check 'Perform Runtime Contract Checking' with any mode) - error disappears. It also fixes regular unpredictable Visual Studio crashes when I use 'Code analysis' (FxCop) and contracts static analysis, which I despaired to fix. I manually define 'CONTRACTS_FULL' symbol on all builds to fix ReSharper bug and I thought that disabled rewriter causes to runtime exceptions that have no influence on static analysis tools...