diff options
author | qadeer <unknown> | 2014-11-08 09:50:33 -0800 |
---|---|---|
committer | qadeer <unknown> | 2014-11-08 09:50:33 -0800 |
commit | 10bc14d4b152db1d98d989d629563a244b6e4272 (patch) | |
tree | 788eea73c3b9499317d8622340cbcaadebca1c75 /Source/Houdini | |
parent | b96b3c7c9d8aa4a22e5d90a760e0c4c95e6e042c (diff) |
changed the suffix of the trace file from .bpl to .txt to avoid confusing the lit tool
Diffstat (limited to 'Source/Houdini')
-rw-r--r-- | Source/Houdini/ConcurrentHoudini.cs | 190 | ||||
-rw-r--r-- | Source/Houdini/Houdini.cs | 2 | ||||
-rw-r--r-- | Source/Houdini/StagedHoudini.cs | 2 |
3 files changed, 97 insertions, 97 deletions
diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs index 5c0f217f..bfc7cbc1 100644 --- a/Source/Houdini/ConcurrentHoudini.cs +++ b/Source/Houdini/ConcurrentHoudini.cs @@ -1,90 +1,90 @@ -using System; -using System.IO; -using System.Collections.Generic; -using System.Collections.Concurrent; -using System.Diagnostics; -using System.Diagnostics.Contracts; -using System.Text.RegularExpressions; -using System.Linq; -using VC; - -namespace Microsoft.Boogie.Houdini -{ - public class ConcurrentHoudini : Houdini - { - - protected int taskID; - - private static ConcurrentDictionary<string, RefutedAnnotation> refutedSharedAnnotations; - - public static ConcurrentDictionary<string, RefutedAnnotation> RefutedSharedAnnotations { get { return refutedSharedAnnotations; } } - - public ConcurrentHoudini(int taskId, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") { - Contract.Assert(taskId >= 0); - this.program = program; - this.cexTraceFile = cexTraceFile; - this.taskID = taskId; - Initialize(program, stats); - } - - static ConcurrentHoudini() - { - refutedSharedAnnotations = new ConcurrentDictionary<string, RefutedAnnotation>(); - } - - protected override bool ExchangeRefutedAnnotations() - { - 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); - - if (kv.Key != null) { - RefutedAnnotation ra = null; - Implementation refutationSite = null; - - foreach (var r in program.Implementations) { - 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.Procedures) { - 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); - - AddRelatedToWorkList(ra); - UpdateAssignment(ra); - count++; - } - } - - return count > 0 ? true : false; - } - - protected override void ShareRefutedAnnotation(RefutedAnnotation refutedAnnotation) { - refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation); - } +using System;
+using System.IO;
+using System.Collections.Generic;
+using System.Collections.Concurrent;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using System.Text.RegularExpressions;
+using System.Linq;
+using VC;
+
+namespace Microsoft.Boogie.Houdini
+{
+ public class ConcurrentHoudini : Houdini
+ {
+
+ protected int taskID;
+
+ private static ConcurrentDictionary<string, RefutedAnnotation> refutedSharedAnnotations;
+
+ public static ConcurrentDictionary<string, RefutedAnnotation> RefutedSharedAnnotations { get { return refutedSharedAnnotations; } }
+
+ public ConcurrentHoudini(int taskId, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.txt") {
+ Contract.Assert(taskId >= 0);
+ this.program = program;
+ this.cexTraceFile = cexTraceFile;
+ this.taskID = taskId;
+ Initialize(program, stats);
+ }
+
+ static ConcurrentHoudini()
+ {
+ refutedSharedAnnotations = new ConcurrentDictionary<string, RefutedAnnotation>();
+ }
+
+ protected override bool ExchangeRefutedAnnotations()
+ {
+ 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);
+
+ if (kv.Key != null) {
+ RefutedAnnotation ra = null;
+ Implementation refutationSite = null;
+
+ foreach (var r in program.Implementations) {
+ 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.Procedures) {
+ 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);
+
+ AddRelatedToWorkList(ra);
+ UpdateAssignment(ra);
+ count++;
+ }
+ }
+
+ return count > 0 ? true : false;
+ }
+
+ protected override void ShareRefutedAnnotation(RefutedAnnotation refutedAnnotation) {
+ refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation);
+ }
protected override void ApplyRefutedSharedAnnotations() {
if (refutedSharedAnnotations.Count > 0) {
@@ -94,11 +94,11 @@ namespace Microsoft.Boogie.Houdini }
}
}
- } - - protected override int GetTaskID() { - return taskID; - } - - } -} + }
+
+ protected override int GetTaskID() {
+ return taskID;
+ }
+
+ }
+}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 74cf0d26..fef24688 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -276,7 +276,7 @@ namespace Microsoft.Boogie.Houdini { protected Houdini() { }
- public Houdini(Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") {
+ public Houdini(Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.txt") {
this.program = program;
this.cexTraceFile = cexTraceFile;
Initialize(program, stats);
diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs index a3b02250..56d4a07a 100644 --- a/Source/Houdini/StagedHoudini.cs +++ b/Source/Houdini/StagedHoudini.cs @@ -108,7 +108,7 @@ namespace Microsoft.Boogie.Houdini if (h.Count() == 0)
{
- h.Add(new Houdini(ProgramFromFile(tempFilename), new HoudiniSession.HoudiniStatistics(), "houdiniCexTrace_" + s.GetId() + ".bpl"));
+ h.Add(new Houdini(ProgramFromFile(tempFilename), new HoudiniSession.HoudiniStatistics(), "houdiniCexTrace_" + s.GetId() + ".txt"));
}
System.Diagnostics.Debug.Assert(h.Count() == 1);
|