From eea0a9e74d6782d08f8dd01c0e1dbec15f1a02cb Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 19:12:40 +0100 Subject: More refactoring --- Source/Houdini/AbstractHoudini.cs | 2 +- Source/Houdini/Houdini.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'Source/Houdini') diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index ceef059e..321d4072 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -82,7 +82,7 @@ namespace Microsoft.Boogie.Houdini { // type check existentialFunctions.Values.Iter(func => { - if (func.OutParams.Length != 1 || !func.OutParams[0].TypedIdent.Type.IsBool) + if (func.OutParams.Count != 1 || !func.OutParams[0].TypedIdent.Type.IsBool) throw new AbsHoudiniInternalError(string.Format("Existential function {0} must return bool", func.Name)); if(func.Body != null) throw new AbsHoudiniInternalError(string.Format("Existential function {0} should not have a body", func.Name)); diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index f896c27f..b4408f03 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -265,7 +265,7 @@ namespace Microsoft.Boogie.Houdini { } private CmdSeq InlineRequiresForCallCmd(CallCmd node) { Dictionary substMap = new Dictionary(); - for (int i = 0; i < node.Proc.InParams.Length; i++) { + for (int i = 0; i < node.Proc.InParams.Count; i++) { substMap.Add(node.Proc.InParams[i], node.Ins[i]); } Substitution substitution = Substituter.SubstitutionFromHashtable(substMap); -- cgit v1.2.3