summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Pantazis Deligiannis <pdeligia@me.com>2013-10-06 16:38:52 +0100
committerGravatar Pantazis Deligiannis <pdeligia@me.com>2013-10-06 16:38:52 +0100
commite3e9aff76e22d05cdb3c558c8106d4a201aa0141 (patch)
tree4748d842595bb7ea8e27dba76d9dff4a548ec934 /Source
parent3297f35c08738cd95bd01c1f4ab1e8baadddf67e (diff)
fixed bug with the exchange refuted invariants process
Diffstat (limited to 'Source')
-rw-r--r--Source/Houdini/ConcurrentHoudini.cs36
-rw-r--r--Source/Houdini/Houdini.cs2
2 files changed, 33 insertions, 5 deletions
diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
index 687dfb78..b16370e9 100644
--- a/Source/Houdini/ConcurrentHoudini.cs
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -86,11 +86,40 @@ namespace Microsoft.Boogie.Houdini
{
int count = 0;
+ if (CommandLineOptions.Clo.DebugConcurrentHoudini)
+ Console.WriteLine("# number of shared refuted annotations: " + refutedSharedAnnotations.Count);
+
foreach (string key in refutedSharedAnnotations.Keys) {
KeyValuePair<Variable, bool> kv = currentHoudiniState.Assignment.FirstOrDefault(entry => entry.Key.Name.Equals(key) && entry.Value);
- RefutedAnnotation ra = refutedSharedAnnotations[key];
if (kv.Key != null) {
+ RefutedAnnotation ra = null;
+ Implementation refutationSite = null;
+
+ foreach (var r in program.TopLevelDeclarations.OfType<Implementation>()) {
+ if (r.Name.Equals(refutedSharedAnnotations[key].RefutationSite.Name)) {
+ refutationSite = r;
+ break;
+ }
+ }
+ Debug.Assert(refutationSite != null);
+
+ if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.REQUIRES) {
+ Procedure proc = null;
+ foreach (var p in program.TopLevelDeclarations.OfType<Procedure>()) {
+ if (p.Name.Equals(refutedSharedAnnotations[key].CalleeProc.Name)) {
+ proc = p;
+ break;
+ }
+ }
+ Debug.Assert(proc != null);
+ ra = RefutedAnnotation.BuildRefutedRequires(kv.Key, proc, refutationSite);
+ } else if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.ENSURES)
+ ra = RefutedAnnotation.BuildRefutedEnsures(kv.Key, refutationSite);
+ else if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.ASSERT)
+ ra = RefutedAnnotation.BuildRefutedAssert(kv.Key, refutationSite);
+ Debug.Assert(ra != null);
+
if (CommandLineOptions.Clo.DebugConcurrentHoudini)
Console.WriteLine("(+) " + ra.Constant + "," + ra.Kind + "," + ra.CalleeProc + "," + ra.RefutationSite);
@@ -121,7 +150,7 @@ namespace Microsoft.Boogie.Houdini
RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
// some candidate annotation removed
if (refutedAnnotation != null) {
- refutedSharedAnnotations.TryAdd (refutedAnnotation.Constant.Name, refutedAnnotation);
+ refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation);
AddRelatedToWorkList(refutedAnnotation);
UpdateAssignment(refutedAnnotation);
dequeue = false;
@@ -142,9 +171,6 @@ namespace Microsoft.Boogie.Houdini
}
}
- if (CommandLineOptions.Clo.DebugConcurrentHoudini)
- Console.WriteLine("# number of shared refuted annotations: " + refutedSharedAnnotations.Count);
-
if (ExchangeRefutedAnnotations()) dequeue = false;
break;
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index c3575800..4b533e5b 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -712,6 +712,8 @@ namespace Microsoft.Boogie.Houdini {
}
protected void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) {
+ if (refutedAnnotation == null) Console.WriteLine("TEEEEEST!!!");
+
Contract.Assume(currentHoudiniState.Implementation != null);
foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, refutedAnnotation.RefutationSite)) {
if (!currentHoudiniState.isBlackListed(implementation.Name)) {