diff options
author | 2011-11-22 13:46:41 -0800 | |
---|---|---|
committer | 2011-11-22 13:46:41 -0800 | |
commit | 4a45770d4a00399455b232c21c5cd10f3a2a93a6 (patch) | |
tree | cfd726e7970a1481445a23c7e4cf5b6f4be33067 /Source/Core | |
parent | 1140d9e05274d8cc87f60602e317832cf05888fc (diff) |
added support for handling duplicate axioms
Diffstat (limited to 'Source/Core')
-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 32b27ae6..73f494f3 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 ------------------------------
|