diff options
| -rw-r--r-- | Source/Dafny/Compiler.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 60b8f143..a4541414 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -247,7 +247,7 @@ namespace Microsoft.Dafny { else if (d is ClassDecl) {
var cl = (ClassDecl)d;
Indent(indent);
- if (cl.TraitsObj != null)
+ if (cl.TraitsObj != null && cl.TraitsObj.Count > 0)
{
wr.WriteLine("public class @{0} : @{1}", cl.CompileName, cl.TraitsStr);
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index d31e427b..8119735b 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -509,7 +509,7 @@ namespace Microsoft.Dafny { {
foreach (ModuleDefinition m in program.Modules)
{
- if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitsObj != null) || (d is TraitDecl)))
+ if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitsObj != null && ((ClassDecl)d).TraitsObj.Count > 0) || (d is TraitDecl)))
{
//adding const unique NoTraitAtAll: ClassName;
Token tNoTrait = new Token();
@@ -527,7 +527,7 @@ namespace Microsoft.Dafny { if (d is ClassDecl)
{
var c = (ClassDecl)d;
- if (c is ClassDecl && c.TraitsObj != null)
+ if (c is ClassDecl && c.TraitsObj != null && c.TraitsObj.Count > 0)
{
foreach (TraitDecl traitObj in c.TraitsObj)
{
@@ -545,7 +545,7 @@ namespace Microsoft.Dafny { sink.AddTopLevelDeclaration(traitParentAxiom);
}
}
- else if (c is ClassDecl && c.TraitsObj == null)
+ else if (c is ClassDecl && (c.TraitsObj == null || c.TraitsObj.Count == 0))
{
//this adds: axiom TraitParent(class.B) == NoTraitAtAll; Where B does not extend any traits
Bpl.TypedIdent noTraitAtAll_id = new Bpl.TypedIdent(c.tok, "NoTraitAtAll", predef.ClassNameType);
@@ -1328,7 +1328,7 @@ namespace Microsoft.Dafny { //this adds: axiom implements$J(class.C);
else if (c is ClassDecl)
{
- if (c.TraitsObj != null)
+ if (c.TraitsObj != null && c.TraitsObj.Count > 0)
{
//var dtypeFunc = FunctionCall(c.tok, BuiltinFunction.DynamicType, null, o);
//Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
|