diff options
| author |  Ally Donaldson <unknown> | 2013-07-22 19:12:40 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-07-22 19:12:40 +0100 |
| commit | eea0a9e74d6782d08f8dd01c0e1dbec15f1a02cb (patch) | |
| tree | 26b5693006a283d80fb47507263e404c282ae2ef /Source/VCGeneration | |
| parent | 62d2fa72d5e1816d6cb1239063302808424c6d13 (diff) | |
More refactoring
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index fe8d67f5..01366633 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -938,8 +938,8 @@ namespace VC { }
// where clauses of out-parameters
- Contract.Assert(impl.OutParams.Length == impl.Proc.OutParams.Length);
- for (int i = 0; i < impl.OutParams.Length; i++) {
+ Contract.Assert(impl.OutParams.Count == impl.Proc.OutParams.Count);
+ for (int i = 0; i < impl.OutParams.Count; i++) {
Variable f = cce.NonNull(impl.Proc.OutParams[i]);
if (f.TypedIdent.WhereExpr != null) {
Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr);
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index ac7ee9be..b4080e2c 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -643,7 +643,7 @@ namespace Microsoft.Boogie var proc = decl as Procedure;
if (proc == null) continue;
if (!proc.Name.StartsWith(recordProcName)) continue;
- Contract.Assert(proc.InParams.Length == 1);
+ Contract.Assert(proc.InParams.Count == 1);
// Make a new function
TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index c5d88c5c..5848e63b 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -326,7 +326,7 @@ namespace VC { var proc = decl as Procedure;
if (proc == null) continue;
if (!proc.Name.StartsWith(recordProcName)) continue;
- Contract.Assert(proc.InParams.Length == 1);
+ Contract.Assert(proc.InParams.Count == 1);
// Make a new function
TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 873a5589..eff8c2e2 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1240,7 +1240,7 @@ namespace VC { VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
- if (vcgen.CurrentLocalVariables.Length != 0)
+ if (vcgen.CurrentLocalVariables.Count != 0)
{
Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;
List<VCExprVar> boundVars = new List<VCExprVar>();
|