summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration')
-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();