diff options
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]);
|