summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-08-20 00:54:15 +0000
committerGravatar tabarbe <unknown>2010-08-20 00:54:15 +0000
commit86cd755eec47845e400990c39f44bb5bbbf25d6a (patch)
tree3ed1834157cdd8ce0c4d652c8c159c23601069b6
parent0528ba569a5e3a94b1561e3759fdb1274ad029a8 (diff)
Boogie: Fixed some doubly-inherited-contract occurrences.
-rw-r--r--Source/VCGeneration/Context.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index da0bc5b0..928dd4a6 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -36,7 +36,7 @@ namespace Microsoft.Boogie
}
[ContractClassFor(typeof(ProverContext))]
-public class ProverContextContracts:ProverContext{
+public abstract class ProverContextContracts:ProverContext{
public override void AddAxiom(VCExpr vc) {
}
public override void AddAxiom(Axiom a, string attributes)
@@ -257,7 +257,7 @@ void ObjectInvariant()
[ContractClassFor(typeof(VCExprTranslator))]
- public class VCExprTranslatorContracts : VCExprTranslator {
+ public abstract class VCExprTranslatorContracts : VCExprTranslator {
public override object Clone() {
Contract.Ensures(Contract.Result<object>() != null);
throw new NotImplementedException();