diff options
author | 2011-05-03 21:18:29 -0700 | |
---|---|---|
committer | 2011-05-03 21:18:29 -0700 | |
commit | e1376a171abad9fca388a302781e59b404e8c515 (patch) | |
tree | 40bdc7718e1efddbe085500727bba70843753cde | |
parent | 8000bf8044202d668fe473c22fc4c15a3e9f3980 (diff) |
LetVC can get null label2absy from lazy inlining. So, I weakened the precondition otherwise the checked build was failing
-rw-r--r-- | Source/VCGeneration/VC.cs | 2 | ||||
-rw-r--r-- | Source/VCGeneration/Wlp.cs | 3 |
2 files changed, 0 insertions, 5 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 8c8b17a0..11db59b0 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -3621,7 +3621,6 @@ namespace VC { Hashtable/*<int, Absy!>*/ label2absy,
ProverContext proverCtxt) {
Contract.Requires(startBlock != null);
- Contract.Requires(label2absy != null);
Contract.Requires(proverCtxt != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -3640,7 +3639,6 @@ namespace VC { ProverContext proverCtxt)
{
Contract.Requires(block != null);
- Contract.Requires(label2absy != null);
Contract.Requires(blockVariables!= null);
Contract.Requires(cce.NonNullElements(bindings));
Contract.Requires(proverCtxt != null);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 23be6082..f5469ebf 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -17,7 +17,6 @@ namespace VC { [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(Label2absy!=null);
Contract.Invariant(Ctxt != null);
}
@@ -27,7 +26,6 @@ namespace VC { public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt)
{
- Contract.Requires(label2absy != null);
Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
this.Ctxt = ctxt;
@@ -36,7 +34,6 @@ namespace VC { public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt, Variable controlFlowVariable)
{
- Contract.Requires(label2absy != null);
Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
this.Ctxt = ctxt;
|