NullReferenceException in Clousot/cccheck

[DanTup]

I enabled Code Contracts (all default settings, except unticked Check In Background hoping it might work around #137 - it didn't) on a project in a big solution I have, and this was spat into the output window as it ran.

Unfortunately the chances of my getting a repro I can provide are slim (it's a massive project I can't share, and I doubt I could repro it in small, shareable codebase), but I'm hoping since it's an NRE with a stack, it might be possible to figure out from the error alone.

There are no contract annotations in any of our code (though the default settings include inferring and suggesting some).

CodeContracts: MyProject.Thing.AL: Run static contract analysis.
CodeContracts: MyProject.Thing.AL: Time spent connecting to the cache: 00:00:01.0514598
CodeContracts: MyProject.Thing.AL: Cache used: (LocalDb)\MSSQLLocalDB
C:\Work\Source\Thing\Thing-Code-Contracts\MyProject.Thing.AL\DataFields\MediaDataField.cs(83,5): message : CodeContracts: Suggested ensures for member Retrieve: The caller expects the postcondition Contract.Ensures(Contract.Result<SystemWrapper.IO.IFileInfoWrap>() != null); to hold for the interface member Retrieve. Consider adding such postcondition to enforce all implementations to guarantee it
C:\Work\Source\Thing\Thing-Code-Contracts\MyProject.Thing.AL\DataFields\CollectionDataField.cs(37,4): message : CodeContracts: Suggested ensures for member get_Value: The caller expects the postcondition Contract.Ensures(Contract.Result<System.Collections.Generic.List<T>>() != null); to hold for the interface member get_Value. Consider adding the postcondition to enforce all implementations to guarantee it
CodeContracts: MyProject.Thing.AL: Internal error in Clousot/cccheck --- catching it, and continuing
CodeContracts: MyProject.Thing.AL: \nException Type:System.NullReferenceException
CodeContracts: MyProject.Thing.AL: \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: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.BoxedExpression.ContractExpression.get_SourceAssertionCondition()
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.ClousotExpressionCodeProvider`5.SourceAssertionCondition(PC pc)
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.MethodCache`9.SubroutineBase`1.SourceAssertionCondition(Label label)
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.MethodCache`9.BlockWithLabels`1.SourceAssertionCondition(APC pc)
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericValueAnalysis`2.<ReducePostconditions>b__12(SyntacticTest test)
CodeContracts: MyProject.Thing.AL: \n   at System.Linq.Enumerable.WhereSelectListIterator`2.MoveNext()
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.DataStructures.Set`1.AddRange(IEnumerable`1 range)
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.DataStructures.Set`1..ctor(IEnumerable`1 original)
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericValueAnalysis`2.ReducePostconditions(List`1 postconditions)
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericValueAnalysis`2.SuggestPostcondition(ContractInferenceManager inferenceManager\, IFixpointInfo`2 fixpointInfo)
CodeContracts: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.RunContractInference(Int32 phasecount\, String methodFullName\, IMethodDriver`12 mdriver\, AnalysisStatistics& methodStats\, List`1 results\, ContractInferenceManager inferenceManager\, ComposedFactQuery`1 factQuery)
CodeContracts: MyProject.Thing.AL: \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: MyProject.Thing.AL: \n   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethodInternal2(Method method\, MethodAnalysisFlags analysisFlags\, IClassDriver`13& cdriver\, AnalysisStatistics& methodStats\, APC& entryPC)
CodeContracts: MyProject.Thing.AL: Validated:  99.6%
CodeContracts: MyProject.Thing.AL: Checked 880 assertions: 833 correct 3 unknown (44 masked)
CodeContracts: MyProject.Thing.AL: Contract density: 2.55
CodeContracts: MyProject.Thing.AL: Total methods analyzed 89
CodeContracts: MyProject.Thing.AL: Methods analyzed with a faster abstract domain 0
CodeContracts: MyProject.Thing.AL: Method analyses read from the cache 75
CodeContracts: MyProject.Thing.AL: Methods not found in the cache 14
CodeContracts: MyProject.Thing.AL: Methods with 0 warnings 77
CodeContracts: MyProject.Thing.AL: Time spent in internal, potentially costly, operations
CodeContracts: MyProject.Thing.AL: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.1861224 (invoked 79224 times)

[daiplusplus]

I have a similar issue myself, here's my stack-trace below.

My project isn't anything super-secret or confidential, it's a simple database application using Entity Framework 6, so I'll be happy to provide the project if anyone needs it.

The output doesn't tell me which method it was analyzing when it died, but based on the last-good and next-good output I believe it was trying to process a function that contained a rather complicated Linq expression.

CodeContracts: Rss: Internal error in Clousot/cccheck --- catching it, and continuing
CodeContracts: Rss: \nException Type:System.NullReferenceException
CodeContracts: Rss: \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: Rss: \n   at Microsoft.Research.CodeAnalysis.BoxedExpressionReader`11.ExpressionInPostStateHelper(BoxedExpression exp\, Boolean replaceReturnValue\, Boolean overrideAccessModifiers\, Boolean allowReturnValue\, Details& details)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.BoxedExpressionReader`11.ExpressionInPostStateHelper(BoxedExpression exp\, Boolean replaceReturnValue\, Boolean overrideAccessModifiers\, Boolean allowReturnValue\, Details& details)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.BoxedExpressionReader`11.ExpressionInPostStateHelper(BoxedExpression exp\, Boolean replaceReturnValue\, Boolean overrideAccessModifiers\, Boolean allowReturnValue\, Details& details)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.BoxedExpressionReader`11.ExpressionInPostStateHelper(BoxedExpression exp\, Boolean replaceReturnValue\, Boolean overrideAccessModifiers\, Boolean allowReturnValue\, Details& details)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.BoxedExpressionReader`11.ExpressionInPostStateHelper(BoxedExpression exp\, Boolean replaceReturnValue\, Boolean overrideAccessModifiers\, Boolean allowReturnValue\, Details& details)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.BoxedExpressionReader`11.ExpressionInPostStateHelper(BoxedExpression exp\, Boolean replaceReturnValue\, Boolean overrideAccessModifiers\, Boolean allowReturnValue\, Details& details)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.BoxedExpressionReader`11.ExpressionInPostStateHelper(BoxedExpression exp\, Boolean replaceReturnValue\, Boolean overrideAccessModifiers\, Boolean allowReturnValue\, Details& details)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.BoxedExpressionReader`11.ExpressionInPostStateHelper(BoxedExpression exp\, Boolean replaceReturnValue\, Boolean overrideAccessModifiers\, Boolean allowReturnValue\, Details& details)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericValueAnalysis`2.ToListOfBoxedExpressions(AbstractDomain astate\, BoxedExpressionReader`11 expInPostState)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericNumericalAnalysis`1.SuggestPostconditionsFromReturnState(IFixpointInfo`2 fixpointInfo\, List`1 expressions)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericNumericalAnalysis`1.SuggestAnalysisSpecificPostconditions(ContractInferenceManager inferenceManager\, IFixpointInfo`2 fixpointInfo\, List`1 postconditions)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.ArrayAnalysis`2.SuggestAnalysisSpecificPostconditions(ContractInferenceManager inferenceManager\, IFixpointInfo`2 fixpointInfo\, List`1 postconditions)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericValueAnalysis`2.SuggestPostcondition(ContractInferenceManager inferenceManager\, IFixpointInfo`2 fixpointInfo)
CodeContracts: Rss: \n   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.RunContractInference(Int32 phasecount\, String methodFullName\, IMethodDriver`12 mdriver\, AnalysisStatistics& methodStats\, List`1 results\, ContractInferenceManager inferenceManager\, ComposedFactQuery`1 factQuery)
CodeContracts: Rss: \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: Rss: \n   at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethodInternal2(Method method\, MethodAnalysisFlags analysisFlags\, IClassDriver`13& cdriver\, AnalysisStatistics& methodStats\, APC& entryPC)