(Yet another) NullReferenceException in Clousot/cccheck

[fedotovalex]

This seems to be different from #138 as the call stack is very different. On a plus side, I managed to reduce it to a small reproducible case:

using System;
using System.Diagnostics.Contracts;

namespace Library
{
    public class Base
    {
        public Base(
            string a
            )
        {
            if (a == null)
                throw new ArgumentNullException("a");

            Contract.EndContractBlock();

            _b = 1;
            _a = a;
            _c = C();
        }

        protected Base(
            string a,
            byte[] c
            )
        {
            if (a == null)
                throw new ArgumentNullException("a");

            Contract.EndContractBlock();

            _b = 1;
            _a = a;
            _c = c;
        }

        protected static byte[] C()
        {
            Contract.Ensures(Contract.Result<byte[]>() != null);
            return new byte[1];
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(_b > 0 && _b < 8);
            Contract.Invariant(_a != null);
        }

        private readonly int _b;
        private readonly string _a;
        private readonly byte[] _c;
    }

    public class Derived : Base
    {
        public Derived(
            )
            : base("Hello, world!")
        {
        }
    }
}

cccheck command line:

-nobox -nologo -nopex -remote  -suggest=!! -premode combined -suggest codefixes -framework:v4.5 -warninglevel full  -maxwarnings 1200 -nonnull -bounds: -arrays -wp=true -bounds:type=subpolyhedra,reduction=simplex,diseq=false  -arrays -adaptive -arithmetic -enum -suggest asserttocontracts -missingPublicRequiresAreErrors -missingPublicEnsuresAreErrors -suggest assumes -suggest objectinvariants -suggest readonlyfields -infer requires -infer autopropertiesensures -infer objectinvariants -outputwarnmasks -timeout 300 -show progress "-resolvedPaths:C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\Microsoft.CSharp.dll;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\mscorlib.dll;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Core.dll;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Data.DataSetExtensions.dll;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Data.dll;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.dll;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Net.Http.dll;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Xml.dll;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Xml.Linq.dll" "-libPaths:C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\CodeContracts;C:\Program Files (x86)\Microsoft\Contracts\Contracts\.NETFramework\v4.5 " "C:\Projects\Library\obj\Release\Decl\Library.dll"

cccheck output:

CodeContracts: Library: Background contract analysis started.
CodeContracts: Library: Method 1 :  System.Diagnostics.Contracts.ContractDeclarativeAssemblyAttribute.#ctor()
CodeContracts: Library: Method 2 :  Library.Base.#ctor(System.String,System.Byte[])
CodeContracts: Library: Method 3 :  Library.Base.C()
CodeContracts: Library: Method 4 :  Library.Base.#ctor(System.String)
CodeContracts: Library: Installing the object invariants
CodeContracts: Library: assume(invariant) this._a != null
CodeContracts: Library: Method 5 :  Library.Derived.#ctor()
CodeContracts: Library: Internal error in Clousot/cccheck --- catching it, and continuing
CodeContracts: Library: \nException Type:System.NullReferenceException
CodeContracts: Library: \nMessage:Object reference not set to an instance of an object.\, Stack TraceSystem.NullReferenceException: Object reference not set to an instance of an object.
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.SymbolicValue.GetUniqueKey(SymbolicValue v)
CodeContracts: Library: \n   at Microsoft.Research.DataStructures.FunctionalIntKeyMap`2.get_Item(A key)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.Analyzers.NonNull.TypeBindings`11.Analysis.EdgeConversion(APC from\, APC to\, Boolean isJoin\, IFunctionalMap`2 sourceTargetMap\, Domain state)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.ArrayAnalysis`2.EdgeConversion(APC from\, APC to\, Boolean isJoin\, IFunctionalMap`2 sourceTargetMap\, ArrayState state)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.ForwardAnalysisSolver`3.PushState(APC pc\, APC next\, AState state)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.DFARoot`2.ComputeFixpoint()
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.ForwardDFA`2.Run(AState startState)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.CodeLayer`13.<>c__DisplayClass1`1.<CreateForward>b__0(AnalysisState initialState)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.RunTheAnalysis[AbstractDomain\,Options](String methodName\, IMethodDriver`12 driver\, GenericValueAnalysis`2 analysis)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.Analyzers.Arrays.Analyze[Local\,Parameter\,Method\,Field\,Property\,Event\,Type\,Attribute\,Assembly\,Expression\,Variable](String fullMethodName\, IMethodDriver`12 mdriver\, Predicate`1 cachePCs)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.RunFactsDiscoveryAnalyses(Method method\, Int32 phasecount\, String methodFullName\, IClassDriver`13 cdriver\, IMethodDriver`12 mdriver\, List`1 results\, List`1 obligations\, ComposedFactQuery`1 factQuery)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.MethodAnalysisNonCached(Method method\, MethodAnalysisFlags& analysisFlags\, Int32& phasecount\, String methodFullName\, IClassDriver`13 cdriver\, IMethodDriver`12 mdriver\, AnalysisStatistics& methodStats\, ContractDensity& methodContractDensity)
CodeContracts: Library: \n   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethodInternal2(Method method\, MethodAnalysisFlags analysisFlags\, IClassDriver`13& cdriver\, AnalysisStatistics& methodStats\, APC& entryPC)
CodeContracts: Library: Validated: 100.0 %
CodeContracts: Library: Checked 15 assertions: 15 correct
CodeContracts: Library: Contract density: 1.88
CodeContracts: Library: Total methods analyzed 5
CodeContracts: Library: Methods analyzed with a faster abstract domain 0
CodeContracts: Library: Methods with 0 warnings 5
CodeContracts: Library: Time spent in internal, potentially costly, operations
CodeContracts: Library: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0069984 (invoked 159 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0099966 (invoked 571 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0179988 (invoked 44 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.1155192 (invoked 5 times)
Overall time spent performing action #ArraysJoin: 00:00:00.0599800 (invoked 1 times)
CodeContracts: Library: Total time 4.101sec. 820ms/method
CodeContracts: Library: Retained 0 preconditions after filtering
CodeContracts: Library: Inferred 1 object invariants
CodeContracts: Library: Retained 0 object invariants after filtering
CodeContracts: Library: Discovered 3 postconditions to suggest
CodeContracts: Library: Retained 0 postconditions after filtering
CodeContracts: Library: Detected 0 code fixes
CodeContracts: Library: Proof obligations with a code fix: 0
C:\WINDOWS\system32\Library.dll(1,1): message : CodeContracts: Checked 15 assertions: 15 correct
CodeContracts: Library: 
CodeContracts: Library: Background contract analysis done.