-
Notifications
You must be signed in to change notification settings - Fork 254
/
PrintStmt.cs
58 lines (48 loc) · 1.8 KB
/
PrintStmt.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
using System.Collections.Generic;
using System.CommandLine;
using System.Diagnostics.Contracts;
using System.Linq;
using DafnyCore;
using DafnyCore.Options;
namespace Microsoft.Dafny;
public class PrintStmt : Statement, ICloneable<PrintStmt>, ICanFormat {
public readonly List<Expression> Args;
public static readonly Option<bool> TrackPrintEffectsOption = new("--track-print-effects",
"A compiled method, constructor, or iterator is allowed to have print effects only if it is marked with {{:print}}.");
static PrintStmt() {
DafnyOptions.RegisterLegacyBinding(TrackPrintEffectsOption, (options, value) => {
options.EnforcePrintEffects = value;
});
DooFile.RegisterLibraryChecks(
checks: new Dictionary<Option, OptionCompatibility.OptionCheck> {
{ TrackPrintEffectsOption, OptionCompatibility.CheckOptionLocalImpliesLibrary }
});
}
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Args));
}
public PrintStmt Clone(Cloner cloner) {
return new PrintStmt(cloner, this);
}
public PrintStmt(Cloner cloner, PrintStmt original) : base(cloner, original) {
Args = original.Args.Select(cloner.CloneExpr).ToList();
}
public PrintStmt(RangeToken rangeToken, List<Expression> args)
: base(rangeToken) {
Contract.Requires(rangeToken != null);
Contract.Requires(cce.NonNullElements(args));
Args = args;
}
public override IEnumerable<Expression> NonSpecificationSubExpressions {
get {
foreach (var e in base.NonSpecificationSubExpressions) { yield return e; }
foreach (var arg in Args) {
yield return arg;
}
}
}
public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
return formatter.SetIndentPrintRevealStmt(indentBefore, OwnedTokens);
}
}