diff options
Diffstat (limited to 'Source')
| -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;
|