问题描述
我在代码分析期间编译后得到此异常：
I get this exception after compilation during code analysis:
CodeContracts：核心：未捕获异常失败：对象引用未设置为对象的实例。
CodeContracts：核心：堆栈跟踪： 在Microsoft.Research.CodeAnalysis.ForAllIndexedExpression.Substitute [Variable]（Func`3 map）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.Path。<> c__DisplayClass2`1。< Substitute> b__0（BoxedExpression b）
CodeContracts：Core： 在Microsoft.Research.DataStructures.FList`1.Apply（FList`1 list，Action`1 action）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.Path.Substitute [Variable]（Func`3 converter）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.Exploration.Rename（APC from，APC to，Path path，IFunctionalMap`2 renaming）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.OldAnalysisDriver`11.MDriver.BackwardTransfer [州，访客]（APC从，APC到，州州，访客访客）
CodeContracts：核心： at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.Exploration.ExpandPath（Path head，FList`1& paths）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.Exploration.DischargePaths（FList`1路径）
CodeContracts：核心： 在Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.DischargeObligation（IMethodDriver`12 mdriver，IFactQuery`2 facts，Int32 maxPathSize，APC pc，BoxedExpression goalExpression）
CodeContracts：Core： &NBSP;在Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.DischargeObligation（IMethodDriver`12 mdriver，IFactQuery`2 fact，Int32 maxPathSize，APC pc，Variable goal）
CodeContracts：Core： &NBSP; at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.Discharge [Local，Parameter，Method，Field，Property，Event，Type，Attribute，Assembly，Expression，Variable，LogOptions]（APC pc，Variable goal，Int32 maxPathSize，IMethodDriver`12
mdriver，IFactQuery`2个事实）
CodeContracts：核心： 在Microsoft.Research.CodeAnalysis.AssertionFinder.TypeBindings`11.ValidateAssertions（IFactQuery`2 facts，IMethodDriver`12 mdriver，IOutputResults output，AssertionStatistics& assertStats）
CodeContracts：Core： at Microsoft.Research.CodeAnalysis.AssertionFinder.ValidateAssertions [Local，Parameter，Method，Field，Property，Event，Type，Attribute，Assembly，Expression，Variable]（IFactQuery`2 facts，IMethodDriver`12 driver，IOutputResults
output ，AssertionStatistics& assertStats）
CodeContracts：核心： at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeNonIteratorMethodInternal（Method method）
CodeContracts：Core： at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethodInternal（Method method）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethod（Method method）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeAssembly（String assemblyName，Set`1 assembliesUnderAnalysis）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.InternalAnalyze（）
CodeContracts：Core： 在Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.Analyze（）
CodeContracts：核心：
$
CodeContracts：核心：完成后台合同分析。
CodeContracts: Core: Failed with uncaught exception: Object reference not set to an instance of an object.
CodeContracts: Core: Stack trace: at Microsoft.Research.CodeAnalysis.ForAllIndexedExpression.Substitute[Variable](Func`3 map)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.Path.<>c__DisplayClass2`1.<Substitute>b__0(BoxedExpression b)
CodeContracts: Core: at Microsoft.Research.DataStructures.FList`1.Apply(FList`1 list, Action`1 action)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.Path.Substitute[Variable](Func`3 converter)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.Exploration.Rename(APC from, APC to, Path path, IFunctionalMap`2 renaming)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.OldAnalysisDriver`11.MDriver.BackwardTransfer[State,Visitor](APC from, APC to, State state, Visitor visitor)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.Exploration.ExpandPath(Path head, FList`1& paths)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.Exploration.DischargePaths(FList`1 paths)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.DischargeObligation(IMethodDriver`12 mdriver, IFactQuery`2 facts, Int32 maxPathSize, APC pc, BoxedExpression goalExpression)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.DischargeObligation(IMethodDriver`12 mdriver, IFactQuery`2 facts, Int32 maxPathSize, APC pc, Variable goal)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.Discharge[Local,Parameter,Method,Field,Property,Event,Type,Attribute,Assembly,Expression,Variable,LogOptions](APC pc, Variable goal, Int32 maxPathSize, IMethodDriver`12 mdriver, IFactQuery`2 facts)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.AssertionFinder.TypeBindings`11.ValidateAssertions(IFactQuery`2 facts, IMethodDriver`12 mdriver, IOutputResults output, AssertionStatistics& assertStats)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.AssertionFinder.ValidateAssertions[Local,Parameter,Method,Field,Property,Event,Type,Attribute,Assembly,Expression,Variable](IFactQuery`2 facts, IMethodDriver`12 driver, IOutputResults output, AssertionStatistics& assertStats)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeNonIteratorMethodInternal(Method method)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethodInternal(Method method)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethod(Method method)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeAssembly(String assemblyName, Set`1 assembliesUnderAnalysis)
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.InternalAnalyze()
CodeContracts: Core: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.Analyze()
CodeContracts: Core:
CodeContracts: Core: Background contract analysis done.
public class Message {
public IEnumerable<CorrelationID> CorrelationIDs {
get {
Contract.Ensures(null != Contract.Result<IEnumerable<CorrelationID>>());
Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<CorrelationID>>(), x => null != x));
throw new NotImplementedException();
}
}
}
public class Session {
private void ProcessResponse(Message msg) {
Contract.Requires(null != msg);
foreach(var id in msg.CorrelationIDs) {
ProcessResponse(msg, id.Value, isResponseComplete);
}
}
}
推荐答案
我已经尝试了你的repro（在添加一些代码以使其编译之后）使用最新的内部快照，它是好的。
I've tried your repro (after adding some code to make it compile) with the latest internal snapshot and it was ok.
所以我希望在下一个版本中修复它，但如果不是，请告诉我。
So I hope this is fixed in the next release, but if it is not , please let me know.
f
这篇关于Code Contracts崩溃分析呼叫站点的Ensures（ForAll）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！