summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-08-04 21:52:41 +0000
committerGravatar tabarbe <unknown>2010-08-04 21:52:41 +0000
commit471bfd72d5c49ae66f0c64504e5eacc006f083f1 (patch)
tree363aa99233d98483f7d7175eaa751795e9c8ba54 /Source
parent043bb35883b8b71dfb8a70c3d9abe6a79a6ed212 (diff)
Boogie: Removed trailing spaces in code
Diffstat (limited to 'Source')
-rw-r--r--Source/AIFramework/CommonFunctionSymbols.ssc4
-rw-r--r--Source/AIFramework/Functional.ssc8
-rw-r--r--Source/AIFramework/MultiLattice.ssc4
-rw-r--r--Source/AIFramework/Mutable.ssc4
-rw-r--r--Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc2
-rw-r--r--Source/AIFramework/VariableMap/ConstantAbstraction.ssc4
-rw-r--r--Source/AIFramework/VariableMap/ConstantExpressions.ssc18
-rw-r--r--Source/AIFramework/VariableMap/Intervals.ssc24
-rw-r--r--Source/AIFramework/VariableMap/VariableMapLattice.ssc16
-rw-r--r--Source/AbsInt/AbstractInterpretation.cs14
-rw-r--r--Source/AbsInt/Traverse.cs2
-rw-r--r--Source/Basetypes/BigNum.ssc2
-rw-r--r--Source/Core/Absy.ssc4
-rw-r--r--Source/Core/AbsyCmd.ssc2
-rw-r--r--Source/Core/AbsyExpr.ssc14
-rw-r--r--Source/Core/AbsyType.ssc8
-rw-r--r--Source/Core/CommandLineOptions.ssc24
-rw-r--r--Source/Core/DeadVarElim.ssc12
-rw-r--r--Source/Core/Duplicator.ssc4
-rw-r--r--Source/Core/GraphAlgorithms.ssc2
-rw-r--r--Source/Core/Inline.ssc18
-rw-r--r--Source/Core/Parser.ssc440
-rw-r--r--Source/Core/PureCollections.ssc106
-rw-r--r--Source/Core/Scanner.ssc72
-rw-r--r--Source/Core/StandardVisitor.ssc108
-rw-r--r--Source/Core/TypeAmbiguitySeeker.ssc2
-rw-r--r--Source/Core/Xml.ssc8
-rw-r--r--Source/Graph/Graph.ssc2
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs6
-rw-r--r--Source/Provers/Simplify/Prover.cs2
-rw-r--r--Source/Provers/Z3/Inspector.cs2
-rw-r--r--Source/Provers/Z3/Prover.cs4
-rw-r--r--Source/Provers/Z3/ProverInterface.cs2
-rw-r--r--Source/Provers/Z3/TypeDeclCollector.cs2
-rw-r--r--Source/VCExpr/Boogie2VCExpr.ssc10
-rw-r--r--Source/VCExpr/Clustering.ssc4
-rw-r--r--Source/VCExpr/SimplifyLikeLineariser.ssc6
-rw-r--r--Source/VCExpr/TypeErasure.ssc14
-rw-r--r--Source/VCExpr/TypeErasureArguments.ssc2
-rw-r--r--Source/VCExpr/TypeErasurePremisses.ssc8
-rw-r--r--Source/VCExpr/VCExprAST.ssc4
-rw-r--r--Source/VCExpr/VCExprASTVisitors.ssc2
-rw-r--r--Source/VCGeneration/Check.cs6
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs2
-rw-r--r--Source/VCGeneration/Context.cs2
-rw-r--r--Source/VCGeneration/DoomCheck.cs78
-rw-r--r--Source/VCGeneration/DoomErrorHandler.cs4
-rw-r--r--Source/VCGeneration/VC.cs14
-rw-r--r--Source/VCGeneration/VCDoomed.cs22
49 files changed, 562 insertions, 562 deletions
diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc
index e05e8dac..bc59df97 100644
--- a/Source/AIFramework/CommonFunctionSymbols.ssc
+++ b/Source/AIFramework/CommonFunctionSymbols.ssc
@@ -441,7 +441,7 @@ namespace Microsoft.AbstractInterpretationFramework
private static readonly AIType! heaptype = new Heap();
public static AIType! Type { get { return heaptype; } }
- // the types in the following, select1, select2, are hard-coded;
+ // the types in the following, select1, select2, are hard-coded;
// these types may not always be appropriate
private static readonly FunctionSymbol! _select1 = new FunctionSymbol("sel1",
// Heap x FieldName -> Prop
@@ -455,7 +455,7 @@ namespace Microsoft.AbstractInterpretationFramework
);
public static FunctionSymbol! Select2 { get { return _select2; } }
- // the types in the following, store1, store2, are hard-coded;
+ // the types in the following, store1, store2, are hard-coded;
// these types may not always be appropriate
private static readonly FunctionSymbol! _update1 = new FunctionSymbol("upd1",
// Heap x FieldName x Value -> Heap
diff --git a/Source/AIFramework/Functional.ssc b/Source/AIFramework/Functional.ssc
index 1413230e..bee40031 100644
--- a/Source/AIFramework/Functional.ssc
+++ b/Source/AIFramework/Functional.ssc
@@ -102,7 +102,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
assume r != null;
assert this.Contains(key); // The entry must be defined
- r[key] = value;
+ r[key] = value;
return new FunctionalHashtable(r);
}
@@ -195,7 +195,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
public override int GetHashCode()
{
int h = this.first == null ? 0 : this.first.GetHashCode();
- h ^= this.second == null ? 0 : this.second.GetHashCode();
+ h ^= this.second == null ? 0 : this.second.GetHashCode();
return h;
}
}
@@ -232,7 +232,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections.Generic
public override int GetHashCode()
{
int h = this.first == null ? 0 : this.first.GetHashCode();
- h ^= this.second == null ? 0 : this.second.GetHashCode();
+ h ^= this.second == null ? 0 : this.second.GetHashCode();
return h;
}
@@ -271,7 +271,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections.Generic
public override int GetHashCode()
{
int h = this.first == null ? 0 : this.first.GetHashCode();
- h ^= this.second == null ? 0 : this.second.GetHashCode();
+ h ^= this.second == null ? 0 : this.second.GetHashCode();
h ^= this.third == null ? 0 : this.third.GetHashCode();
return h;
}
diff --git a/Source/AIFramework/MultiLattice.ssc b/Source/AIFramework/MultiLattice.ssc
index 761f4c7e..514e2548 100644
--- a/Source/AIFramework/MultiLattice.ssc
+++ b/Source/AIFramework/MultiLattice.ssc
@@ -11,7 +11,7 @@ namespace Microsoft.AbstractInterpretationFramework
using System.Diagnostics;
using Microsoft.AbstractInterpretationFramework.Collections;
- using Microsoft.Boogie;
+ using Microsoft.Boogie;
using ISet = Microsoft.Boogie.Set;
@@ -39,7 +39,7 @@ namespace Microsoft.AbstractInterpretationFramework
{
newEPL[i] = (Element) ((!)otherEPL[i]).Clone();
}
- this.elementPerLattice = newEPL;
+ this.elementPerLattice = newEPL;
}
}
diff --git a/Source/AIFramework/Mutable.ssc b/Source/AIFramework/Mutable.ssc
index 36bb3647..6b5e0a20 100644
--- a/Source/AIFramework/Mutable.ssc
+++ b/Source/AIFramework/Mutable.ssc
@@ -5,7 +5,7 @@
//-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework.Collections
{
- using System.Collections;
+ using System.Collections;
using Microsoft.Contracts;
/// <summary>
@@ -52,7 +52,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
// ICollection members
public void CopyTo (System.Array! a, int i) {
if (this.Count > a.Length - i) throw new System.ArgumentException();
- int j = i;
+ int j = i;
foreach(object o in this){
a.SetValue(o, j++);
}
diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
index a99a4ee8..e444b0ca 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
+++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
@@ -717,7 +717,7 @@ namespace Microsoft.AbstractInterpretationFramework
CHECK_NEXT_CONSTRAINT: {}
#if DEBUG_PRINT
- Console.WriteLine("Widen checking: done with that constraint");
+ Console.WriteLine("Widen checking: done with that constraint");
#endif
}
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
index 97fb57ce..8ba3065f 100644
--- a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
+++ b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
@@ -67,13 +67,13 @@ namespace Microsoft.AbstractInterpretationFramework
public override bool IsTop (Element! element)
{
Elt e = (Elt)element;
- return e.domainValue == Value.Top;
+ return e.domainValue == Value.Top;
}
public override bool IsBottom (Element! element)
{
Elt e = (Elt)element;
- return e.domainValue == Value.Bottom;
+ return e.domainValue == Value.Bottom;
}
public override Element! NontrivialJoin (Element! first, Element! second)
diff --git a/Source/AIFramework/VariableMap/ConstantExpressions.ssc b/Source/AIFramework/VariableMap/ConstantExpressions.ssc
index 306c4e8f..fcf49b25 100644
--- a/Source/AIFramework/VariableMap/ConstantExpressions.ssc
+++ b/Source/AIFramework/VariableMap/ConstantExpressions.ssc
@@ -82,7 +82,7 @@ namespace Microsoft.AbstractInterpretationFramework
get
{
assert (this.variableBindings == null) <==> (this.variableDependences == null);
- return this.variableBindings == null && this.variableDependences == null;
+ return this.variableBindings == null && this.variableDependences == null;
}
}
@@ -91,7 +91,7 @@ namespace Microsoft.AbstractInterpretationFramework
/// </summary>
public static AbstractElement! Join(AbstractElement! left, AbstractElement! right)
{
- AbstractElement! result = new AbstractElement();
+ AbstractElement! result = new AbstractElement();
// Put all the variables in the left
foreach(IVariable! var in left.variableBindings.Keys)
@@ -103,7 +103,7 @@ namespace Microsoft.AbstractInterpretationFramework
if(rightVal== null) // the expression is not there
{
- result.variableBindings.Add(var, leftVal);
+ result.variableBindings.Add(var, leftVal);
}
else // both abstract elements have a definition for the variable....
{
@@ -121,7 +121,7 @@ namespace Microsoft.AbstractInterpretationFramework
if(rightVal== null) // the expression is not there
{
- result.variableBindings.Add(var, rightVal);
+ result.variableBindings.Add(var, rightVal);
}
else // both abstract elements have a definition for the variable....
{
@@ -219,18 +219,18 @@ namespace Microsoft.AbstractInterpretationFramework
List<IVariable> depRight = right.variableDependences[var];
// Intersect the two sets
- result.variableDependences.Add(var, depLeft);
+ result.variableDependences.Add(var, depLeft);
foreach(IVariable v in depRight)
{
if(!result.variableDependences.ContainsKey(v))
{
- result.variableDependences.Remove(v);
+ result.variableDependences.Remove(v);
}
}
}
// Now we remove the dependencies with variables not in variableBindings
- List<IVariable>! varsToRemove = new List<IVariable>();
+ List<IVariable>! varsToRemove = new List<IVariable>();
foreach(IVariable var in result.
@@ -252,7 +252,7 @@ namespace Microsoft.AbstractInterpretationFramework
{
List<IVariable> dependingVars = this.variableDependences[var];
List<IVariable> clonedDependingVars = new List<IVariable>(dependingVars);
- cloned.variableDependences.Add(var, clonedDependingVars);
+ cloned.variableDependences.Add(var, clonedDependingVars);
}
}
@@ -268,7 +268,7 @@ namespace Microsoft.AbstractInterpretationFramework
public override string! ToString()
{
- string! retString = "";
+ string! retString = "";
retString += "Bindings";
foreach(IVariable var in this.variableBindings.Keys)
diff --git a/Source/AIFramework/VariableMap/Intervals.ssc b/Source/AIFramework/VariableMap/Intervals.ssc
index 7f6211ba..f507e020 100644
--- a/Source/AIFramework/VariableMap/Intervals.ssc
+++ b/Source/AIFramework/VariableMap/Intervals.ssc
@@ -57,7 +57,7 @@ namespace Microsoft.AbstractInterpretationFramework
{
IntervalElement interval = (IntervalElement) element;
- return interval.IsTop();
+ return interval.IsTop();
}
/// <summary>
@@ -67,7 +67,7 @@ namespace Microsoft.AbstractInterpretationFramework
{
IntervalElement interval = (IntervalElement) element;
- return interval.IsBottom();
+ return interval.IsBottom();
}
/// <summary>
@@ -83,7 +83,7 @@ namespace Microsoft.AbstractInterpretationFramework
IntervalElement! join = IntervalElement.Factory(inf, sup);
- return join;
+ return join;
}
/// <summary>
@@ -146,9 +146,9 @@ namespace Microsoft.AbstractInterpretationFramework
/// </summary>
public override IExpr! ToPredicate(IVariable! var, Element! element)
{
- IntervalElement! interval = (IntervalElement!) element;
+ IntervalElement! interval = (IntervalElement!) element;
IExpr lowerBound = null;
- IExpr upperBound = null;
+ IExpr upperBound = null;
if(! (interval.Inf is InfinitaryInt))
{
@@ -168,7 +168,7 @@ namespace Microsoft.AbstractInterpretationFramework
return lowerBound;
else
if(upperBound != null)
- return upperBound;
+ return upperBound;
else // If we reach this point, both lowerBound and upperBound are null, i.e. we have no bounds on var, so we return simply true...
return this.factory.True;
}
@@ -178,7 +178,7 @@ namespace Microsoft.AbstractInterpretationFramework
/// </summary>
public override bool Understands(IFunctionSymbol! f, IList /*<IExpr*/ ! args)
{
- return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
}
@@ -211,7 +211,7 @@ namespace Microsoft.AbstractInterpretationFramework
}
}
// otherwise we simply return Top
- return IntervalElement.Top;
+ return IntervalElement.Top;
}
/// <summary>
@@ -237,7 +237,7 @@ namespace Microsoft.AbstractInterpretationFramework
}
else if(exp is IFunApp)
{
- IFunApp fun = (IFunApp) exp;
+ IFunApp fun = (IFunApp) exp;
if(fun.FunctionSymbol is IntSymbol) // An integer
{
@@ -271,7 +271,7 @@ namespace Microsoft.AbstractInterpretationFramework
else if(fun.FunctionSymbol.Equals(Int.Div))
retVal = leftVal / rightVal;
else if(fun.FunctionSymbol.Equals(Int.Mod))
- retVal = leftVal % rightVal;
+ retVal = leftVal % rightVal;
}
}
@@ -385,7 +385,7 @@ namespace Microsoft.AbstractInterpretationFramework
ExtendedInt! inf = a.inf + b.inf;
ExtendedInt! sup = a.sup + b.sup;
- return Factory(inf, sup);
+ return Factory(inf, sup);
}
// Subtraction
@@ -394,7 +394,7 @@ namespace Microsoft.AbstractInterpretationFramework
ExtendedInt! inf = a.inf - b.sup;
ExtendedInt! sup = a.sup - b.inf;
- IntervalElement! sub = Factory(inf, sup);
+ IntervalElement! sub = Factory(inf, sup);
return sub;
}
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
index 34f876f5..c0293493 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
@@ -78,7 +78,7 @@ namespace Microsoft.AbstractInterpretationFramework
public bool IsBottom {
get {
- return this.constraints == null;
+ return this.constraints == null;
}
}
@@ -89,7 +89,7 @@ namespace Microsoft.AbstractInterpretationFramework
requires !this.IsBottom;
{
assume this.constraints != null;
- return (!) this.constraints.Keys;
+ return (!) this.constraints.Keys;
}
}
@@ -117,7 +117,7 @@ namespace Microsoft.AbstractInterpretationFramework
requires !this.IsBottom;
{
assume this.constraints != null;
- return (Element)constraints[key];
+ return (Element)constraints[key];
}
}
@@ -303,7 +303,7 @@ namespace Microsoft.AbstractInterpretationFramework
}
Elt! join = new Elt(newMap);
- // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
+ // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
return join;
}
@@ -368,9 +368,9 @@ namespace Microsoft.AbstractInterpretationFramework
}
Element! widen= new Elt(newMap);
- // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
+ // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
- return widen;
+ return widen;
}
internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)
@@ -482,7 +482,7 @@ namespace Microsoft.AbstractInterpretationFramework
else
{
IExpr! left = (IExpr!) fun.Arguments[0];
- IExpr! right = (IExpr!) fun.Arguments[1];
+ IExpr! right = (IExpr!) fun.Arguments[1];
if(!(left is IVariable || right is IVariable)) // At least one of the two operands must be a variable
return false;
@@ -493,7 +493,7 @@ namespace Microsoft.AbstractInterpretationFramework
|| fun.FunctionSymbol.Equals(Int.Mul)
|| fun.FunctionSymbol.Equals(Int.Div)
|| fun.FunctionSymbol.Equals(Int.Mod))
- return IsArithmeticExpr(left) && IsArithmeticExpr(right);
+ return IsArithmeticExpr(left) && IsArithmeticExpr(right);
else
return false;
}
diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs
index bf25434a..b1d16225 100644
--- a/Source/AbsInt/AbstractInterpretation.cs
+++ b/Source/AbsInt/AbstractInterpretation.cs
@@ -176,7 +176,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
foreach (Implementation impl in implementations)
{
impl.AbstractFunction = AbstractFunction.Empty.WithPair(this.lattice.Bottom, this.lattice.Bottom);
- this.implWorkItems.Enqueue(impl);
+ this.implWorkItems.Enqueue(impl);
}
while (this.implWorkItems.Count > 0) // until fixed point reached
@@ -554,7 +554,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
//PM: The following assertion follows from a nontrivial invariant of ArrayAssignCmd,
//PM: which we do not have yet. Therefore, we put in an assume fo now.
assume assmt.Index1 != null;
- assert assmt.Index1 != null;
+ assert assmt.Index1 != null;
// heap succession predicate
Expr heapsucc = Expr.HeapSucc(oldHeap, newHeap, assmt.Index0, assmt.Index1);
@@ -735,14 +735,14 @@ namespace Microsoft.Boogie.AbstractInterpretation {
lattice.ToPredicate(incomingValue).DoVisit(freeVarsVisitorForA);
lattice.ToPredicate(block.PreInvariant).DoVisit(freeVarsVisitorForB);
- List<AI.IVariable!>! freeVarsOfA = freeVarsVisitorForA.FreeVariables;
- List<AI.IVariable!>! freeVarsOfB = freeVarsVisitorForB.FreeVariables;
+ List<AI.IVariable!>! freeVarsOfA = freeVarsVisitorForA.FreeVariables;
+ List<AI.IVariable!>! freeVarsOfB = freeVarsVisitorForB.FreeVariables;
System.Console.WriteLine("@@ Compared for block {0}:", block.Label);
System.Console.WriteLine("@@ Incoming: {0}", lattice.ToPredicate((!) incomingValue));
- System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfA));
+ System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfA));
System.Console.WriteLine("@@ Previous: {0}", lattice.ToPredicate(block.PreInvariant));
- System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfB));
+ System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfB));
System.Console.WriteLine("@@ result = False");
System.Console.WriteLine("@@ end Compare");
string operation = "";
@@ -762,7 +762,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
#endif
// The default is to have have a widening that perform a (approximation of) the closure of the operands, so to improve the precision
- // block.PreInvariant = WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue);
+ // block.PreInvariant = WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue);
block.PreInvariant = (AI.Lattice.Element)lattice.Widen(block.PreInvariant, incomingValue);
}
block.iterations++;
diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs
index 2890730b..c4f226d9 100644
--- a/Source/AbsInt/Traverse.cs
+++ b/Source/AbsInt/Traverse.cs
@@ -72,7 +72,7 @@ namespace Microsoft.Boogie {
Contract.Assume(g.labelTargets != null);
cce.BeginExpose(g.labelTargets);
foreach (Block succ in g.labelTargets)
- // invariant b.currentlyTraversed;
+ // invariant b.currentlyTraversed;
//PM: The following loop invariant will work once properties are axiomatized
//&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);
{
diff --git a/Source/Basetypes/BigNum.ssc b/Source/Basetypes/BigNum.ssc
index b8ebcde0..33ecf672 100644
--- a/Source/Basetypes/BigNum.ssc
+++ b/Source/Basetypes/BigNum.ssc
@@ -140,7 +140,7 @@ namespace Microsoft.Basetypes {
}
}
- private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000);
+ private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000);
[Pure]
private string! toHex(string! format) {
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index 07723e4d..fbc2d253 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -881,7 +881,7 @@ namespace Microsoft.Boogie
p.Parent.Emit(stream);
}
if (ChildrenComplete)
- stream.Write(this, level, " complete");
+ stream.Write(this, level, " complete");
}
stream.WriteLine(";");
@@ -1119,7 +1119,7 @@ namespace Microsoft.Boogie
// Register all type parameters at the resolution context
protected void RegisterTypeParameters(ResolutionContext! rc) {
foreach (TypeVariable! v in TypeParameters)
- rc.AddTypeBinder(v);
+ rc.AddTypeBinder(v);
}
protected void SortTypeParams() {
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index d682029e..b24e83e3 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -1467,7 +1467,7 @@ namespace Microsoft.Boogie
int previousTypeBinderState = rc.TypeBinderState;
try {
foreach (TypeVariable! v in Proc.TypeParameters)
- rc.AddTypeBinder(v);
+ rc.AddTypeBinder(v);
Type.CheckBoundVariableOccurrences(Proc.TypeParameters,
formalInTypes, formalOutTypes,
this.tok, "types of given arguments",
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index 776ff8b3..5947c822 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -115,7 +115,7 @@ namespace Microsoft.Boogie
else { return Binary(BinaryOperator.Opcode.Or, e1, e2); }
}
public static Expr! Not (Expr! e1) {
- NAryExpr nary = e1 as NAryExpr;
+ NAryExpr nary = e1 as NAryExpr;
if (e1 == true_) { return false_; }
else if (e1 == false_) { return true_; }
@@ -480,7 +480,7 @@ namespace Microsoft.Boogie
public override bool Equals(object obj)
{
BvConst other = obj as BvConst;
- if (other == null) return false;
+ if (other == null) return false;
return Bits == other.Bits && Value == other.Value;
}
@@ -1375,8 +1375,8 @@ namespace Microsoft.Boogie
case Opcode.Imp: if (e1 is bool && e2 is bool) { return ! (bool)e1 || (bool)e2; } break;
case Opcode.Iff: if (e1 is bool && e2 is bool) { return e1 == e2; } break;
- case Opcode.Eq: return Equals(e1,e2);
- case Opcode.Neq: return ! Equals(e1,e2);
+ case Opcode.Eq: return Equals(e1,e2);
+ case Opcode.Neq: return ! Equals(e1,e2);
case Opcode.Subtype: throw new System.NotImplementedException();
}
@@ -1942,7 +1942,7 @@ namespace Microsoft.Boogie
return null;
}
- return ((!)args[0]).Type;
+ return ((!)args[0]).Type;
}
public Type Typecheck(ref ExprSeq! args,
@@ -2272,7 +2272,7 @@ namespace Microsoft.Boogie
}
public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)
{
- AI.IFunApp! retFun;
+ AI.IFunApp! retFun;
if(args.Count == 3)
{
@@ -2403,7 +2403,7 @@ namespace Microsoft.Boogie
}
public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)
{
- AI.IFunApp! retFun;
+ AI.IFunApp! retFun;
if(args.Count == 2)
{
diff --git a/Source/Core/AbsyType.ssc b/Source/Core/AbsyType.ssc
index c5f1309d..3d2ab73a 100644
--- a/Source/Core/AbsyType.ssc
+++ b/Source/Core/AbsyType.ssc
@@ -147,7 +147,7 @@ namespace Microsoft.Boogie
} catch (UnificationFailedException) {
return false;
}
- return true;
+ return true;
}
public abstract void Unify(Type! that,
@@ -508,7 +508,7 @@ namespace Microsoft.Boogie
// we only allow type parameters to be substituted
assert forall{TypeVariable! var in subst.Keys; typeParams.Has(var)};
- return subst;
+ return subst;
}
#else
/// <summary>
@@ -785,7 +785,7 @@ namespace Microsoft.Boogie
public BvType(int bits)
: base(Token.NoToken)
{
- Bits = bits;
+ Bits = bits;
}
//----------- Cloning ----------------------------------
@@ -2051,7 +2051,7 @@ namespace Microsoft.Boogie
: base(token) {
this.Decl = decl;
this.Arguments = arguments;
- this.ExpandedType = expandedType;
+ this.ExpandedType = expandedType;
}
//----------- Cloning ----------------------------------
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 70de931f..9fb05d24 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -157,7 +157,7 @@ namespace Microsoft.Boogie
public bool UseArrayTheory = false;
public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
- public bool DoModSetAnalysis = false;
+ public bool DoModSetAnalysis = false;
public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation
public int /*0..9*/StepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator
invariant 0 <= StepsBeforeWidening && StepsBeforeWidening <= 9;
@@ -181,7 +181,7 @@ namespace Microsoft.Boogie
public int SmokeTimeout = 10; // default to 10s
public int ProverCCLimit = 5;
public bool z3AtFlag = true;
- public bool RestartProverPerVC = false;
+ public bool RestartProverPerVC = false;
public double VcsMaxCost = 1.0;
public double VcsPathJoinMult = 0.8;
@@ -325,7 +325,7 @@ namespace Microsoft.Boogie
int res = 1; // the result value
while (ps.i < args.Length)
- invariant ps.IsPeerConsistent;
+ invariant ps.IsPeerConsistent;
invariant ps.args == args;
{
ps.s = args[ps.i];
@@ -518,7 +518,7 @@ namespace Microsoft.Boogie
{
XmlSinkFilename = args[ps.i];
}
- break;
+ break;
case "-print":
case "/print":
@@ -761,7 +761,7 @@ namespace Microsoft.Boogie
PrintErrorModelFile = args[ps.i];
}
CEVPrint = true;
- break;
+ break;
case "-printModelToFile":
case "/printModelToFile":
@@ -769,7 +769,7 @@ namespace Microsoft.Boogie
{
PrintErrorModelFile = args[ps.i];
}
- break;
+ break;
case "-enhancedErrorMessages":
@@ -780,7 +780,7 @@ namespace Microsoft.Boogie
case "-forceBplErrors":
case "/forceBplErrors":
ForceBplErrors = true;
- break;
+ break;
case "-bv":
case "/bv":
@@ -961,10 +961,10 @@ namespace Microsoft.Boogie
switch (args[ps.i])
{
case "0":
- LazyInlining = 0;
+ LazyInlining = 0;
break;
case "1":
- LazyInlining = 1;
+ LazyInlining = 1;
break;
case "2":
LazyInlining = 2;
@@ -981,10 +981,10 @@ namespace Microsoft.Boogie
switch (args[ps.i])
{
case "0":
- StratifiedInlining = 0;
+ StratifiedInlining = 0;
break;
case "1":
- StratifiedInlining = 1;
+ StratifiedInlining = 1;
break;
default:
StratifiedInlining = Int32.Parse((!)args[ps.i]);
@@ -992,7 +992,7 @@ namespace Microsoft.Boogie
break;
}
}
- break;
+ break;
case "-typeEncoding":
case "/typeEncoding":
if (ps.ConfirmArgumentCount(1)) {
diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc
index 4e3a431f..1a5d0b30 100644
--- a/Source/Core/DeadVarElim.ssc
+++ b/Source/Core/DeadVarElim.ssc
@@ -146,7 +146,7 @@ namespace Microsoft.Boogie
insideOldExpr ++;
node.Expr = this.VisitExpr(node.Expr);
insideOldExpr --;
- return node;
+ return node;
}
public override Expr! VisitIdentifierExpr(IdentifierExpr! node) {
@@ -596,12 +596,12 @@ namespace Microsoft.Boogie
predEdges.Add(b, new Set<Block!>());
}
- nodes.Add(b);
+ nodes.Add(b);
}
private void addEdge(Block! src, Block! tgt) {
registerNode(src);
- registerNode(tgt);
+ registerNode(tgt);
succEdges[src].Add(tgt);
predEdges[tgt].Add(src);
@@ -975,7 +975,7 @@ namespace Microsoft.Boogie
// Continue with intra propagation
GenKillWeight! summary = getWeightCall((CallCmd!)cmd);
- prop = summary.getLiveVars(prop);
+ prop = summary.getLiveVars(prop);
} else {
LiveVariableAnalysis.Propagate(cmd, prop);
}
@@ -1156,7 +1156,7 @@ namespace Microsoft.Boogie
private static GenKillWeight! getWeightAfterCall(Cmd! cmd) {
if(weightCacheAfterCall.ContainsKey(cmd))
- return weightCacheAfterCall[cmd];
+ return weightCacheAfterCall[cmd];
Set<Variable!>! gen = new Set<Variable!>();
Set<Variable!>! kill = new Set<Variable!>();
@@ -1187,7 +1187,7 @@ namespace Microsoft.Boogie
private static GenKillWeight! getWeightBeforeCall(Cmd! cmd) {
assert (cmd is CallCmd);
if(weightCacheBeforeCall.ContainsKey(cmd))
- return weightCacheBeforeCall[cmd];
+ return weightCacheBeforeCall[cmd];
Set<Variable!>! gen = new Set<Variable!>();
Set<Variable!>! kill = new Set<Variable!>();
diff --git a/Source/Core/Duplicator.ssc b/Source/Core/Duplicator.ssc
index 3fde1bf2..667eaf5e 100644
--- a/Source/Core/Duplicator.ssc
+++ b/Source/Core/Duplicator.ssc
@@ -245,11 +245,11 @@ namespace Microsoft.Boogie
}
public override Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
{
- return base.VisitAssertRequiresCmd((AssertRequiresCmd)node.Clone());
+ return base.VisitAssertRequiresCmd((AssertRequiresCmd)node.Clone());
}
public override Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
{
- return base.VisitAssertEnsuresCmd((AssertEnsuresCmd)node.Clone());
+ return base.VisitAssertEnsuresCmd((AssertEnsuresCmd)node.Clone());
}
public override Ensures! VisitEnsures(Ensures! node)
{
diff --git a/Source/Core/GraphAlgorithms.ssc b/Source/Core/GraphAlgorithms.ssc
index aac45d73..e1303316 100644
--- a/Source/Core/GraphAlgorithms.ssc
+++ b/Source/Core/GraphAlgorithms.ssc
@@ -156,7 +156,7 @@ namespace Microsoft.Boogie
foreach(ICollection<Node> component in this)
{
- string! tmp = System.String.Format("\nComponent #{0} = ", i++);
+ string! tmp = System.String.Format("\nComponent #{0} = ", i++);
outStr += tmp;
bool firstInRow = true;
diff --git a/Source/Core/Inline.ssc b/Source/Core/Inline.ssc
index 6dff13c3..0db27d6d 100644
--- a/Source/Core/Inline.ssc
+++ b/Source/Core/Inline.ssc
@@ -170,7 +170,7 @@ namespace Microsoft.Boogie {
List<Block!>! newBlocks = new List<Block!>();
foreach(Block block in blocks) {
- TransferCmd! transferCmd = (!) block.TransferCmd;
+ TransferCmd! transferCmd = (!) block.TransferCmd;
CmdSeq cmds = block.Cmds;
CmdSeq newCmds = new CmdSeq();
Block newBlock;
@@ -178,12 +178,12 @@ namespace Microsoft.Boogie {
int lblCount = 0;
for(int i = 0; i < cmds.Length; ++i) {
- Cmd cmd = cmds[i];
+ Cmd cmd = cmds[i];
CallCmd callCmd = cmd as CallCmd;
if(callCmd == null) {
// if not call command, leave it as is
- newCmds.Add(codeCopier.CopyCmd(cmd));
+ newCmds.Add(codeCopier.CopyCmd(cmd));
} else {
assert(callCmd.Proc != null);
Procedure proc = null;
@@ -242,7 +242,7 @@ namespace Microsoft.Boogie {
newBlocks.AddRange(inlinedBlocks);
lblCount = nextlblCount;
- newCmds = new CmdSeq();
+ newCmds = new CmdSeq();
} else if (inline == 0) {
inlinedSomething = true;
if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {
@@ -328,8 +328,8 @@ namespace Microsoft.Boogie {
}
}
- codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap);
- codeCopier.OldSubst = Substituter.SubstitutionFromHashtable(substMapOld);
+ codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap);
+ codeCopier.OldSubst = Substituter.SubstitutionFromHashtable(substMapOld);
}
protected void EndInline() {
@@ -374,7 +374,7 @@ namespace Microsoft.Boogie {
}
}
- VariableSeq locVars = (!)impl.OriginalLocVars;
+ VariableSeq locVars = (!)impl.OriginalLocVars;
// add where clauses of local vars as assume
for(int i = 0; i < locVars.Length; ++i) {
@@ -410,7 +410,7 @@ namespace Microsoft.Boogie {
GotoCmd inGotoCmd = new GotoCmd(callCmd.tok, new StringSeq(GetInlinedProcLabel(proc.Name) + "$" + startLabel));
Block inBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Entry", inCmds, inGotoCmd);
- inlinedBlocks.Add(inBlock);
+ inlinedBlocks.Add(inBlock);
// inject the blocks of the implementation
Block intBlock;
@@ -418,7 +418,7 @@ namespace Microsoft.Boogie {
CmdSeq copyCmds = codeCopier.CopyCmdSeq(block.Cmds);
TransferCmd transferCmd = CreateInlinedTransferCmd((!) block.TransferCmd, GetInlinedProcLabel(proc.Name));
intBlock = new Block(block.tok, GetInlinedProcLabel(proc.Name) + "$" + block.Label, copyCmds, transferCmd);
- inlinedBlocks.Add(intBlock);
+ inlinedBlocks.Add(intBlock);
}
// create out block
diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index 7ca3bd73..432c5ab2 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -241,7 +241,7 @@ private class BvBounds : Expr {
}
case 27: {
Axiom(out ax);
- Pgm.TopLevelDeclarations.Add(ax);
+ Pgm.TopLevelDeclarations.Add(ax);
break;
}
case 28: {
@@ -267,7 +267,7 @@ private class BvBounds : Expr {
}
case 31: {
Implementation(out nnim);
- Pgm.TopLevelDeclarations.Add(nnim);
+ Pgm.TopLevelDeclarations.Add(nnim);
break;
}
}
@@ -280,15 +280,15 @@ private class BvBounds : Expr {
ds = new VariableSeq();
bool u = false; QKeyValue kv = null;
bool ChildrenComplete = false;
- List<ConstantParent!> Parents = null;
+ List<ConstantParent!> Parents = null;
Expect(19);
- y = t;
+ y = t;
while (la.kind == 25) {
Attribute(ref kv);
}
if (la.kind == 20) {
Get();
- u = true;
+ u = true;
}
IdsType(out xs);
if (la.kind == 21) {
@@ -339,11 +339,11 @@ private class BvBounds : Expr {
Expect(8);
if (StartOf(2)) {
VarOrType(out tyd);
- arguments.Add(new Formal(tyd.tok, tyd, true));
+ arguments.Add(new Formal(tyd.tok, tyd, true));
while (la.kind == 11) {
Get();
VarOrType(out tyd);
- arguments.Add(new Formal(tyd.tok, tyd, true));
+ arguments.Add(new Formal(tyd.tok, tyd, true));
}
}
Expect(9);
@@ -352,16 +352,16 @@ private class BvBounds : Expr {
Expect(8);
VarOrType(out tyd);
Expect(9);
- retTyd = tyd;
+ retTyd = tyd;
} else if (la.kind == 10) {
Get();
Type(out retTy);
- retTyd = new TypedIdent(retTy.tok, "", retTy);
+ retTyd = new TypedIdent(retTy.tok, "", retTy);
} else SynErr(89);
if (la.kind == 25) {
Get();
Expression(out tmp);
- definition = tmp;
+ definition = tmp;
Expect(26);
} else if (la.kind == 7) {
Get();
@@ -440,35 +440,35 @@ private class BvBounds : Expr {
}
void Axiom(out Axiom! m) {
- Expr! e; QKeyValue kv = null;
+ Expr! e; QKeyValue kv = null;
Expect(27);
while (la.kind == 25) {
Attribute(ref kv);
}
- IToken! x = t;
+ IToken! x = t;
Proposition(out e);
Expect(7);
- m = new Axiom(x,e, null, kv);
+ m = new Axiom(x,e, null, kv);
}
void UserDefinedTypes(out List<Declaration!>! ts) {
- Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> ();
+ Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> ();
Expect(28);
while (la.kind == 25) {
Attribute(ref kv);
}
UserDefinedType(out decl, kv);
- ts.Add(decl);
+ ts.Add(decl);
while (la.kind == 11) {
Get();
UserDefinedType(out decl, kv);
- ts.Add(decl);
+ ts.Add(decl);
}
Expect(7);
}
void GlobalVars(out VariableSeq! ds) {
- TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null;
+ TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null;
Expect(6);
while (la.kind == 25) {
Attribute(ref kv);
@@ -507,10 +507,10 @@ private class BvBounds : Expr {
}
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
} else SynErr(91);
- proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
+ proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
void Implementation(out Implementation! impl) {
@@ -524,13 +524,13 @@ private class BvBounds : Expr {
Expect(31);
ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
ImplBody(out locals, out stmtList);
- impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors);
+ impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors);
}
void Attribute(ref QKeyValue kv) {
- Trigger trig = null;
+ Trigger trig = null;
AttributeOrTrigger(ref kv, ref trig);
- if (trig != null) this.SemErr("only attributes, not triggers, allowed here");
+ if (trig != null) this.SemErr("only attributes, not triggers, allowed here");
}
void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq! tyds) {
@@ -542,7 +542,7 @@ private class BvBounds : Expr {
}
void LocalVars(VariableSeq! ds) {
- TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null;
+ TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null;
Expect(6);
while (la.kind == 25) {
Attribute(ref kv);
@@ -556,7 +556,7 @@ private class BvBounds : Expr {
}
void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq! ds) {
- TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq();
+ TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq();
Expect(8);
if (la.kind == 1) {
IdsTypeWheres(allowWhereClauses, tyds);
@@ -569,7 +569,7 @@ private class BvBounds : Expr {
}
void BoundVars(IToken! x, out VariableSeq! ds) {
- TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq();
+ TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq();
IdsTypeWheres(false, tyds);
foreach (TypedIdent! tyd in tyds) {
ds.Add(new BoundVariable(tyd.tok, tyd));
@@ -578,7 +578,7 @@ private class BvBounds : Expr {
}
void IdsType(out TypedIdentSeq! tyds) {
- TokenSeq! ids; Bpl.Type! ty;
+ TokenSeq! ids; Bpl.Type! ty;
Idents(out ids);
Expect(10);
Type(out ty);
@@ -590,34 +590,34 @@ private class BvBounds : Expr {
}
void Idents(out TokenSeq! xs) {
- IToken! id; xs = new TokenSeq();
+ IToken! id; xs = new TokenSeq();
Ident(out id);
- xs.Add(id);
+ xs.Add(id);
while (la.kind == 11) {
Get();
Ident(out id);
- xs.Add(id);
+ xs.Add(id);
}
}
void Type(out Bpl.Type! ty) {
- IToken! tok; ty = dummyType;
+ IToken! tok; ty = dummyType;
if (la.kind == 8 || la.kind == 13 || la.kind == 14) {
TypeAtom(out ty);
} else if (la.kind == 1) {
Ident(out tok);
- TypeSeq! args = new TypeSeq ();
+ TypeSeq! args = new TypeSeq ();
if (StartOf(2)) {
TypeArgs(args);
}
- ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
+ ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
} else if (la.kind == 15 || la.kind == 17) {
MapType(out ty);
} else SynErr(92);
}
void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {
- TokenSeq! ids; Bpl.Type! ty; Expr wh = null; Expr! nne;
+ TokenSeq! ids; Bpl.Type! ty; Expr wh = null; Expr! nne;
Idents(out ids);
Expect(10);
Type(out ty);
@@ -638,24 +638,24 @@ private class BvBounds : Expr {
}
void Expression(out Expr! e0) {
- IToken! x; Expr! e1;
+ IToken! x; Expr! e1;
ImpliesExpression(false, out e0);
while (la.kind == 52 || la.kind == 53) {
EquivOp();
- x = t;
+ x = t;
ImpliesExpression(false, out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1);
}
}
void TypeAtom(out Bpl.Type! ty) {
- ty = dummyType;
+ ty = dummyType;
if (la.kind == 13) {
Get();
- ty = new BasicType(t, SimpleType.Int);
+ ty = new BasicType(t, SimpleType.Int);
} else if (la.kind == 14) {
Get();
- ty = new BasicType(t, SimpleType.Bool);
+ ty = new BasicType(t, SimpleType.Bool);
} else if (la.kind == 8) {
Get();
Type(out ty);
@@ -672,23 +672,23 @@ private class BvBounds : Expr {
}
void TypeArgs(TypeSeq! ts) {
- IToken! tok; Type! ty;
+ IToken! tok; Type! ty;
if (la.kind == 8 || la.kind == 13 || la.kind == 14) {
TypeAtom(out ty);
- ts.Add(ty);
+ ts.Add(ty);
if (StartOf(2)) {
TypeArgs(ts);
}
} else if (la.kind == 1) {
Ident(out tok);
TypeSeq! args = new TypeSeq ();
- ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args));
+ ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args));
if (StartOf(2)) {
TypeArgs(ts);
}
} else if (la.kind == 15 || la.kind == 17) {
MapType(out ty);
- ts.Add(ty);
+ ts.Add(ty);
} else SynErr(94);
}
@@ -701,10 +701,10 @@ private class BvBounds : Expr {
if (la.kind == 17) {
TypeParams(out nnTok, out typeParameters);
- tok = nnTok;
+ tok = nnTok;
}
Expect(15);
- if (tok == null) tok = t;
+ if (tok == null) tok = t;
if (StartOf(2)) {
Types(arguments);
}
@@ -715,9 +715,9 @@ private class BvBounds : Expr {
}
void TypeParams(out IToken! tok, out Bpl.TypeVariableSeq! typeParams) {
- TokenSeq! typeParamToks;
+ TokenSeq! typeParamToks;
Expect(17);
- tok = t;
+ tok = t;
Idents(out typeParamToks);
Expect(18);
typeParams = new TypeVariableSeq ();
@@ -727,13 +727,13 @@ private class BvBounds : Expr {
}
void Types(TypeSeq! ts) {
- Bpl.Type! ty;
+ Bpl.Type! ty;
Type(out ty);
- ts.Add(ty);
+ ts.Add(ty);
while (la.kind == 11) {
Get();
Type(out ty);
- ts.Add(ty);
+ ts.Add(ty);
}
}
@@ -741,40 +741,40 @@ private class BvBounds : Expr {
ChildrenComplete = false;
Parents = null;
bool u;
- IToken! parent;
+ IToken! parent;
Expect(21);
Parents = new List<ConstantParent!> ();
- u = false;
+ u = false;
if (la.kind == 1 || la.kind == 20) {
if (la.kind == 20) {
Get();
- u = true;
+ u = true;
}
Ident(out parent);
Parents.Add(new ConstantParent (
- new IdentifierExpr(parent, parent.val), u));
+ new IdentifierExpr(parent, parent.val), u));
while (la.kind == 11) {
Get();
- u = false;
+ u = false;
if (la.kind == 20) {
Get();
- u = true;
+ u = true;
}
Ident(out parent);
Parents.Add(new ConstantParent (
- new IdentifierExpr(parent, parent.val), u));
+ new IdentifierExpr(parent, parent.val), u));
}
}
if (la.kind == 22) {
Get();
- ChildrenComplete = true;
+ ChildrenComplete = true;
}
}
void VarOrType(out TypedIdent! tyd) {
- string! varName = ""; Bpl.Type! ty; IToken! tok;
+ string! varName = ""; Bpl.Type! ty; IToken! tok;
Type(out ty);
- tok = ty.tok;
+ tok = ty.tok;
if (la.kind == 10) {
Get();
if (ty is UnresolvedTypeIdentifier &&
@@ -786,7 +786,7 @@ private class BvBounds : Expr {
Type(out ty);
}
- tyd = new TypedIdent(tok, varName, ty);
+ tyd = new TypedIdent(tok, varName, ty);
}
void Proposition(out Expr! e) {
@@ -795,7 +795,7 @@ private class BvBounds : Expr {
void UserDefinedType(out Declaration! decl, QKeyValue kv) {
IToken! id; IToken! id2; TokenSeq! paramTokens = new TokenSeq ();
- Type! body = dummyType; bool synonym = false;
+ Type! body = dummyType; bool synonym = false;
Ident(out id);
if (la.kind == 1) {
WhiteSpaceIdents(out paramTokens);
@@ -803,7 +803,7 @@ private class BvBounds : Expr {
if (la.kind == 29) {
Get();
Type(out body);
- synonym = true;
+ synonym = true;
}
if (synonym) {
TypeVariableSeq! typeParams = new TypeVariableSeq();
@@ -817,19 +817,19 @@ private class BvBounds : Expr {
}
void WhiteSpaceIdents(out TokenSeq! xs) {
- IToken! id; xs = new TokenSeq();
+ IToken! id; xs = new TokenSeq();
Ident(out id);
- xs.Add(id);
+ xs.Add(id);
while (la.kind == 1) {
Ident(out id);
- xs.Add(id);
+ xs.Add(id);
}
}
void ProcSignature(bool allowWhereClausesOnFormals, out IToken! name, out TypeVariableSeq! typeParams,
out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
IToken! typeParamTok; typeParams = new TypeVariableSeq();
- outs = new VariableSeq(); kv = null;
+ outs = new VariableSeq(); kv = null;
while (la.kind == 25) {
Attribute(ref kv);
}
@@ -845,7 +845,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
void Spec(RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post) {
- TokenSeq! ms;
+ TokenSeq! ms;
if (la.kind == 32) {
Get();
if (la.kind == 1) {
@@ -865,7 +865,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {
- locals = new VariableSeq();
+ locals = new VariableSeq();
Expect(25);
while (la.kind == 6) {
LocalVars(locals);
@@ -874,51 +874,51 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
void SpecPrePost(bool free, RequiresSeq! pre, EnsuresSeq! post) {
- Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null;
+ Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null;
if (la.kind == 34) {
Get();
- tok = t;
+ tok = t;
while (la.kind == 25) {
Attribute(ref kv);
}
if (StartOf(5)) {
Proposition(out e);
Expect(7);
- pre.Add(new Requires(tok, free, e, null, kv));
+ pre.Add(new Requires(tok, free, e, null, kv));
} else if (la.kind == 36) {
SpecBody(out locals, out blocks);
Expect(7);
- pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv));
+ pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv));
} else SynErr(96);
} else if (la.kind == 35) {
Get();
- tok = t;
+ tok = t;
while (la.kind == 25) {
Attribute(ref kv);
}
if (StartOf(5)) {
Proposition(out e);
Expect(7);
- post.Add(new Ensures(tok, free, e, null, kv));
+ post.Add(new Ensures(tok, free, e, null, kv));
} else if (la.kind == 36) {
SpecBody(out locals, out blocks);
Expect(7);
- post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv));
+ post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv));
} else SynErr(97);
} else SynErr(98);
}
void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {
- locals = new VariableSeq(); Block! b;
+ locals = new VariableSeq(); Block! b;
Expect(36);
while (la.kind == 6) {
LocalVars(locals);
}
SpecBlock(out b);
- blocks = new BlockSeq(b);
+ blocks = new BlockSeq(b);
while (la.kind == 1) {
SpecBlock(out b);
- blocks.Add(b);
+ blocks.Add(b);
}
Expect(37);
}
@@ -947,7 +947,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
if (la.kind == 38) {
Get();
- y = t;
+ y = t;
Idents(out xs);
foreach (IToken! s in xs) { ss.Add(s.val); }
b = new Block(x,x.val,cs,new GotoCmd(y,ss));
@@ -955,7 +955,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
} else if (la.kind == 39) {
Get();
Expression(out e);
- b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
+ b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
} else SynErr(99);
Expect(7);
}
@@ -972,22 +972,22 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
LabelOrAssign(out c, out label);
} else if (la.kind == 46) {
Get();
- x = t;
+ x = t;
while (la.kind == 25) {
Attribute(ref kv);
}
Proposition(out e);
- c = new AssertCmd(x,e, kv);
+ c = new AssertCmd(x,e, kv);
Expect(7);
} else if (la.kind == 47) {
Get();
- x = t;
+ x = t;
Proposition(out e);
- c = new AssumeCmd(x,e);
+ c = new AssumeCmd(x,e);
Expect(7);
} else if (la.kind == 48) {
Get();
- x = t;
+ x = t;
Idents(out xs);
Expect(7);
ids = new IdentifierExprSeq();
@@ -999,7 +999,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
} else if (la.kind == 50) {
CallCmd(out cn);
Expect(7);
- c = cn;
+ c = cn;
} else SynErr(100);
}
@@ -1078,13 +1078,13 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
if (la.kind == 40) {
IfCmd(out ifcmd);
- ec = ifcmd;
+ ec = ifcmd;
} else if (la.kind == 42) {
WhileCmd(out wcmd);
- ec = wcmd;
+ ec = wcmd;
} else if (la.kind == 45) {
BreakCmd(out bcmd);
- ec = bcmd;
+ ec = bcmd;
} else SynErr(101);
}
@@ -1095,14 +1095,14 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
if (la.kind == 38) {
Get();
- y = t;
+ y = t;
Idents(out xs);
foreach (IToken! s in xs) { ss.Add(s.val); }
tc = new GotoCmd(y, ss);
} else if (la.kind == 39) {
Get();
- tc = new ReturnCmd(t);
+ tc = new ReturnCmd(t);
} else SynErr(102);
Expect(7);
}
@@ -1115,7 +1115,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
StmtList! els; StmtList elseOption = null;
Expect(40);
- x = t;
+ x = t;
Guard(out guard);
Expect(25);
StmtList(out thn);
@@ -1123,14 +1123,14 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
Get();
if (la.kind == 40) {
IfCmd(out elseIf);
- elseIfOption = elseIf;
+ elseIfOption = elseIf;
} else if (la.kind == 25) {
Get();
StmtList(out els);
- elseOption = els;
+ elseOption = els;
} else SynErr(103);
}
- ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
+ ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
void WhileCmd(out WhileCmd! wcmd) {
@@ -1140,14 +1140,14 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
StmtList! body;
Expect(42);
- x = t;
+ x = t;
Guard(out guard);
- assume guard == null || Owner.None(guard);
+ assume guard == null || Owner.None(guard);
while (la.kind == 33 || la.kind == 43) {
- isFree = false; z = la/*lookahead token*/;
+ isFree = false; z = la/*lookahead token*/;
if (la.kind == 33) {
Get();
- isFree = true;
+ isFree = true;
}
Expect(43);
Expression(out e);
@@ -1161,7 +1161,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
Expect(25);
StmtList(out body);
- wcmd = new WhileCmd(x, guard, invariants, body);
+ wcmd = new WhileCmd(x, guard, invariants, body);
}
void BreakCmd(out BreakCmd! bcmd) {
@@ -1169,24 +1169,24 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
string breakLabel = null;
Expect(45);
- x = t;
+ x = t;
if (la.kind == 1) {
Ident(out y);
- breakLabel = y.val;
+ breakLabel = y.val;
}
Expect(7);
- bcmd = new BreakCmd(x, breakLabel);
+ bcmd = new BreakCmd(x, breakLabel);
}
void Guard(out Expr e) {
- Expr! ee; e = null;
+ Expr! ee; e = null;
Expect(8);
if (la.kind == 44) {
Get();
- e = null;
+ e = null;
} else if (StartOf(5)) {
Expression(out ee);
- e = ee;
+ e = ee;
} else SynErr(104);
Expect(9);
}
@@ -1199,32 +1199,32 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
List<Expr!>! rhss;
Ident(out id);
- x = t;
+ x = t;
if (la.kind == 10) {
Get();
- c = null; label = x;
+ c = null; label = x;
} else if (la.kind == 11 || la.kind == 15 || la.kind == 49) {
MapAssignIndexes(id, out lhs);
lhss = new List<AssignLhs!> ();
- lhss.Add(lhs);
+ lhss.Add(lhs);
while (la.kind == 11) {
Get();
Ident(out id);
MapAssignIndexes(id, out lhs);
- lhss.Add(lhs);
+ lhss.Add(lhs);
}
Expect(49);
x = t; /* use location of := */
Expression(out e0);
rhss = new List<Expr!> ();
- rhss.Add(e0);
+ rhss.Add(e0);
while (la.kind == 11) {
Get();
Expression(out e0);
- rhss.Add(e0);
+ rhss.Add(e0);
}
Expect(7);
- c = new AssignCmd(x, lhss, rhss);
+ c = new AssignCmd(x, lhss, rhss);
} else SynErr(105);
}
@@ -1237,7 +1237,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
c = dummyCmd;
Expect(50);
- x = t;
+ x = t;
while (la.kind == 25) {
Attribute(ref kv);
}
@@ -1247,17 +1247,17 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
Get();
if (StartOf(8)) {
CallForallArg(out en);
- es.Add(en);
+ es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
- es.Add(en);
+ es.Add(en);
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv);
+ c = new CallCmd(x, first.val, es, ids, kv);
} else if (la.kind == 11 || la.kind == 49) {
- ids.Add(new IdentifierExpr(first, first.val));
+ ids.Add(new IdentifierExpr(first, first.val));
if (la.kind == 11) {
Get();
CallOutIdent(out p);
@@ -1283,35 +1283,35 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
Expect(8);
if (StartOf(8)) {
CallForallArg(out en);
- es.Add(en);
+ es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
- es.Add(en);
+ es.Add(en);
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv);
+ c = new CallCmd(x, first.val, es, ids, kv);
} else SynErr(106);
} else if (la.kind == 51) {
Get();
Ident(out first);
Expect(8);
- args = new List<Expr>();
+ args = new List<Expr>();
if (StartOf(8)) {
CallForallArg(out en);
- args.Add(en);
+ args.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
- args.Add(en);
+ args.Add(en);
}
}
Expect(9);
- c = new CallForallCmd(x, first.val, args, kv);
+ c = new CallForallCmd(x, first.val, args, kv);
} else if (la.kind == 44) {
Get();
- ids.Add(null);
+ ids.Add(null);
if (la.kind == 11) {
Get();
CallOutIdent(out p);
@@ -1337,15 +1337,15 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
Expect(8);
if (StartOf(8)) {
CallForallArg(out en);
- es.Add(en);
+ es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
- es.Add(en);
+ es.Add(en);
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv);
+ c = new CallCmd(x, first.val, es, ids, kv);
} else SynErr(107);
}
@@ -1360,21 +1360,21 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
while (la.kind == 15) {
Get();
x = t;
- indexes = new List<Expr!> ();
+ indexes = new List<Expr!> ();
if (StartOf(5)) {
Expression(out e0);
- indexes.Add(e0);
+ indexes.Add(e0);
while (la.kind == 11) {
Get();
Expression(out e0);
- indexes.Add(e0);
+ indexes.Add(e0);
}
}
Expect(16);
runningLhs =
- new MapAssignLhs (x, runningLhs, indexes);
+ new MapAssignLhs (x, runningLhs, indexes);
}
- lhs = runningLhs;
+ lhs = runningLhs;
}
void CallForallArg(out Expr exprOptional) {
@@ -1385,7 +1385,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
Get();
} else if (StartOf(5)) {
Expression(out e);
- exprOptional = e;
+ exprOptional = e;
} else SynErr(108);
}
@@ -1397,42 +1397,42 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
Get();
} else if (la.kind == 1) {
Ident(out p);
- id = p;
+ id = p;
} else SynErr(109);
}
void Expressions(out ExprSeq! es) {
- Expr! e; es = new ExprSeq();
+ Expr! e; es = new ExprSeq();
Expression(out e);
- es.Add(e);
+ es.Add(e);
while (la.kind == 11) {
Get();
Expression(out e);
- es.Add(e);
+ es.Add(e);
}
}
void ImpliesExpression(bool noExplies, out Expr! e0) {
- IToken! x; Expr! e1;
+ IToken! x; Expr! e1;
LogicalExpression(out e0);
if (StartOf(9)) {
if (la.kind == 54 || la.kind == 55) {
ImpliesOp();
- x = t;
+ x = t;
ImpliesExpression(true, out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1);
} else {
ExpliesOp();
if (noExplies)
this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");
- x = t;
+ x = t;
LogicalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
while (la.kind == 56 || la.kind == 57) {
ExpliesOp();
- x = t;
+ x = t;
LogicalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
}
}
}
@@ -1447,30 +1447,30 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
void LogicalExpression(out Expr! e0) {
- IToken! x; Expr! e1; BinaryOperator.Opcode op;
+ IToken! x; Expr! e1; BinaryOperator.Opcode op;
RelationalExpression(out e0);
if (StartOf(10)) {
if (la.kind == 58 || la.kind == 59) {
AndOp();
- x = t;
+ x = t;
RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
while (la.kind == 58 || la.kind == 59) {
AndOp();
- x = t;
+ x = t;
RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
}
} else {
OrOp();
- x = t;
+ x = t;
RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
while (la.kind == 60 || la.kind == 61) {
OrOp();
- x = t;
+ x = t;
RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
}
}
}
@@ -1493,12 +1493,12 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
void RelationalExpression(out Expr! e0) {
- IToken! x; Expr! e1; BinaryOperator.Opcode op;
+ IToken! x; Expr! e1; BinaryOperator.Opcode op;
BvTerm(out e0);
if (StartOf(11)) {
RelOp(out x, out op);
BvTerm(out e1);
- e0 = Expr.Binary(x, op, e0, e1);
+ e0 = Expr.Binary(x, op, e0, e1);
}
}
@@ -1519,67 +1519,67 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
void BvTerm(out Expr! e0) {
- IToken! x; Expr! e1;
+ IToken! x; Expr! e1;
Term(out e0);
while (la.kind == 70) {
Get();
- x = t;
+ x = t;
Term(out e1);
- e0 = new BvConcatExpr(x, e0, e1);
+ e0 = new BvConcatExpr(x, e0, e1);
}
}
void RelOp(out IToken! x, out BinaryOperator.Opcode op) {
- x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
+ x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
switch (la.kind) {
case 62: {
Get();
- x = t; op=BinaryOperator.Opcode.Eq;
+ x = t; op=BinaryOperator.Opcode.Eq;
break;
}
case 17: {
Get();
- x = t; op=BinaryOperator.Opcode.Lt;
+ x = t; op=BinaryOperator.Opcode.Lt;
break;
}
case 18: {
Get();
- x = t; op=BinaryOperator.Opcode.Gt;
+ x = t; op=BinaryOperator.Opcode.Gt;
break;
}
case 63: {
Get();
- x = t; op=BinaryOperator.Opcode.Le;
+ x = t; op=BinaryOperator.Opcode.Le;
break;
}
case 64: {
Get();
- x = t; op=BinaryOperator.Opcode.Ge;
+ x = t; op=BinaryOperator.Opcode.Ge;
break;
}
case 65: {
Get();
- x = t; op=BinaryOperator.Opcode.Neq;
+ x = t; op=BinaryOperator.Opcode.Neq;
break;
}
case 66: {
Get();
- x = t; op=BinaryOperator.Opcode.Subtype;
+ x = t; op=BinaryOperator.Opcode.Subtype;
break;
}
case 67: {
Get();
- x = t; op=BinaryOperator.Opcode.Neq;
+ x = t; op=BinaryOperator.Opcode.Neq;
break;
}
case 68: {
Get();
- x = t; op=BinaryOperator.Opcode.Le;
+ x = t; op=BinaryOperator.Opcode.Le;
break;
}
case 69: {
Get();
- x = t; op=BinaryOperator.Opcode.Ge;
+ x = t; op=BinaryOperator.Opcode.Ge;
break;
}
default: SynErr(115); break;
@@ -1587,33 +1587,33 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
void Term(out Expr! e0) {
- IToken! x; Expr! e1; BinaryOperator.Opcode op;
+ IToken! x; Expr! e1; BinaryOperator.Opcode op;
Factor(out e0);
while (la.kind == 71 || la.kind == 72) {
AddOp(out x, out op);
Factor(out e1);
- e0 = Expr.Binary(x, op, e0, e1);
+ e0 = Expr.Binary(x, op, e0, e1);
}
}
void Factor(out Expr! e0) {
- IToken! x; Expr! e1; BinaryOperator.Opcode op;
+ IToken! x; Expr! e1; BinaryOperator.Opcode op;
UnaryExpression(out e0);
while (la.kind == 44 || la.kind == 73 || la.kind == 74) {
MulOp(out x, out op);
UnaryExpression(out e1);
- e0 = Expr.Binary(x, op, e0, e1);
+ e0 = Expr.Binary(x, op, e0, e1);
}
}
void AddOp(out IToken! x, out BinaryOperator.Opcode op) {
- x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
+ x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
if (la.kind == 71) {
Get();
- x = t; op=BinaryOperator.Opcode.Add;
+ x = t; op=BinaryOperator.Opcode.Add;
} else if (la.kind == 72) {
Get();
- x = t; op=BinaryOperator.Opcode.Sub;
+ x = t; op=BinaryOperator.Opcode.Sub;
} else SynErr(116);
}
@@ -1623,30 +1623,30 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
if (la.kind == 72) {
Get();
- x = t;
+ x = t;
UnaryExpression(out e);
- e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e);
+ e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e);
} else if (la.kind == 75 || la.kind == 76) {
NegOp();
- x = t;
+ x = t;
UnaryExpression(out e);
- e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
+ e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(12)) {
CoercionExpression(out e);
} else SynErr(117);
}
void MulOp(out IToken! x, out BinaryOperator.Opcode op) {
- x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
+ x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
if (la.kind == 44) {
Get();
- x = t; op=BinaryOperator.Opcode.Mul;
+ x = t; op=BinaryOperator.Opcode.Mul;
} else if (la.kind == 73) {
Get();
- x = t; op=BinaryOperator.Opcode.Div;
+ x = t; op=BinaryOperator.Opcode.Div;
} else if (la.kind == 74) {
Get();
- x = t; op=BinaryOperator.Opcode.Mod;
+ x = t; op=BinaryOperator.Opcode.Mod;
} else SynErr(118);
}
@@ -1666,10 +1666,10 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
ArrayExpression(out e);
while (la.kind == 10) {
Get();
- x = t;
+ x = t;
if (StartOf(2)) {
Type(out coercedTo);
- e = Expr.CoerceType(x, e, coercedTo);
+ e = Expr.CoerceType(x, e, coercedTo);
} else if (la.kind == 3) {
Nat(out bn);
if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {
@@ -1694,7 +1694,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
Get();
x = t; allArgs = new ExprSeq ();
allArgs.Add(e);
- store = false; bvExtract = false;
+ store = false; bvExtract = false;
if (StartOf(13)) {
if (StartOf(5)) {
Expression(out index0);
@@ -1722,7 +1722,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
} else {
Get();
Expression(out e1);
- allArgs.Add(e1); store = true;
+ allArgs.Add(e1); store = true;
}
}
Expect(16);
@@ -1733,7 +1733,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
((BvBounds)index0).Upper.ToIntSafe,
((BvBounds)index0).Lower.ToIntSafe);
else
- e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
+ e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
}
}
@@ -1761,34 +1761,34 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
switch (la.kind) {
case 77: {
Get();
- e = new LiteralExpr(t, false);
+ e = new LiteralExpr(t, false);
break;
}
case 78: {
Get();
- e = new LiteralExpr(t, true);
+ e = new LiteralExpr(t, true);
break;
}
case 3: {
Nat(out bn);
- e = new LiteralExpr(t, bn);
+ e = new LiteralExpr(t, bn);
break;
}
case 2: {
BvLit(out bn, out n);
- e = new LiteralExpr(t, bn, n);
+ e = new LiteralExpr(t, bn, n);
break;
}
case 1: {
Ident(out x);
- id = new IdentifierExpr(x, x.val); e = id;
+ id = new IdentifierExpr(x, x.val); e = id;
if (la.kind == 8) {
Get();
if (StartOf(5)) {
Expressions(out es);
- e = new NAryExpr(x, new FunctionCall(id), es);
+ e = new NAryExpr(x, new FunctionCall(id), es);
} else if (la.kind == 9) {
- e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
+ e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
} else SynErr(121);
Expect(9);
}
@@ -1796,11 +1796,11 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
case 79: {
Get();
- x = t;
+ x = t;
Expect(8);
Expression(out e);
Expect(9);
- e = new OldExpr(x, e);
+ e = new OldExpr(x, e);
break;
}
case 8: {
@@ -1809,27 +1809,27 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
Expression(out e);
if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
- "are not allowed");
+ "are not allowed");
} else if (la.kind == 51 || la.kind == 81) {
Forall();
- x = t;
+ x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
- e = new ForallExpr(x, typeParams, ds, kv, trig, e);
+ e = new ForallExpr(x, typeParams, ds, kv, trig, e);
} else if (la.kind == 82 || la.kind == 83) {
Exists();
- x = t;
+ x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
- e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
+ e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
} else if (la.kind == 84 || la.kind == 85) {
Lambda();
- x = t;
+ x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (trig != null)
SemErr("triggers not allowed in lambda expressions");
if (typeParams.Length + ds.Length > 0)
- e = new LambdaExpr(x, typeParams, ds, kv, e);
+ e = new LambdaExpr(x, typeParams, ds, kv, e);
} else SynErr(122);
Expect(9);
break;
@@ -1906,16 +1906,16 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
void IfThenElseExpression(out Expr! e) {
IToken! tok;
- Expr! e0, e1, e2;
- e = dummyExpr;
+ Expr! e0, e1, e2;
+ e = dummyExpr;
Expect(40);
- tok = t;
+ tok = t;
Expression(out e0);
Expect(80);
Expression(out e1);
Expect(41);
Expression(out e2);
- e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2));
+ e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2));
}
void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
@@ -1924,18 +1924,18 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
List<object!> parameters; object! param;
Expect(25);
- tok = t;
+ tok = t;
if (la.kind == 10) {
Get();
Expect(1);
- key = t.val; parameters = new List<object!>();
+ key = t.val; parameters = new List<object!>();
if (StartOf(14)) {
AttributeParameter(out param);
- parameters.Add(param);
+ parameters.Add(param);
while (la.kind == 11) {
Get();
AttributeParameter(out param);
- parameters.Add(param);
+ parameters.Add(param);
}
}
if (key == "nopats") {
@@ -1959,11 +1959,11 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
} else if (StartOf(5)) {
Expression(out e);
- es = new ExprSeq(e);
+ es = new ExprSeq(e);
while (la.kind == 11) {
Get();
Expression(out e);
- es.Add(e);
+ es.Add(e);
}
if (trig==null) {
trig = new Trigger(tok, true, es, null);
@@ -1981,10 +1981,10 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
if (la.kind == 4) {
Get();
- o = t.val.Substring(1, t.val.Length-2);
+ o = t.val.Substring(1, t.val.Length-2);
} else if (StartOf(5)) {
Expression(out e);
- o = e;
+ o = e;
} else SynErr(129);
}
diff --git a/Source/Core/PureCollections.ssc b/Source/Core/PureCollections.ssc
index 971af388..e6d68a34 100644
--- a/Source/Core/PureCollections.ssc
+++ b/Source/Core/PureCollections.ssc
@@ -68,7 +68,7 @@ namespace PureCollections {
if (o == null || !(o is Tuple) || elems.Length != ((!)((Tuple)o).elems).Length)
return false;
- Tuple s = (Tuple) o;
+ Tuple s = (Tuple) o;
for(int i = 0; i < elems.Length; i ++)
if ( ! Equals(this.elems[i], s.elems[i]))
return false;
@@ -90,7 +90,7 @@ namespace PureCollections {
if (elem != null)
h += elem.GetHashCode();
}
- return h;
+ return h;
}
//Compare - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
@@ -122,7 +122,7 @@ namespace PureCollections {
//ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[Pure]
public override string! ToString() {
- assert this.elems != null;
+ assert this.elems != null;
if (elems.Length==0)
return "()";
@@ -241,7 +241,7 @@ namespace PureCollections {
public void Insert(Object key, Object val) {
if (key == null)
- throw new MissingCase();
+ throw new MissingCase();
assert this.elems != null;
if (elems.Length == 0 || 2*card >= elems.Length){
@@ -274,7 +274,7 @@ namespace PureCollections {
card ++;
return;
} else if (key.Equals(elems[j])) {
- vals[j] = val;
+ vals[j] = val;
return;
}
}
@@ -322,16 +322,16 @@ namespace PureCollections {
if (o == null || !o.Equals(s.vals[i]))
return false;
}
- return true;
+ return true;
}
public static bool operator < (Map s, Map t){
- return s == null || t == null ? false : s.card < t.card && s <= t;
+ return s == null || t == null ? false : s.card < t.card && s <= t;
}
public static bool operator >= (Map s, Map t){
- return t <= s;
+ return t <= s;
}
public static bool operator > (Map s, Map t){
- return t < s;
+ return t < s;
}
// Equality - - - - - - - - - - - - - - - - - - - - - - -
@@ -349,7 +349,7 @@ namespace PureCollections {
}
[Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
public static bool operator != (Map s, Map t){
- return ! (t == s);
+ return ! (t == s);
}
[Pure]
public override int GetHashCode (){
@@ -363,7 +363,7 @@ namespace PureCollections {
h += elem.GetHashCode() + ((!)vals[i]).GetHashCode();
}
}
- return h;
+ return h;
}
//Ordinary map operations- - - - - - - - - - - - - - - - - - - - - - - -
@@ -371,7 +371,7 @@ namespace PureCollections {
[Pure]
public bool Has(Object x) {
if (x == null)
- throw new MissingCase();
+ throw new MissingCase();
assert this.elems != null;
if (elems.Length == 0)
@@ -397,7 +397,7 @@ namespace PureCollections {
if (elems[j] != null && x.Equals(elems[j]))
return vals[j];
}
- return null;
+ return null;
}
public static Map Override(Map! s, Map! t) {
@@ -410,7 +410,7 @@ namespace PureCollections {
for(int i = 0; i< t.elems.Length; i++)
if (t.elems[i] != null)
m.Insert(t.elems[i], t.vals[i]);
- return m;
+ return m;
}
}
@@ -492,7 +492,7 @@ namespace PureCollections {
}
public void Add(object o){
- assert this.elems != null;
+ assert this.elems != null;
int n = this.elems.Length;
int i = this.card++;
if (i == n){
@@ -520,7 +520,7 @@ namespace PureCollections {
public void Remove(Object x) {
if (x == null)
throw new MissingCase();
- assert this.elems != null;
+ assert this.elems != null;
for (int i = 0; i < card; i++) {
if (x.Equals(elems[i])) {
++i;
@@ -549,7 +549,7 @@ namespace PureCollections {
[Pure]
public override string! ToString() {
string s ="";
- assert this.elems != null;
+ assert this.elems != null;
if (card > 0 && elems[0] is Char) {
for(int i =0; i < card ; i++)
{
@@ -585,27 +585,27 @@ namespace PureCollections {
return false;
}
if (s.card != t.card) return false;
- assert s.elems != null;
- assert t.elems != null;
+ assert s.elems != null;
+ assert t.elems != null;
for(int i = 0; i < s.card; i++)
if (! Equals(s.elems[i], t.elems[i]))
return false;
- return true;
+ return true;
}
[Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
public static bool operator != (Sequence s, Sequence t){
- return !(s == t);
+ return !(s == t);
}
[Pure]
public override int GetHashCode (){
int h = 0;
for(int i = 0; i < card; i++)
{
- assert this.elems != null;
+ assert this.elems != null;
object elem = elems[i];
if (elem != null) { h += elem.GetHashCode(); }
}
- return h;
+ return h;
}
//Subset- - - - - - - - - - - - - - - - - - - - - - - - - - - - -
// View Sequence of T as Set of (Integer,T)
@@ -623,23 +623,23 @@ namespace PureCollections {
if (s==null) throw new ArgumentNullException("s");
if (t==null) throw new ArgumentNullException("t");
if (s.card >= t.card) return false;
- assert s.elems != null;
- assert t.elems != null;
+ assert s.elems != null;
+ assert t.elems != null;
for(int i = 0; i < s.card; i++)
if ( ! Equals(s.elems[i], t.elems[i]))
return false;
- return true;
+ return true;
}
public static bool operator <= (Sequence s, Sequence t){
if (s==null) throw new ArgumentNullException("s");
if (t==null) throw new ArgumentNullException("t");
if (s.card > t.card) return false;
- assert s.elems != null;
- assert t.elems != null;
+ assert s.elems != null;
+ assert t.elems != null;
for(int i = 0; i < s.card; i++)
if ( ! Equals(s.elems[i], t.elems[i]))
return false;
- return true;
+ return true;
}
public static bool operator > (Sequence s, Sequence t){ return t < s;}
public static bool operator >= (Sequence s, Sequence t){ return t <= s;}
@@ -649,7 +649,7 @@ namespace PureCollections {
public bool Has(object x) { // WS translate to tailrecursion
if (x == null)
throw new MissingCase();
- assert this.elems != null;
+ assert this.elems != null;
for (int i = 0; i< card; i++)
if (x.Equals(elems[i]))
return true;
@@ -662,7 +662,7 @@ namespace PureCollections {
public int IndexOf(object x) {
if (x == null)
throw new MissingCase();
- assert this.elems != null;
+ assert this.elems != null;
for (int i = 0; i< card; i++)
if (x.Equals(elems[i]))
return i;
@@ -675,7 +675,7 @@ namespace PureCollections {
public int LastIndexOf(object x) {
if (x == null)
throw new MissingCase();
- assert this.elems != null;
+ assert this.elems != null;
for (int i = card - 1; i >= 0; i--)
if (x.Equals(elems[i]))
return i;
@@ -687,26 +687,26 @@ namespace PureCollections {
public static Sequence Tail(Sequence! s) {
Sequence n = new Sequence(new Capacity(s.card-1));
- assert n.elems != null;
- assert s.elems != null;
+ assert n.elems != null;
+ assert s.elems != null;
for (int i = 1; i< s.card; i++) n.elems[n.card++] = s.elems[i];
return n;
}
public static Sequence Front(Sequence! s) {
Sequence n = new Sequence(new Capacity(s.card-1));
- assert n.elems != null;
- assert s.elems != null;
+ assert n.elems != null;
+ assert s.elems != null;
for (int i = 0; i< s.card-1; i++) n.elems[n.card++] = s.elems[i];
return n;
}
public static Sequence Concat(Sequence! s) {
Sequence n = new Sequence(new Capacity(s.card));
- assert n.elems != null;
- assert s.elems != null;
+ assert n.elems != null;
+ assert s.elems != null;
for (int i = 0; i< s.card; i++) {
Sequence t = (Sequence!) s.elems[i];
- assert t.elems != null;
+ assert t.elems != null;
for (int j = 0; j < t.card; j ++)
n.Add(t.elems[j]);
}
@@ -715,8 +715,8 @@ namespace PureCollections {
public static Sequence Reverse(Sequence! s) {
Sequence n = new Sequence(new Capacity(s.card));
- assert n.elems != null;
- assert s.elems != null;
+ assert n.elems != null;
+ assert s.elems != null;
for (int i = s.card-1; i>=0; i--) n.elems[n.card++] = s.elems[i];
return n;
}
@@ -730,9 +730,9 @@ namespace PureCollections {
public static Sequence! Append(Sequence! s, Sequence! t) {
Sequence! n = new Sequence(new Capacity(s.card + t.card));
- assert n.elems != null;
- assert s.elems != null;
- assert t.elems != null;
+ assert n.elems != null;
+ assert s.elems != null;
+ assert t.elems != null;
for (int i = 0; i< s.card; i++) n.elems[n.card++] = s.elems[i];
for (int i = 0; i< t.card; i++) n.elems[n.card++] = t.elems[i];
return n;
@@ -740,18 +740,18 @@ namespace PureCollections {
public static Sequence Zip(Sequence! s, Sequence! t) {
int min = s.card<t.card ? s.card : t.card;
Sequence n = new Sequence(new Capacity(min));
- assert n.elems != null;
- assert s.elems != null;
- assert t.elems != null;
+ assert n.elems != null;
+ assert s.elems != null;
+ assert t.elems != null;
for (int i = 0; i< min; i++) n.elems[n.card++] = new Tuple(s.elems[i], t.elems[i]);
return n;
}
public static Tuple Unzip(Sequence! s) {
Sequence n0 = new Sequence(new Capacity(s.card));
Sequence n1 = new Sequence(new Capacity(s.card));
- assert s.elems != null;
- assert n0.elems != null;
- assert n1.elems != null;
+ assert s.elems != null;
+ assert n0.elems != null;
+ assert n1.elems != null;
for (int i = 0; i< s.card; i++) {
n0.elems[n0.card++] = ((!)((Tuple!)s.elems[i]).elems)[0];
n1.elems[n1.card++] = ((!)((Tuple!)s.elems[i]).elems)[1];
@@ -762,7 +762,7 @@ namespace PureCollections {
public static Sequence FromTo(int from, int to) { //WS hash the result!
if (from > to) return new Sequence();
Sequence n = new Sequence(new Capacity(to-from+1));
- assert n.elems != null;
+ assert n.elems != null;
for (int i = from; i<= to; i++)
n.elems[n.card++] = i;
return n;
@@ -773,10 +773,10 @@ namespace PureCollections {
int incr = step-from;
if (incr >0)
for (int i = from; i<= to; i+=incr)
- n.Add(i);
+ n.Add(i);
else if (incr < 0)
for (int i = to; i>= from; i-=incr)
- n.Add(i);
+ n.Add(i);
return n;
}
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc
index c4988de3..97a2dfea 100644
--- a/Source/Core/Scanner.ssc
+++ b/Source/Core/Scanner.ssc
@@ -237,40 +237,40 @@ public class Scanner {
for (int i = 126; i <= 126; ++i) start[i] = 2;
for (int i = 48; i <= 57; ++i) start[i] = 9;
for (int i = 34; i <= 34; ++i) start[i] = 6;
- start[92] = 1;
- start[59] = 10;
- start[40] = 11;
- start[41] = 12;
- start[58] = 47;
- start[44] = 13;
- start[91] = 14;
- start[93] = 15;
- start[60] = 48;
- start[62] = 49;
- start[123] = 50;
- start[125] = 51;
- start[61] = 52;
- start[42] = 18;
- start[8660] = 21;
- start[8658] = 23;
- start[8656] = 24;
- start[38] = 25;
- start[8743] = 27;
- start[124] = 28;
- start[8744] = 30;
- start[33] = 53;
- start[8800] = 34;
- start[8804] = 35;
- start[8805] = 36;
- start[43] = 54;
- start[45] = 38;
- start[47] = 39;
- start[37] = 40;
- start[172] = 41;
- start[8704] = 42;
- start[8707] = 43;
- start[955] = 44;
- start[8226] = 46;
+ start[92] = 1;
+ start[59] = 10;
+ start[40] = 11;
+ start[41] = 12;
+ start[58] = 47;
+ start[44] = 13;
+ start[91] = 14;
+ start[93] = 15;
+ start[60] = 48;
+ start[62] = 49;
+ start[123] = 50;
+ start[125] = 51;
+ start[61] = 52;
+ start[42] = 18;
+ start[8660] = 21;
+ start[8658] = 23;
+ start[8656] = 24;
+ start[38] = 25;
+ start[8743] = 27;
+ start[124] = 28;
+ start[8744] = 30;
+ start[33] = 53;
+ start[8800] = 34;
+ start[8804] = 35;
+ start[8805] = 36;
+ start[43] = 54;
+ start[45] = 38;
+ start[47] = 39;
+ start[37] = 40;
+ start[172] = 41;
+ start[8704] = 42;
+ start[8707] = 43;
+ start[955] = 44;
+ start[8226] = 46;
start[Buffer.EOF] = -1;
}
@@ -351,7 +351,7 @@ public class Scanner {
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
if (ch == EOL) {
- line++; col = 0;
+ line++; col = 0;
} else if (ch == '#' && col == 1) {
int prLine = line;
int prColumn = 0;
@@ -510,7 +510,7 @@ public class Scanner {
int recKind = noSym;
int recEnd = pos;
t = new Token();
- t.pos = pos; t.col = col; t.line = line;
+ t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
if (start.ContainsKey(ch)) { state = (int) (!) start[ch]; }
diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc
index e476e41b..be39fb8f 100644
--- a/Source/Core/StandardVisitor.ssc
+++ b/Source/Core/StandardVisitor.ssc
@@ -58,12 +58,12 @@ namespace Microsoft.Boogie
}
public virtual AIVariableExpr! VisitAIVariableExpr(AIVariableExpr! node)
{
- return node;
+ return node;
}
public virtual Cmd! VisitAssertCmd(AssertCmd! node)
{
node.Expr = this.VisitExpr(node.Expr);
- return node;
+ return node;
}
public virtual Cmd! VisitAssignCmd(AssignCmd! node)
{
@@ -76,21 +76,21 @@ namespace Microsoft.Boogie
public virtual Cmd! VisitAssumeCmd(AssumeCmd! node)
{
node.Expr = this.VisitExpr(node.Expr);
- return node;
+ return node;
}
public virtual AtomicRE! VisitAtomicRE(AtomicRE! node)
{
node.b = this.VisitBlock(node.b);
- return node;
+ return node;
}
public virtual Axiom! VisitAxiom(Axiom! node)
{
node.Expr = this.VisitExpr(node.Expr);
- return node;
+ return node;
}
public virtual Type! VisitBasicType(BasicType! node)
{
- return this.VisitType(node);
+ return this.VisitType(node);
}
public virtual BvConcatExpr! VisitBvConcatExpr(BvConcatExpr! node)
{
@@ -100,7 +100,7 @@ namespace Microsoft.Boogie
}
public virtual Type! VisitBvType(BvType! node)
{
- return this.VisitType(node);
+ return this.VisitType(node);
}
public virtual Type! VisitBvTypeProxy(BvTypeProxy! node)
{
@@ -114,13 +114,13 @@ namespace Microsoft.Boogie
{
node.Cmds = this.VisitCmdSeq(node.Cmds);
node.TransferCmd = this.VisitTransferCmd((!)node.TransferCmd);
- return node;
+ return node;
}
public virtual Expr! VisitBlockExpr(BlockExpr! node)
{
node.LocVars = this.VisitVariableSeq(node.LocVars);
node.Blocks = this.VisitBlockSeq(node.Blocks);
- return node;
+ return node;
}
public virtual BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)
{
@@ -138,7 +138,7 @@ namespace Microsoft.Boogie
public virtual BoundVariable! VisitBoundVariable(BoundVariable! node)
{
node = (BoundVariable) this.VisitVariable(node);
- return node;
+ return node;
}
public virtual Cmd! VisitCallCmd(CallCmd! node)
{
@@ -148,7 +148,7 @@ namespace Microsoft.Boogie
for (int i = 0; i < node.Outs.Count; ++i)
if (node.Outs[i] != null)
node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr((!)node.Outs[i]);
- return node;
+ return node;
}
public virtual Cmd! VisitCallForallCmd(CallForallCmd! node)
{
@@ -162,7 +162,7 @@ namespace Microsoft.Boogie
}
node.Ins = elist;
node.Proc = this.VisitProcedure((!)node.Proc);
- return node;
+ return node;
}
public virtual CmdSeq! VisitCmdSeq(CmdSeq! cmdSeq)
{
@@ -173,7 +173,7 @@ namespace Microsoft.Boogie
public virtual Choice! VisitChoice(Choice! node)
{
node.rs = this.VisitRESeq(node.rs);
- return node;
+ return node;
}
public virtual Cmd! VisitCommentCmd(CommentCmd! node)
{
@@ -181,7 +181,7 @@ namespace Microsoft.Boogie
}
public virtual Constant! VisitConstant(Constant! node)
{
- return node;
+ return node;
}
public virtual CtorType! VisitCtorType(CtorType! node)
{
@@ -191,29 +191,29 @@ namespace Microsoft.Boogie
}
public virtual Declaration! VisitDeclaration(Declaration! node)
{
- return node;
+ return node;
}
public virtual List<Declaration!>! VisitDeclarationList(List<Declaration!>! declarationList)
{
for (int i = 0, n = declarationList.Count; i < n; i++)
declarationList[i] = (Declaration!) this.Visit(declarationList[i]);
- return declarationList;
+ return declarationList;
}
public virtual DeclWithFormals! VisitDeclWithFormals(DeclWithFormals! node)
{
node.InParams = this.VisitVariableSeq(node.InParams);
node.OutParams = this.VisitVariableSeq(node.OutParams);
- return node;
+ return node;
}
public virtual ExistsExpr! VisitExistsExpr(ExistsExpr! node)
{
node = (ExistsExpr) this.VisitQuantifierExpr(node);
- return node;
+ return node;
}
public virtual BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)
{
node.Bitvector = this.VisitExpr(node.Bitvector);
- return node;
+ return node;
}
public virtual Expr! VisitExpr(Expr! node)
{
@@ -224,7 +224,7 @@ namespace Microsoft.Boogie
{
for (int i = 0, n = exprSeq.Length; i < n; i++)
exprSeq[i] = this.VisitExpr( (!)exprSeq[i]);
- return exprSeq;
+ return exprSeq;
}
public virtual Requires! VisitRequires(Requires! @requires)
{
@@ -251,50 +251,50 @@ namespace Microsoft.Boogie
public virtual ForallExpr! VisitForallExpr(ForallExpr! node)
{
node = (ForallExpr) this.VisitQuantifierExpr(node);
- return node;
+ return node;
}
public virtual LambdaExpr! VisitLambdaExpr(LambdaExpr! node)
{
node = (LambdaExpr) this.VisitBinderExpr(node);
- return node;
+ return node;
}
public virtual Formal! VisitFormal(Formal! node)
{
- return node;
+ return node;
}
public virtual Function! VisitFunction(Function! node)
{
node = (Function) this.VisitDeclWithFormals(node);
if (node.Body != null)
node.Body = this.VisitExpr(node.Body);
- return node;
+ return node;
}
public virtual GlobalVariable! VisitGlobalVariable(GlobalVariable! node)
{
node = (GlobalVariable) this.VisitVariable(node);
- return node;
+ return node;
}
public virtual GotoCmd! VisitGotoCmd(GotoCmd! node)
{
node.labelTargets = this.VisitBlockSeq((!)node.labelTargets);
- return node;
+ return node;
}
public virtual Cmd! VisitHavocCmd(HavocCmd! node)
{
node.Vars = this.VisitIdentifierExprSeq(node.Vars);
- return node;
+ return node;
}
public virtual Expr! VisitIdentifierExpr(IdentifierExpr! node)
{
if (node.Decl != null)
node.Decl = this.VisitVariable(node.Decl);
- return node;
+ return node;
}
public virtual IdentifierExprSeq! VisitIdentifierExprSeq(IdentifierExprSeq! identifierExprSeq)
{
for (int i = 0, n = identifierExprSeq.Length; i < n; i++)
identifierExprSeq[i] = (IdentifierExpr) this.VisitIdentifierExpr( (!)identifierExprSeq[i]);
- return identifierExprSeq;
+ return identifierExprSeq;
}
public virtual Implementation! VisitImplementation(Implementation! node)
{
@@ -302,16 +302,16 @@ namespace Microsoft.Boogie
node.Blocks = this.VisitBlockList(node.Blocks);
node.Proc = this.VisitProcedure((!)node.Proc);
node = (Implementation) this.VisitDeclWithFormals(node); // do this first or last?
- return node;
+ return node;
}
public virtual LiteralExpr! VisitLiteralExpr(LiteralExpr! node)
{
- return node;
+ return node;
}
public virtual LocalVariable! VisitLocalVariable(LocalVariable! node)
{
- return node;
+ return node;
}
public virtual AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)
@@ -319,7 +319,7 @@ namespace Microsoft.Boogie
node.Map = (AssignLhs!)this.Visit(node.Map);
for (int i = 0; i < node.Indexes.Count; ++i)
node.Indexes[i] = (Expr!)this.Visit(node.Indexes[i]);
- return node;
+ return node;
}
public virtual MapType! VisitMapType(MapType! node)
{
@@ -345,12 +345,12 @@ namespace Microsoft.Boogie
public virtual Expr! VisitNAryExpr(NAryExpr! node)
{
node.Args = this.VisitExprSeq(node.Args);
- return node;
+ return node;
}
public virtual Expr! VisitOldExpr(OldExpr! node)
{
node.Expr = this.VisitExpr(node.Expr);
- return node;
+ return node;
}
public virtual Procedure! VisitProcedure(Procedure! node)
{
@@ -359,19 +359,19 @@ namespace Microsoft.Boogie
node.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
node.OutParams = this.VisitVariableSeq(node.OutParams);
node.Requires = this.VisitRequiresSeq(node.Requires);
- return node;
+ return node;
}
public virtual Program! VisitProgram(Program! node)
{
node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);
- return node;
+ return node;
}
public virtual BinderExpr! VisitBinderExpr(BinderExpr! node)
{
node.Body = this.VisitExpr(node.Body);
node.Dummies = this.VisitVariableSeq(node.Dummies);
//node.Type = this.VisitType(node.Type);
- return node;
+ return node;
}
public virtual QuantifierExpr! VisitQuantifierExpr(QuantifierExpr! node)
{
@@ -379,7 +379,7 @@ namespace Microsoft.Boogie
if (node.Triggers != null) {
node.Triggers = this.VisitTrigger(node.Triggers);
}
- return node;
+ return node;
}
public virtual Cmd! VisitRE(RE! node)
{
@@ -389,11 +389,11 @@ namespace Microsoft.Boogie
{
for (int i = 0, n = reSeq.Length; i < n; i++)
reSeq[i] = (RE) this.VisitRE( (!)reSeq[i]);
- return reSeq;
+ return reSeq;
}
public virtual ReturnCmd! VisitReturnCmd(ReturnCmd! node)
{
- return (ReturnCmd) this.VisitTransferCmd(node);
+ return (ReturnCmd) this.VisitTransferCmd(node);
}
public virtual ReturnExprCmd! VisitReturnExprCmd(ReturnExprCmd! node)
{
@@ -404,23 +404,23 @@ namespace Microsoft.Boogie
{
node.first = (RE) this.VisitRE(node.first);
node.second = (RE) this.VisitRE(node.second);
- return node;
+ return node;
}
public virtual AssignLhs! VisitSimpleAssignLhs(SimpleAssignLhs! node)
{
node.AssignedVariable =
(IdentifierExpr) this.VisitIdentifierExpr(node.AssignedVariable);
- return node;
+ return node;
}
public virtual Cmd! VisitStateCmd(StateCmd! node)
{
node.Locals = this.VisitVariableSeq(node.Locals);
node.Cmds = this.VisitCmdSeq(node.Cmds);
- return node;
+ return node;
}
public virtual TransferCmd! VisitTransferCmd(TransferCmd! node)
{
- return node;
+ return node;
}
public virtual Trigger! VisitTrigger(Trigger! node)
{
@@ -433,17 +433,17 @@ namespace Microsoft.Boogie
}
}
node.Tr = this.VisitExprSeq(node.Tr);
- return node;
+ return node;
}
// called by default for all nullary type constructors and type variables
public virtual Type! VisitType(Type! node)
{
- return node;
+ return node;
}
public virtual TypedIdent! VisitTypedIdent(TypedIdent! node)
{
node.Type = (Type)this.Visit(node.Type);
- return node;
+ return node;
}
public virtual Declaration! VisitTypeCtorDecl(TypeCtorDecl! node)
{
@@ -462,7 +462,7 @@ namespace Microsoft.Boogie
}
public virtual Type! VisitTypeVariable(TypeVariable! node)
{
- return this.VisitType(node);
+ return this.VisitType(node);
}
public virtual Type! VisitTypeProxy(TypeProxy! node)
{
@@ -474,30 +474,30 @@ namespace Microsoft.Boogie
}
public virtual Type! VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier! node)
{
- return this.VisitType(node);
+ return this.VisitType(node);
}
public virtual Variable! VisitVariable(Variable! node)
{
node.TypedIdent = this.VisitTypedIdent(node.TypedIdent);
- return node;
+ return node;
}
public virtual VariableSeq! VisitVariableSeq(VariableSeq! variableSeq)
{
for (int i = 0, n = variableSeq.Length; i < n; i++)
variableSeq[i] = this.VisitVariable( (!)variableSeq[i]);
- return variableSeq;
+ return variableSeq;
}
public virtual Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
{
node.Ensures = this.VisitEnsures(node.Ensures);
node.Expr = this.VisitExpr(node.Expr);
- return node;
+ return node;
}
public virtual Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
{
node.Requires = this.VisitRequires(node.Requires);
node.Expr = this.VisitExpr(node.Expr);
- return node;
+ return node;
}
}
}
diff --git a/Source/Core/TypeAmbiguitySeeker.ssc b/Source/Core/TypeAmbiguitySeeker.ssc
index 762b9c04..fc7cf071 100644
--- a/Source/Core/TypeAmbiguitySeeker.ssc
+++ b/Source/Core/TypeAmbiguitySeeker.ssc
@@ -42,7 +42,7 @@ namespace Microsoft.Boogie
public override AssignLhs! VisitMapAssignLhs(MapAssignLhs! node) {
CheckTypeParams(node, (!)node.TypeParameters);
- return base.VisitMapAssignLhs(node);
+ return base.VisitMapAssignLhs(node);
}
}
diff --git a/Source/Core/Xml.ssc b/Source/Core/Xml.ssc
index 4dadaf8c..e0583793 100644
--- a/Source/Core/Xml.ssc
+++ b/Source/Core/Xml.ssc
@@ -121,12 +121,12 @@ namespace Microsoft.Boogie
WriteTokenAttributes(b.tok);
wr.WriteAttributeString("label", b.Label);
}
- wr.WriteEndElement();
+ wr.WriteEndElement();
}
wr.WriteEndElement();
}
}
- wr.WriteEndElement();
+ wr.WriteEndElement();
}
}
@@ -155,12 +155,12 @@ namespace Microsoft.Boogie
this.WriteTokenAttributes(b.tok);
wr.WriteAttributeString("label", b.Label);
}
- wr.WriteEndElement();
+ wr.WriteEndElement();
}
wr.WriteEndElement();
}
}
- wr.WriteEndElement();
+ wr.WriteEndElement();
}
}
diff --git a/Source/Graph/Graph.ssc b/Source/Graph/Graph.ssc
index dcbd12a3..12f7fd8c 100644
--- a/Source/Graph/Graph.ssc
+++ b/Source/Graph/Graph.ssc
@@ -435,7 +435,7 @@ public class Graph<Node> {
}
// mark root so it won't be used again
incomingEdges[rootIndex] = -1;
- Node root = numberToNode[rootIndex].Val;
+ Node root = numberToNode[rootIndex].Val;
sorted.Add(root);
++sortedIndex;
foreach (Node s in this.Successors(root)){
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index b211b8f4..881df2ce 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -180,7 +180,7 @@ void ObjectInvariant()
internal const string iffName = "iff"; // logical equivalence
internal const string eqName = "="; // equality
internal const string lessName = "<";
- internal const string greaterName = ">";
+ internal const string greaterName = ">";
internal const string atmostName = "<=";
internal const string atleastName = ">=";
internal const string TRUEName = "true"; // nullary predicate that is always true
@@ -358,7 +358,7 @@ void ObjectInvariant()
Linearise(node.Body, options);
- WriteTriggers(node.Triggers, options);
+ WriteTriggers(node.Triggers, options);
wr.Write(")");
return true;
@@ -591,7 +591,7 @@ void ObjectInvariant()
}
}
- return true;
+ return true;
}
public bool VisitEqOp (VCExprNAry node, LineariserOptions options) {
diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs
index 6db18cb4..b8810e00 100644
--- a/Source/Provers/Simplify/Prover.cs
+++ b/Source/Provers/Simplify/Prover.cs
@@ -97,7 +97,7 @@ namespace Microsoft.Boogie.Simplify {
}
public void Close()
- //modifies this.*;
+ //modifies this.*;
{
cce.BeginExpose(this);
{
diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
index 90284358..6425dd00 100644
--- a/Source/Provers/Z3/Inspector.cs
+++ b/Source/Provers/Z3/Inspector.cs
@@ -44,7 +44,7 @@ void ObjectInvariant()
Labels[lab.label] = lab.pos;
}
}
- return true;
+ return true;
}
}
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 14b551df..208f934b 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -675,7 +675,7 @@ void ObjectInvariant()
cce.Owner.AssignSame(boxedN, cce.Owner.ElementProxy(partitionToValue));
partitionToValue.Add(boxedN);
Contract.Assume( !valueToPartition.ContainsKey(boxedN)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(boxedN, zID);
+ valueToPartition.Add(boxedN, zID);
} else if (type.StartsWith("bv") && BigNum.TryParse(number, out bvVal) && int.TryParse(type.Substring(2), out bvSize)) {
BvConst bitV = new BvConst(bvVal, bvSize);
cce.Owner.AssignSame(bitV, cce.Owner.ElementProxy(partitionToValue));
@@ -1131,7 +1131,7 @@ void ObjectInvariant()
writer.WriteLine("identifierToPartition:");
foreach (KeyValuePair<string, int> kvp in identifierToPartition) {
Contract.Assert(kvp.Key!=null);
- writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
+ writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
}
writer.WriteLine("valueToPartition:");
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 994cb282..689f1024 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -90,7 +90,7 @@ void ObjectInvariant()
public int Timeout { get { return TimeLimit / 1000; } }
public bool Typed {
get {
- return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native;
+ return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native;
}
}
public int Lets {
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs
index d972eba2..892e7a88 100644
--- a/Source/Provers/Z3/TypeDeclCollector.cs
+++ b/Source/Provers/Z3/TypeDeclCollector.cs
@@ -282,7 +282,7 @@ void ObjectInvariant()
private string ExtractBuiltin(Function f) {
Contract.Requires(f != null);
- string retVal = null;
+ string retVal = null;
if (NativeBv) {
retVal = f.FindStringAttribute("bvbuiltin");
}
diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc
index 08554344..29370f69 100644
--- a/Source/VCExpr/Boogie2VCExpr.ssc
+++ b/Source/VCExpr/Boogie2VCExpr.ssc
@@ -123,11 +123,11 @@ namespace Microsoft.Boogie.VCExprAST
}
public void PushScope() {
- Mapping.Add(new Dictionary<VarKind!, VCExprVar!> ());
+ Mapping.Add(new Dictionary<VarKind!, VCExprVar!> ());
}
public void PopScope() {
- assume Mapping.Count > 0;
+ assume Mapping.Count > 0;
Mapping.RemoveAt(Mapping.Count - 1);
}
@@ -266,7 +266,7 @@ namespace Microsoft.Boogie.VCExprAST
public override Expr! VisitIdentifierExpr(IdentifierExpr! node) {
assume node.Decl != null; // the expression has to be resolved
Push(LookupVariable(node.Decl));
- return node;
+ return node;
}
///////////////////////////////////////////////////////////////////////////////////
@@ -328,13 +328,13 @@ namespace Microsoft.Boogie.VCExprAST
public override ExistsExpr! VisitExistsExpr(ExistsExpr! node)
{
node = (ExistsExpr) this.VisitQuantifierExpr(node);
- return node;
+ return node;
}
public override ForallExpr! VisitForallExpr(ForallExpr! node)
{
node = (ForallExpr) this.VisitQuantifierExpr(node);
- return node;
+ return node;
}
private VCExpr! TranslateQuantifierExpr(QuantifierExpr! node)
diff --git a/Source/VCExpr/Clustering.ssc b/Source/VCExpr/Clustering.ssc
index 7692ceb1..3b256121 100644
--- a/Source/VCExpr/Clustering.ssc
+++ b/Source/VCExpr/Clustering.ssc
@@ -187,7 +187,7 @@ namespace Microsoft.Boogie.Clustering
int reprSizeA, reprSizeB;
visitor.RepresentationSize(globalVars, out reprSizeA, out reprSizeB);
- Dist = (a.Size - 1) * reprSizeA + (b.Size - 1) * reprSizeB;
+ Dist = (a.Size - 1) * reprSizeA + (b.Size - 1) * reprSizeB;
}
}
@@ -443,7 +443,7 @@ namespace Microsoft.Boogie.Clustering
VCExprVar nodeAsVar = node as VCExprVar;
if (nodeAsVar == null || globalVars.ContainsKey(nodeAsVar))
Size = Size + 1;
- return true;
+ return true;
}
}
} \ No newline at end of file
diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc
index 64af05fd..52c51c3e 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.ssc
+++ b/Source/VCExpr/SimplifyLikeLineariser.ssc
@@ -262,7 +262,7 @@ namespace Microsoft.Boogie.VCExprAST
internal const string! eqName = "EQ"; // equality
internal const string! neqName = "NEQ"; // inequality
internal const string! lessName = "<";
- internal const string! greaterName = ">";
+ internal const string! greaterName = ">";
internal const string! atmostName = "<=";
internal const string! atleastName = ">=";
internal const string! TRUEName = "TRUE"; // nullary predicate that is always true
@@ -377,7 +377,7 @@ namespace Microsoft.Boogie.VCExprAST
} else {
wr.Write("({0} ", eqName);
WriteId(printedName);
- wr.Write(" {0})", boolTrueName);
+ wr.Write(" {0})", boolTrueName);
}
return true;
@@ -663,7 +663,7 @@ namespace Microsoft.Boogie.VCExprAST
ExprLineariser.Linearise(node[0], options);
wr.Write("))");
} else {
- WriteApplication(impliesName, node, options);
+ WriteApplication(impliesName, node, options);
}
return true;
}
diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc
index bbf9d16e..8ea6ff81 100644
--- a/Source/VCExpr/TypeErasure.ssc
+++ b/Source/VCExpr/TypeErasure.ssc
@@ -131,7 +131,7 @@ namespace Microsoft.Boogie.TypeErasure
List<VCExprVar!>! res = new List<VCExprVar!> (types.Count);
for (int i = 0; i < types.Count; ++i)
res.Add(gen.Variable(baseName + i, types[i]));
- return res;
+ return res;
}
}
@@ -318,7 +318,7 @@ namespace Microsoft.Boogie.TypeErasure
Typed2UntypedVariables.Add(var, res);
AddVarTypeAxiom(res, var.Type);
}
- return (!)res;
+ return (!)res;
}
protected abstract void AddVarTypeAxiom(VCExprVar! var, Type! originalType);
@@ -371,7 +371,7 @@ namespace Microsoft.Boogie.TypeErasure
CurrentCtorNum = BigNum.ZERO;
TypeCtorReprs = new Dictionary<TypeCtorDecl!, TypeCtorRepr> ();
TypeVariableMapping = new Dictionary<TypeVariable!, VCExprVar!> ();
- Typed2UntypedVariables = new Dictionary<VCExprVar!, VCExprVar!> ();
+ Typed2UntypedVariables = new Dictionary<VCExprVar!, VCExprVar!> ();
TypeCtorDecl! uDecl = new TypeCtorDecl(Token.NoToken, "U", 0);
UDecl = uDecl;
@@ -847,7 +847,7 @@ namespace Microsoft.Boogie.TypeErasure
VCExprVar res;
if (!bindings.VCExprVarBindings.TryGetValue(node, out res))
return AxBuilder.Typed2Untyped(node);
- return (!)res;
+ return (!)res;
}
////////////////////////////////////////////////////////////////////////////
@@ -863,7 +863,7 @@ namespace Microsoft.Boogie.TypeErasure
VariableBindings! bindings) {
List<VCExprVar!>! newBoundVars = new List<VCExprVar!> (oldBoundVars.Count);
foreach (VCExprVar! var in oldBoundVars) {
- Type! newType = AxBuilder.TypeAfterErasure(var.Type);
+ Type! newType = AxBuilder.TypeAfterErasure(var.Type);
VCExprVar! newVar = Gen.Variable(var.Name, newType);
newBoundVars.Add(newVar);
bindings.VCExprVarBindings.Add(var, newVar);
@@ -899,7 +899,7 @@ namespace Microsoft.Boogie.TypeErasure
foreach (VCExprVar! var in node.BoundVars) {
Type! newType =
castVariables.Contains(var) ? AxBuilder.U
- : AxBuilder.TypeAfterErasure(var.Type);
+ : AxBuilder.TypeAfterErasure(var.Type);
VCExprVar! newVar = Gen.Variable(var.Name, newType);
newBoundVars.Add(newVar);
newBindings.VCExprVarBindings.Add(var, newVar);
@@ -985,7 +985,7 @@ namespace Microsoft.Boogie.TypeErasure
forall{int i in (1:node.Arity); node[i].Type.Equals(oldType)})
return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType));
else
- return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));
+ return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));
}
///////////////////////////////////////////////////////////////////////////
diff --git a/Source/VCExpr/TypeErasureArguments.ssc b/Source/VCExpr/TypeErasureArguments.ssc
index 4fe37a4e..ec03d2e8 100644
--- a/Source/VCExpr/TypeErasureArguments.ssc
+++ b/Source/VCExpr/TypeErasureArguments.ssc
@@ -199,7 +199,7 @@ namespace Microsoft.Boogie.TypeErasure
NonNullType.AssertInitialized(selectTypes);
NonNullType.AssertInitialized(storeTypes);
- select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);
+ select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);
store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes);
if (CommandLineOptions.Clo.UseArrayTheory) {
diff --git a/Source/VCExpr/TypeErasurePremisses.ssc b/Source/VCExpr/TypeErasurePremisses.ssc
index 734bc16b..5f9c0183 100644
--- a/Source/VCExpr/TypeErasurePremisses.ssc
+++ b/Source/VCExpr/TypeErasurePremisses.ssc
@@ -172,7 +172,7 @@ namespace Microsoft.Boogie.TypeErasure
else
bodyWithPremisses = Gen.AndSimp(typePremisses, body);
- return Gen.Let(typeVarBindings, bodyWithPremisses);
+ return Gen.Let(typeVarBindings, bodyWithPremisses);
}
@@ -278,7 +278,7 @@ namespace Microsoft.Boogie.TypeErasure
}
implicitParams.TrimExcess();
- explicitParams.TrimExcess();
+ explicitParams.TrimExcess();
}
internal UntypedFunction Typed2Untyped(Function! fun) {
@@ -364,7 +364,7 @@ namespace Microsoft.Boogie.TypeErasure
// bound term variables are replaced with bound term variables typed in
// a simpler way
foreach (VCExprVar! var in typedInputVars) {
- Type! newType = TypeAfterErasure(var.Type);
+ Type! newType = TypeAfterErasure(var.Type);
VCExprVar! newVar = Gen.Variable(var.Name, newType);
boundVars.Add(newVar);
bindings.VCExprVarBindings.Add(var, newVar);
@@ -396,7 +396,7 @@ namespace Microsoft.Boogie.TypeErasure
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) return;
AddTypeAxiom(GenVarTypeAxiom(var, originalType,
// we don't have any bindings available
- new Dictionary<TypeVariable!, VCExpr!> ()));
+ new Dictionary<TypeVariable!, VCExpr!> ()));
}
public VCExpr! GenVarTypeAxiom(VCExprVar! var, Type! originalType,
diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc
index 2b5003a6..6128fa55 100644
--- a/Source/VCExpr/VCExprAST.ssc
+++ b/Source/VCExpr/VCExprAST.ssc
@@ -197,7 +197,7 @@ namespace Microsoft.Boogie
// combine the antecedents
e0 = And(e0, n[0]);
e1 = n[1];
- continue;
+ continue;
}
}
break;
@@ -788,7 +788,7 @@ namespace Microsoft.Boogie.VCExprAST
internal VCExprMultiAry(VCExprOp! op, List<VCExpr!>! arguments, List<Type!>! typeArguments)
requires (arguments.Count > 2 || typeArguments.Count > 0);
requires op.Arity == arguments.Count;
- requires op.TypeParamArity == typeArguments.Count;
+ requires op.TypeParamArity == typeArguments.Count;
{
base(op);
this.Arguments = arguments;
diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc
index 1ae71b26..2e3c8f8f 100644
--- a/Source/VCExpr/VCExprASTVisitors.ssc
+++ b/Source/VCExpr/VCExprASTVisitors.ssc
@@ -336,7 +336,7 @@ namespace Microsoft.Boogie.VCExprAST
protected override bool StandardResult(VCExpr! node, bool arg) {
Size = Size + 1;
- return true;
+ return true;
}
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 20f4035b..51318640 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -227,7 +227,7 @@ void ObjectInvariant()
public void PushVCExpr(VCExpr vc)
{
Contract.Requires(vc != null);
- //thmProver.Context.AddAxiom(vc);
+ //thmProver.Context.AddAxiom(vc);
thmProver.PushVCExpression(vc);
}
@@ -326,7 +326,7 @@ void ObjectInvariant()
public class ErrorModel {
public Dictionary<string/*!*/, int>/*!*/ identifierToPartition;
public List<List<string/*!>>!*/>> partitionToIdentifiers;
- public List<Object>/*!*/ partitionToValue;
+ public List<Object>/*!*/ partitionToValue;
public Dictionary<object, int>/*!*/ valueToPartition;
public Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions;
@@ -436,7 +436,7 @@ void ObjectInvariant()
{
if (values[i] == tuple[j]) {
// succeeded in matching tuple[j]
- j++;
+ j++;
if (j == tuple.Count-1) return tuple[tuple.Count - 1];
}
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 6b831baa..28744b27 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -78,7 +78,7 @@ namespace Microsoft.Boogie {
if (b.tok == null) {
Console.WriteLine(" <intermediate block>");
} else {
- // for ErrorTrace == 1 restrict the output;
+ // for ErrorTrace == 1 restrict the output;
// do not print tokens with -17:-4 as their location because they have been
// introduced in the translation and do not give any useful feedback to the user
if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 07ee1eeb..81273319 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -252,7 +252,7 @@ void ObjectInvariant()
public abstract class VCExprTranslator : ICloneable {
public abstract string translate(VCExpr expr, int polarity);
public abstract string Lookup(VCExprVar var);
- public abstract Object Clone();
+ public abstract Object Clone();
}
[ContractClassFor(typeof(VCExprTranslator))]
diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs
index 76035577..d4ee1f35 100644
--- a/Source/VCGeneration/DoomCheck.cs
+++ b/Source/VCGeneration/DoomCheck.cs
@@ -39,12 +39,12 @@ void ObjectInvariant()
}
private Checker m_Checker;
- private DoomErrorHandler m_ErrorHandler;
+ private DoomErrorHandler m_ErrorHandler;
[NotDelayed]
public Evc(Checker check) {
Contract.Requires(check != null);
- m_Checker = check;
+ m_Checker = check;
}
@@ -61,11 +61,11 @@ void ObjectInvariant()
// Todo: Check if vc is trivial true or false
outcome = ProverInterface.Outcome.Undetermined;
Contract.Assert( m_ErrorHandler !=null);
- m_Checker.BeginCheck(reachvar.Name, vc, m_ErrorHandler);
+ m_Checker.BeginCheck(reachvar.Name, vc, m_ErrorHandler);
m_Checker.ProverDone.WaitOne();
try {
- outcome = m_Checker.ReadOutcome();
+ outcome = m_Checker.ReadOutcome();
} catch (UnexpectedProverOutputException e)
{
if (CommandLineOptions.Clo.TraceVerify) {
@@ -102,17 +102,17 @@ void ObjectInvariant()
}
}
- private DoomErrorHandler m_ErrHandler;
- private Checker m_Check;
- private InclusionOrder m_Order;
- private Evc m_Evc;
+ private DoomErrorHandler m_ErrHandler;
+ private Checker m_Check;
+ private InclusionOrder m_Order;
+ private Evc m_Evc;
#endregion
[NotDelayed]
public DoomCheck (Implementation passive_impl, Checker check) {
Contract.Requires(passive_impl != null);
Contract.Requires(check != null);
- m_Check = check;
+ m_Check = check;
if (!VC.DCGen.UseItAsDebugger ) {
m_Order = new InclusionOrder(passive_impl.Blocks[0]);
} else {
@@ -126,7 +126,7 @@ void ObjectInvariant()
Contract.Assert( l2a!=null);
Label2Absy = l2a;
// vce = check.VCExprGen.Implies(vce, vce);
- m_Evc.Initialize(vce);
+ m_Evc.Initialize(vce);
}
/* - Set b to the next block that needs to be checked.
@@ -148,9 +148,9 @@ void ObjectInvariant()
if (!m_Order.SetCurrentResult(reachvar, outcome, m_ErrHandler)) {
outcome = ProverInterface.Outcome.Undetermined;
}
- return true;
+ return true;
} else {
- m_Order.SetCurrentResult(reachvar, ProverInterface.Outcome.Undetermined, m_ErrHandler);
+ m_Order.SetCurrentResult(reachvar, ProverInterface.Outcome.Undetermined, m_ErrHandler);
return false;
}
}
@@ -215,8 +215,8 @@ void ObjectInvariant()
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Green;
Console.WriteLine(vc.ToString());
- Console.ForegroundColor = col;
- Console.WriteLine(" ... was asked.");
+ Console.ForegroundColor = col;
+ Console.WriteLine(" ... was asked.");
*/
}
@@ -227,7 +227,7 @@ void ObjectInvariant()
default:
Contract.Assert(false);throw new cce.UnreachableException(); // unexpected enumeration value
}
- return vc;
+ return vc;
}
public VCExpr LetVC(Block startBlock,
@@ -294,7 +294,7 @@ void ObjectInvariant()
VCExpr vc = Wlp.Block(block, SuccCorrect, context);
- v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);
+ v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);
bindings.Add(gen.LetBinding(v, vc));
blockVariables.Add(block, v);
@@ -314,7 +314,7 @@ void ObjectInvariant()
public List<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>();
- InclusionTree RootNode = new InclusionTree(null);
+ InclusionTree RootNode = new InclusionTree(null);
InclusionTree currentNode = null;
[ContractInvariantMethod]
void ObjectInvariant()
@@ -340,7 +340,7 @@ void ObjectInvariant()
Dictionary<Block, List<Block>> unavoidablemap = new Dictionary<Block, List<Block>>();
Block exitblock = BreadthFirst(rootblock, map2);Contract.Assert(exitblock != null);
- BreadthFirstBwd(exitblock, map);
+ BreadthFirstBwd(exitblock, map);
foreach (KeyValuePair<Block, TraceNode> kvp in map) {
Contract.Assert(kvp.Key != null);Contract.Assert(kvp.Value != null);
@@ -371,7 +371,7 @@ void ObjectInvariant()
Insert2Tree(RootNode,kvp);
}
InitCurrentNode(RootNode);
- //printtree(RootNode, "",0);
+ //printtree(RootNode, "",0);
}
void InitCurrentNode(InclusionTree n) {Contract.Requires(n != null);
@@ -424,12 +424,12 @@ void ObjectInvariant()
if (currentNode != null) {
currentNode.IsDoomed = false;
currentNode.HasBeenChecked = true;
- MarkUndoomedParents(currentNode);
+ MarkUndoomedParents(currentNode);
if (cb != null) {
//Console.WriteLine("CE contains: ");
foreach (Block b in cb.TraceNodes)
{Contract.Assert(b != null);
- //Console.Write("{0}, ", b.Label);
+ //Console.Write("{0}, ", b.Label);
MarkUndoomedFromCE(b, RootNode);
}
//Console.WriteLine();
@@ -447,14 +447,14 @@ void ObjectInvariant()
// if (ECContainsAssertFalse(currentNode.EquivBlock)) {
//
// ConsoleColor col = Console.ForegroundColor;
-// Console.ForegroundColor = ConsoleColor.Blue;
+// Console.ForegroundColor = ConsoleColor.Blue;
// Console.WriteLine("Assert false or PossiblyUnreachable was detected, but ignored");
-// Console.ForegroundColor = col;
+// Console.ForegroundColor = col;
//
-// currentNode.HasBeenChecked = true;
-// currentNode.IsDoomed = false;
-// currentNode = currentNode.Parent;
-// return false;
+// currentNode.HasBeenChecked = true;
+// currentNode.IsDoomed = false;
+// currentNode = currentNode.Parent;
+// return false;
// }
List<Block> traceblocks = new List<Block>();
@@ -464,7 +464,7 @@ void ObjectInvariant()
// cb.OnWarning("Doomed program points found!");
if (cb != null) {
- cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);
+ cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);
}
if (currentNode.EquivBlock.Count>0) {
@@ -596,7 +596,7 @@ void ObjectInvariant()
InclusionTree FindNextNode(InclusionTree n) {Contract.Requires(n != null);
Contract.Assert( n!=n.Parent);
- InclusionTree next = n.Parent;
+ InclusionTree next = n.Parent;
if (next!=null) {
foreach (InclusionTree n0 in next.Children) {
Contract.Assert(n0 != null);
@@ -604,7 +604,7 @@ void ObjectInvariant()
return n0;
}
}
- return FindNextNode(next);
+ return FindNextNode(next);
}
return next;
}
@@ -662,7 +662,7 @@ void ObjectInvariant()
bool IsSubset(List<Block> sub, List<Block> super ) {Contract.Requires(sub!=null);Contract.Requires(cce.NonNullElements(super));
foreach (Block b in sub) {
Contract.Assert(b != null);
- if (!super.Contains(b) ) return false;
+ if (!super.Contains(b) ) return false;
}
return true;
}
@@ -683,7 +683,7 @@ void ObjectInvariant()
private class InclusionTree {
public InclusionTree(InclusionTree p) {
Parent = p;
- HasBeenChecked=false;
+ HasBeenChecked=false;
IsDoomed = false;
}
@@ -731,7 +731,7 @@ void ObjectInvariant()
Contract.Assert( firstpred!=null);
if (blockmap.TryGetValue(firstpred, out t0)) {
Contract.Assert( t0 !=null);
- tn.Unavoidables.AddRange(t0.Unavoidables);
+ tn.Unavoidables.AddRange(t0.Unavoidables);
}
}
@@ -739,8 +739,8 @@ void ObjectInvariant()
TraceNode t = null;
if (blockmap.TryGetValue(b0, out t)) {
Contract.Assert( t!=null);
- tn.Predecessors.Add(t);
- IntersectUnavoidables(t,tn);
+ tn.Predecessors.Add(t);
+ IntersectUnavoidables(t,tn);
if (!t.Successors.Contains(tn)) t.Successors.Add(tn);
blockmap[b0]=t;
}
@@ -807,7 +807,7 @@ void ObjectInvariant()
Contract.Assert( firstpred!=null);
if (blockmap.TryGetValue(firstpred, out t0)) {
Contract.Assert( t0 !=null);
- tn.Unavoidables.AddRange(t0.Unavoidables);
+ tn.Unavoidables.AddRange(t0.Unavoidables);
}
@@ -815,8 +815,8 @@ void ObjectInvariant()
TraceNode t = null;
if (blockmap.TryGetValue(b0, out t)) {
Contract.Assert( t!=null);
- tn.Successors.Add(t);
- IntersectUnavoidables(t,tn);
+ tn.Successors.Add(t);
+ IntersectUnavoidables(t,tn);
if (!t.Predecessors.Contains(tn)) t.Predecessors.Add(tn);
blockmap[b0]=t;
}
@@ -880,7 +880,7 @@ void ObjectInvariant()
public TraceNode(Block b) {
Contract.Requires(b != null);
- block=b;
+ block=b;
}
}
diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs
index 010fce95..f31b597e 100644
--- a/Source/VCGeneration/DoomErrorHandler.cs
+++ b/Source/VCGeneration/DoomErrorHandler.cs
@@ -59,7 +59,7 @@ void ObjectInvariant()
Contract.Requires(cce.NonNullElements(traceblocks));
m_Reachvar = reachvar;
m_DoomedBlocks = doomedblocks;
- m_TraceBlocks = traceblocks;
+ m_TraceBlocks = traceblocks;
}
@@ -90,7 +90,7 @@ void ObjectInvariant()
//Console.Write("{0}, ", b.Label);
} else {
AssertCmd a = (AssertCmd)node;
- assertNodes.Add(a);
+ assertNodes.Add(a);
}
}
m_CurrentTrace.AddRange(traceNodes);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 36e9d40e..abb26eba 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1706,7 +1706,7 @@ namespace VC {
CheckIntAttributeOnImpl(impl, "vcs_max_splits", ref max_splits);
CheckIntAttributeOnImpl(impl, "vcs_max_keep_going_splits", ref max_kg_splits);
if (tmp_max_vc_cost >= 0) {
- max_vc_cost = tmp_max_vc_cost;
+ max_vc_cost = tmp_max_vc_cost;
}
Outcome outcome = Outcome.Correct;
@@ -1721,7 +1721,7 @@ namespace VC {
int total = 0;
int no = max_splits == 1 && !keep_going ? -1 : 0;
bool first_round = true;
- bool do_splitting = keep_going || max_splits > 1;
+ bool do_splitting = keep_going || max_splits > 1;
double remaining_cost = 0.0, proven_cost = 0.0;
if (do_splitting) {
@@ -1952,7 +1952,7 @@ namespace VC {
reporter.underapproximationMode = false;
//Console.Write("Checking with preds == true: "); Console.Out.Flush();
- ret = CheckVC(vc, reporter, checker, impl.Name);
+ ret = CheckVC(vc, reporter, checker, impl.Name);
//Console.WriteLine(ret.ToString());
if(ret == Outcome.Correct) {
@@ -2220,7 +2220,7 @@ namespace VC {
VCExprNAry vnary = node as VCExprNAry;
if(vnary == null) return true;
VCExprBoogieFunctionOp bop = vnary.Op as VCExprBoogieFunctionOp;
- if(bop == null) return true;
+ if(bop == null) return true;
if(implName2StratifiedInliningInfo.ContainsKey(bop.Func.Name)) {
fcalls.Add(vnary);
}
@@ -3236,7 +3236,7 @@ namespace VC {
{
Block entryBlock = cce.NonNull( impl.Blocks[0]);
RemoveEmptyBlocks(entryBlock);
- impl.PruneUnreachableBlocks();
+ impl.PruneUnreachableBlocks();
}
#endregion Get rid of empty blocks
@@ -3318,7 +3318,7 @@ namespace VC {
for (int i = 0; i < cmds.Length; i++)
{
Cmd cmd = cce.NonNull( cmds[i]);
- AssertCmd assertCmd = cmd as AssertCmd;
+ AssertCmd assertCmd = cmd as AssertCmd;
if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0)
{
Counterexample newCounterexample;
@@ -3468,7 +3468,7 @@ namespace VC {
string calleeName = naryExpr.Fun.FunctionName;
if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;
VCExprTranslator vcExprTranslator = cce.NonNull(context.exprTranslator);
- Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;
+ Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;
Contract.Assert(boogieExprTranslator != null);
List<int> args = new List<int>();
foreach (Expr expr in naryExpr.Args)
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index 6001093d..55b1131f 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -182,7 +182,7 @@ namespace VC {
Dictionary<Block, Block> tmpdict = new Dictionary<Block, Block>();
CopyImplBlocks(impl.Blocks[0], ref blist, impl.Blocks[0], ref tmpdict);
blist.Reverse();
- //_tmpImpl = new Implementation(impl.tok, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, impl.LocVars, blist);
+ //_tmpImpl = new Implementation(impl.tok, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, impl.LocVars, blist);
#endregion ////////////////////////////////////
@@ -291,7 +291,7 @@ namespace VC {
UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug;
Stopwatch watch = new Stopwatch();
- //Impl2Dot(impl, String.Format("c:/dot/{0}_raw.dot", impl.Name) );
+ //Impl2Dot(impl, String.Format("c:/dot/{0}_raw.dot", impl.Name) );
if (CommandLineOptions.Clo.TraceVerify) {
Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);
@@ -333,10 +333,10 @@ namespace VC {
#endregion
- //EmitImpl(impl,false);
+ //EmitImpl(impl,false);
- //Impl2Dot(impl, String.Format("c:/dot/{0}_passive.dot", impl.Name) );
+ //Impl2Dot(impl, String.Format("c:/dot/{0}_passive.dot", impl.Name) );
// ---------------------------------------------------------------------------
if (UseItAsDebugger) {
@@ -350,9 +350,9 @@ namespace VC {
}
// ---------------------------------------------------------------------------
- // EmitImpl(impl,false);
+ // EmitImpl(impl,false);
- //Impl2Dot(impl, String.Format("c:/dot/{0}_final.dot", impl.Name) );
+ //Impl2Dot(impl, String.Format("c:/dot/{0}_final.dot", impl.Name) );
bool __debug = false;
@@ -419,7 +419,7 @@ namespace VC {
#region Try to produce a counter example (brute force)
if (dc.DoomedSequences.Count > 0) {
ConsoleColor col = Console.ForegroundColor;
- // Console.ForegroundColor = ConsoleColor.Red;
+ // Console.ForegroundColor = ConsoleColor.Red;
// Console.WriteLine(" {0} is DOOMED!", impl.Name);
// foreach (List<Block!> bl in dc.DoomedSequences) {
// Console.Write("Doomed Blocks: ");
@@ -715,12 +715,12 @@ namespace VC {
// Console.Write(" Witness (");
//
// ConsoleColor col = Console.ForegroundColor;
- // Console.ForegroundColor = ConsoleColor.White;
- // Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col );
+ // Console.ForegroundColor = ConsoleColor.White;
+ // Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col );
// Console.ForegroundColor = col;
- // Console.Write("): ");
+ // Console.Write("): ");
// Console.ForegroundColor = ConsoleColor.Yellow;
- // b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);
+ // b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);
// Console.ForegroundColor = col;
m_doomedCmds.Add(b.Cmds[endidx]);