diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 6 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 26 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 15 | ||||
| -rw-r--r-- | Source/Core/ResolutionContext.cs | 142 | ||||
| -rw-r--r-- | Test/test0/Answer | 13 | ||||
| -rw-r--r-- | Test/test0/SeparateVerification0.bpl | 21 | ||||
| -rw-r--r-- | Test/test0/SeparateVerification1.bpl | 19 | ||||
| -rw-r--r-- | Test/test0/runtest.bat | 9 |
8 files changed, 151 insertions, 100 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 3929e237..dcc007fe 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -261,7 +261,8 @@ namespace Microsoft.Boogie { //BoogiePL.Errors.count = 0;
Program program = null;
bool okay = true;
- foreach (string bplFileName in fileNames) {
+ for (int fileId = 0; fileId < fileNames.Count; fileId++) {
+ string bplFileName = fileNames[fileId];
if (!suppressTraceOutput) {
if (CommandLineOptions.Clo.XmlSink != null) {
CommandLineOptions.Clo.XmlSink.WriteFileFragment(bplFileName);
@@ -274,7 +275,8 @@ namespace Microsoft.Boogie { Program programSnippet;
int errorCount;
try {
- errorCount = BoogiePL.Parser.Parse(bplFileName, null, out programSnippet);
+ var defines = new List<string>() { "FILE_" + fileId };
+ errorCount = BoogiePL.Parser.Parse(bplFileName, defines, out programSnippet);
if (programSnippet == null || errorCount != 0) {
Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
okay = false;
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index cde8fc3f..67500c88 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -235,30 +235,26 @@ namespace Microsoft.Boogie { ResolveTypes(rc);
- List<Declaration/*!*/> prunedTopLevelDecls = CommandLineOptions.Clo.OverlookBoogieTypeErrors ? new List<Declaration/*!*/>() : null;
-
+ var prunedTopLevelDecls = new List<Declaration/*!*/>();
foreach (Declaration d in TopLevelDeclarations) {
+ if (QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) {
+ continue;
+ }
// resolve all the non-type-declarations
if (d is TypeCtorDecl || d is TypeSynonymDecl) {
- if (prunedTopLevelDecls != null)
- prunedTopLevelDecls.Add(d);
} else {
int e = rc.ErrorCount;
d.Resolve(rc);
- if (prunedTopLevelDecls != null) {
- if (rc.ErrorCount != e && d is Implementation) {
- // ignore this implementation
- System.Console.WriteLine("Warning: Ignoring implementation {0} because of translation resolution errors", ((Implementation)d).Name);
- rc.ErrorCount = e;
- } else {
- prunedTopLevelDecls.Add(d);
- }
+ if (CommandLineOptions.Clo.OverlookBoogieTypeErrors && rc.ErrorCount != e && d is Implementation) {
+ // ignore this implementation
+ System.Console.WriteLine("Warning: Ignoring implementation {0} because of translation resolution errors", ((Implementation)d).Name);
+ rc.ErrorCount = e;
+ continue;
}
}
+ prunedTopLevelDecls.Add(d);
}
- if (prunedTopLevelDecls != null) {
- TopLevelDeclarations = prunedTopLevelDecls;
- }
+ TopLevelDeclarations = prunedTopLevelDecls;
foreach (Declaration d in TopLevelDeclarations) {
Variable v = d as Variable;
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 5094fb9e..84ecce6d 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1875,6 +1875,21 @@ namespace Microsoft.Boogie { Console.WriteLine(
@"Boogie: The following attributes are supported by this implementation.
+ ---- On top-level declarations ---------------------------------------------
+
+ {:ignore}
+ Ignore the declaration (after checking for duplicate names).
+ See also below for more options when :ignore is used with axioms.
+
+ {:extern}
+ If two top-level declarations introduce the same name (for example, two
+ constants with the same name or two procedures with the same name), then
+ Boogie usually produces an error message. However, if at least one of
+ the declarations is declared with :extern, one of the declarations is
+ ignored. If both declarations are :extern, Boogie arbitrarily chooses
+ one of them to keep; otherwise, Boogie ignore the :extern declaration
+ and keeps the other.
+
---- On axioms -------------------------------------------------------------
{:inline true}
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index d4b353ef..803b1f8b 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -170,15 +170,22 @@ namespace Microsoft.Boogie { public void AddType(NamedDeclaration td) {
Contract.Requires(td != null);
Contract.Assert((td is TypeCtorDecl) || (td is TypeSynonymDecl));
+ Contract.Requires(td.Name != null);
- string name = cce.NonNull(td.Name);
+ string name = td.Name;
if (CheckBvNameClashes(td, name))
return; // error has already been reported
- if (types[name] != null) {
- Error(td, "more than one declaration of type name: {0}", name);
- } else {
+ var previous = (NamedDeclaration)types[name];
+ if (previous == null) {
types.Add(name, td);
+ } else {
+ var r = (NamedDeclaration)SelectNonExtern(td, previous);
+ if (r == null) {
+ Error(td, "more than one declaration of type name: {0}", name);
+ } else {
+ types[name] = r;
+ }
}
}
@@ -247,79 +254,6 @@ namespace Microsoft.Boogie { return null; // not present
}
- // ------------------------------ Types ------------------------------
-
- // user-defined types
- // Hashtable /*string->TypeDecl*/! types = new Hashtable /*string->TypeDecl*/ ();
- /*
- public void AddType(TypeDecl td){
- Contract.Requires(td != null);
- string! name = (!)td.Name;
-
- if (name.StartsWith("bv") && name.Length > 2) {
- bool isBv = true;
- for (int i = 2; i < name.Length; ++i)
- if (!char.IsDigit(name[i])) isBv = false;
- if (isBv)
- Error(td, "type name: {0} is registered for bitvectors", name);
- }
-
- if (types[name] != null)
- {
- Error(td, "more than one declaration of type name: {0}", name);
- }
- else
- {
- types.Add(name, td);
- }
- }
- */
- /// <summary>
- /// Returns the declaration of the named type, or null if
- /// no such type is declared.
- /// </summary>
- /// <param name="name"></param>
- /// <returns></returns>
- /* public TypeDecl LookUpType(string name){
-Contract.Requires(name != null);
- return (TypeDecl)types[name];
- }
- */
- // ------------------------------ Type Binders ------------------------------
- /*
- List<TypeBinderDecl!>! typeBinders = new List<TypeBinderDecl!>(5);
-
- public void AddTypeBinder(TypeBinderDecl td){
- Contract.Requires(td != null);
- for (int i = 0; i < typeBinders.Count; i++) {
- if (typeBinders[i].Name == td.Name) {
- Error(td, "more than one declaration of type binder name: {0}", td.Name);
- return;
- }
- }
- typeBinders.Add(td);
- }
-
- public int TypeBinderState {
- get { return typeBinders.Count; }
- set { typeBinders.RemoveRange(value, typeBinders.Count - value); }
- }
-
- /// <summary>
- /// Returns the declaration of the named type binder, or null if
- /// no such binder is declared.
- /// </summary>
- public TypeDecl LookUpTypeBinder(string name){
- Contract.Requires(name != null);
- for (int i = typeBinders.Count; 0 <= --i; ) {
- TypeBinderDecl td = typeBinders[i];
- if (td.Name == name) {
- return td;
- }
- }
- return null; // not present
- }
- */
// ------------------------------ Variables ------------------------------
class VarContextNode {
@@ -365,10 +299,16 @@ Contract.Requires(name != null); public void AddVariable(Variable var, bool global) {
Contract.Requires(var != null);
- if (FindVariable(cce.NonNull(var.Name), !global) != null) {
- Error(var, "more than one declaration of variable name: {0}", var.Name);
- } else {
+ var previous = FindVariable(cce.NonNull(var.Name), !global);
+ if (previous == null) {
varContext.VarSymbols.Add(var.Name, var);
+ } else {
+ var r = (Variable)SelectNonExtern(var, previous);
+ if (r == null) {
+ Error(var, "more than one declaration of variable name: {0}", var.Name);
+ } else {
+ varContext.VarSymbols[var.Name] = r;
+ }
}
}
@@ -417,11 +357,47 @@ Contract.Requires(name != null); public void AddProcedure(DeclWithFormals proc) {
Contract.Requires(proc != null);
- if (funcdures[cce.NonNull(proc.Name)] != null) {
- Error(proc, "more than one declaration of function/procedure name: {0}", proc.Name);
+ Contract.Requires(proc.Name != null);
+
+ string name = proc.Name;
+ var previous = (DeclWithFormals)funcdures[name];
+ if (previous == null) {
+ funcdures.Add(name, proc);
+ } else {
+ var r = (DeclWithFormals)SelectNonExtern(proc, previous);
+ if (r == null) {
+ Error(proc, "more than one declaration of function/procedure name: {0}", name);
+ } else {
+ funcdures[name] = r;
+ }
+ }
+ }
+
+ /// <summary>
+ /// If both "a" and "b" have an ":extern" attribute, returns either one.
+ /// If one of "a" and "b" has an ":extern" attribute, returns that one.
+ /// If neither of "a" and "b" has an ":extern" attribute, returns null.
+ /// If a non-value value is returned, this method also adds the ":ignore"
+ /// attribute to the declaration NOT returned.
+ /// </summary>
+ Declaration SelectNonExtern(Declaration a, Declaration b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ Contract.Ensures(Contract.Result<Declaration>() == null || Contract.Result<Declaration>() == a || Contract.Result<Declaration>() == b);
+
+ Declaration ignore, keep;
+ if (QKeyValue.FindBoolAttribute(a.Attributes, "extern")) {
+ ignore = a;
+ keep = b;
+ } else if (QKeyValue.FindBoolAttribute(b.Attributes, "extern")) {
+ ignore = b;
+ keep = a;
} else {
- funcdures.Add(proc.Name, proc);
+ return null;
}
+ // prepend :ignore attribute
+ ignore.Attributes = new QKeyValue(ignore.tok, "ignore", new List<object/*!*/>(), ignore.Attributes);
+ return keep;
}
/// <summary>
diff --git a/Test/test0/Answer b/Test/test0/Answer index 0441b69b..d434a8ca 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -247,3 +247,16 @@ BadQuantifier.bpl(3,15): error: invalid QuantifierBody EmptyCallArgs.bpl(31,2): Error: type variable must occur in types of given arguments: a
EmptyCallArgs.bpl(32,2): Error: type variable must occur in types of given arguments: a
2 name resolution errors detected in EmptyCallArgs.bpl
+----- SeparateVerification0.bpl
+SeparateVerification0.bpl(13,6): Error: undeclared identifier: y
+1 name resolution errors detected in SeparateVerification0.bpl
+----- SeparateVerification1.bpl SeparateVerification0.bpl
+SeparateVerification1.bpl(4,6): Error: undeclared identifier: x
+SeparateVerification0.bpl(10,6): Error: undeclared identifier: x
+2 name resolution errors detected in SeparateVerification0.bpl
+----- SeparateVerification0.bpl SeparateVerification0.bpl
+
+Boogie program verifier finished with 0 verified, 0 errors
+----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl new file mode 100644 index 00000000..5a8ef283 --- /dev/null +++ b/Test/test0/SeparateVerification0.bpl @@ -0,0 +1,21 @@ +// need to include this file twice for it to include all necessary declarations
+
+#if FILE_0
+const x: int;
+#else
+const y: int;
+#endif
+
+#if FILE_1
+axiom x == 12;
+procedure Q();
+#else
+axiom y == 7;
+#endif
+
+// duplicates of :extern's are fine (Boogie keeps the non-:extern or chooses arbitrarily among the :extern's)
+type {:extern} T;
+const {:extern} C: int;
+function {:extern} F(): int;
+var {:extern} n: int;
+procedure {:extern} P(inconsistentParameterButThatIsOkayBecauseTheExternIsIgnored: int);
diff --git a/Test/test0/SeparateVerification1.bpl b/Test/test0/SeparateVerification1.bpl new file mode 100644 index 00000000..0e3e7926 --- /dev/null +++ b/Test/test0/SeparateVerification1.bpl @@ -0,0 +1,19 @@ +// to be used with SeparateVerification0.bpl
+
+// x and y are declared in SeparateVerification0.bpl
+axiom x + y <= 100;
+
+// these are declared as :extern as SeparateVerification0.bpl
+type T;
+const C: int;
+function F(): int;
+var n: int;
+procedure P();
+procedure {:extern} Q(x: int);
+
+procedure Main() {
+ call P(); // note, calling the parameter-less non-extern P (an extern and a non-extern
+ // declaration of the same name are usually mostly identical declarations,
+ // but Boogie allows them to be different, because it ignores the extern ones)
+ call Q(); // ditto
+}
diff --git a/Test/test0/runtest.bat b/Test/test0/runtest.bat index c7c6ee3d..5ecc22dc 100644 --- a/Test/test0/runtest.bat +++ b/Test/test0/runtest.bat @@ -31,3 +31,12 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify Orderings.bpl
%BGEXE% %* /noVerify BadQuantifier.bpl
%BGEXE% %* /noVerify EmptyCallArgs.bpl
+
+echo ----- SeparateVerification0.bpl
+%BGEXE% %* /noVerify SeparateVerification0.bpl
+echo ----- SeparateVerification1.bpl SeparateVerification0.bpl
+%BGEXE% %* /noVerify SeparateVerification1.bpl SeparateVerification0.bpl
+echo ----- SeparateVerification0.bpl SeparateVerification0.bpl
+%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl
+echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
+%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
|