diff options
Diffstat (limited to 'Source/Houdini')
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 4 | ||||
| -rw-r--r-- | Source/Houdini/CandidateDependenceAnalyser.cs | 4 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 4 |
3 files changed, 6 insertions, 6 deletions
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 157571f3..2ff5975e 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -2238,7 +2238,7 @@ namespace Microsoft.Boogie.Houdini { foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())
{
- var nensures = new EnsuresSeq();
+ var nensures = new List<Ensures>();
proc.Ensures.OfType<Ensures>()
.Where(ens => !QKeyValue.FindBoolAttribute(ens.Attributes, "ah") &&
!QKeyValue.FindBoolAttribute(ens.Attributes, "pre") &&
@@ -3147,7 +3147,7 @@ namespace Microsoft.Boogie.Houdini { PosPrePreds[impl.Name].UnionWith(posPreT);
// Pick up per-procedure pre-post
- var nens = new EnsuresSeq();
+ var nens = new List<Ensures>();
foreach (var ens in impl.Proc.Ensures.OfType<Ensures>())
{
string s = null;
diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 9a2eb404..0f725ccf 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -437,7 +437,7 @@ namespace Microsoft.Boogie.Houdini { {
#region Handle the preconditions
- RequiresSeq newRequires = new RequiresSeq();
+ List<Requires> newRequires = new List<Requires>();
foreach(Requires r in p.Requires) {
string c;
if (Houdini.MatchCandidate(r.Condition, candidates, out c)) {
@@ -457,7 +457,7 @@ namespace Microsoft.Boogie.Houdini { #endregion
#region Handle the postconditions
- EnsuresSeq newEnsures = new EnsuresSeq();
+ List<Ensures> newEnsures = new List<Ensures>();
foreach(Ensures e in p.Ensures) {
string c;
if (Houdini.MatchCandidate(e.Condition, candidates, out c)) {
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 06d606ff..5078d5a5 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -1165,7 +1165,7 @@ namespace Microsoft.Boogie.Houdini { }
foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {
- RequiresSeq newRequires = new RequiresSeq();
+ List<Requires> newRequires = new List<Requires>();
foreach (Requires r in proc.Requires) {
string c;
if (MatchCandidate(r.Condition, out c)) {
@@ -1185,7 +1185,7 @@ namespace Microsoft.Boogie.Houdini { }
proc.Requires = newRequires;
- EnsuresSeq newEnsures = new EnsuresSeq();
+ List<Ensures> newEnsures = new List<Ensures>();
foreach (Ensures e in proc.Ensures) {
string c;
if (MatchCandidate(e.Condition, out c)) {
|