diff options
| -rw-r--r-- | Source/Core/Absy.cs | 2 | ||||
| -rw-r--r-- | Source/Core/ResolutionContext.cs | 20 |
2 files changed, 21 insertions, 1 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 4ec6eef8..0aaf3c46 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1044,7 +1044,7 @@ namespace Microsoft.Boogie { }
public override void Register(ResolutionContext rc) {
//Contract.Requires(rc != null);
- // nothing to register
+ rc.AddAxiom(this);
}
public override void Resolve(ResolutionContext rc) {
//Contract.Requires(rc != null);
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 251ca1db..128df8c5 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -349,6 +349,26 @@ namespace Microsoft.Boogie { // not present in the relevant levels
return null;
}
+ Hashtable axioms = new Hashtable();
+
+ public void AddAxiom(Axiom axiom) {
+ string axiomName = QKeyValue.FindStringAttribute(axiom.Attributes, "name");
+ if (axiomName == null)
+ return;
+ var previous = (Axiom)axioms[axiomName];
+ if (previous == null) {
+ axioms.Add(axiomName, axiom);
+ }
+ else {
+ var r = (Axiom)SelectNonExtern(axiom, previous);
+ if (r == null) {
+ Error(axiom, "more than one declaration of axiom name: {0}", axiomName);
+ }
+ else {
+ axioms[axiomName] = r;
+ }
+ }
+ }
// ------------------------------ Functions/Procedures ------------------------------
|