diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-10-27 17:36:29 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-10-27 17:36:29 -0700 |
| commit | a8c04614ad34b4a36c1c739f8838fe4fd6232720 (patch) | |
| tree | 73c080b032638d7e046f7e1d18d5fa7a2273c181 /Source/VCExpr/Boogie2VCExpr.cs | |
| parent | 51fe0a74abb863a3bb908e6fced5b9779446d065 (diff) | |
Boogie: Get rid of {:ignore} feature on axioms
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 4d8fed6a..4555f18c 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -17,6 +17,7 @@ using Microsoft.Basetypes; namespace Microsoft.Boogie.VCExprAST {
using Microsoft.Boogie;
+ // TODO: in future we might use that for defining symbols for Boogie's conditional compilation
public class VCGenerationOptions {
private readonly List<string/*!*/>/*!*/ SupportedProverCommands;
[ContractInvariantMethod]
|