diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-13 11:51:04 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-13 11:51:04 -0700 |
| commit | e4cefb56b4312d7c2bf88d9ba3c3bfd2e00940e9 (patch) | |
| tree | 421049d979a73859b13bca1172eab1d62a89f674 /Source/Dafny/Rewriter.cs | |
| parent | e90a947a54044487e8ccf984033b1113eac0d49e (diff) | |
Register the trigger generator as a a rewriter in the Resolver.
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index c0a25a82..480b3f61 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -36,6 +36,35 @@ namespace Microsoft.Dafny }
}
+ public class TriggersRewriter : IRewriter {
+ Resolver Resolver;
+
+ internal TriggersRewriter(Resolver resolver) {
+ Contract.Requires(Resolver != null);
+ this.Resolver = resolver;
+ }
+
+ public void PreResolve(ModuleDefinition m) { }
+
+ public void PostResolve(ModuleDefinition m) {
+ foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
+ if (decl is Function) {
+ var function = (Function)decl;
+ TriggerGenerator.AddTriggers(function.Ens, Resolver);
+ TriggerGenerator.AddTriggers(function.Req, Resolver);
+ TriggerGenerator.AddTriggers(function.Body, Resolver);
+ } else if (decl is Method) {
+ var method = (Method)decl;
+ TriggerGenerator.AddTriggers(method.Ens, Resolver);
+ TriggerGenerator.AddTriggers(method.Req, Resolver);
+ TriggerGenerator.AddTriggers(method.Body, Resolver);
+ }
+ }
+ }
+
+ public void PostCyclicityResolve(ModuleDefinition m) { }
+ }
+
/// <summary>
/// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate
/// into a class. From the user's perspective, what needs to be done is simply:
|