diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/AbsyExpr.ssc | 18 | ||||
| -rw-r--r-- | Source/Core/Parser.ssc | 6 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.ssc | 2 | ||||
| -rw-r--r-- | Source/Core/Util.ssc | 2 |
4 files changed, 14 insertions, 14 deletions
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc index 82854412..78a796c2 100644 --- a/Source/Core/AbsyExpr.ssc +++ b/Source/Core/AbsyExpr.ssc @@ -2990,12 +2990,12 @@ namespace Microsoft.Boogie - public class ExtractExpr : Expr, AI.IFunApp
+ public class BvExtractExpr : Expr, AI.IFunApp
{
public /*readonly--except in StandardVisitor*/ Expr! Bitvector;
public readonly int Start, End;
- public ExtractExpr(IToken! tok, Expr! bv, int end, int start)
+ public BvExtractExpr(IToken! tok, Expr! bv, int end, int start)
: base(tok)
{
Bitvector = bv;
@@ -3008,9 +3008,9 @@ namespace Microsoft.Boogie public override bool Equals(object obj)
{
if (obj == null) return false;
- if (!(obj is ExtractExpr)) return false;
+ if (!(obj is BvExtractExpr)) return false;
- ExtractExpr other = (ExtractExpr)obj;
+ BvExtractExpr other = (BvExtractExpr)obj;
return object.Equals(this.Bitvector, other.Bitvector) &&
this.Start.Equals(other.Start) && this.End.Equals(other.End);
}
@@ -3100,10 +3100,10 @@ namespace Microsoft.Boogie if(args.Count == 3)
{
- retFun = new ExtractExpr(this.tok,
- BoogieFactory.IExpr2Expr((AI.IExpr!)args[0]),
- ((LiteralExpr!)args[1]).asBigNum.ToIntSafe,
- ((LiteralExpr!)args[2]).asBigNum.ToIntSafe);
+ retFun = new BvExtractExpr(this.tok,
+ BoogieFactory.IExpr2Expr((AI.IExpr!)args[0]),
+ ((LiteralExpr!)args[1]).asBigNum.ToIntSafe,
+ ((LiteralExpr!)args[2]).asBigNum.ToIntSafe);
}
else
{
@@ -3120,7 +3120,7 @@ namespace Microsoft.Boogie public override Absy! StdDispatch(StandardVisitor! visitor)
{
- return visitor.VisitExtractExpr(this);
+ return visitor.VisitBvExtractExpr(this);
}
}
diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc index e91eaf7c..8ae741ab 100644 --- a/Source/Core/Parser.ssc +++ b/Source/Core/Parser.ssc @@ -1617,9 +1617,9 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { if (store)
e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);
else if (bvExtract)
- e = new ExtractExpr(x, e,
- ((BvBounds)index0).Upper.ToIntSafe,
- ((BvBounds)index0).Lower.ToIntSafe);
+ e = new BvExtractExpr(x, e,
+ ((BvBounds)index0).Upper.ToIntSafe,
+ ((BvBounds)index0).Lower.ToIntSafe);
else
e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc index a6068426..1e0ceb8f 100644 --- a/Source/Core/StandardVisitor.ssc +++ b/Source/Core/StandardVisitor.ssc @@ -211,7 +211,7 @@ namespace Microsoft.Boogie node = (ExistsExpr) this.VisitQuantifierExpr(node);
return node;
}
- public virtual ExtractExpr! VisitExtractExpr(ExtractExpr! node)
+ public virtual BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)
{
node.Bitvector = this.VisitExpr(node.Bitvector);
return node;
diff --git a/Source/Core/Util.ssc b/Source/Core/Util.ssc index 914ccf09..e90358ac 100644 --- a/Source/Core/Util.ssc +++ b/Source/Core/Util.ssc @@ -266,7 +266,7 @@ namespace Microsoft.Boogie }
public static string! PrettyPrintBplExpr (Expr! e) {
// anything that is unknown will just be printed via ToString
- // OldExpr and QuantifierExpr, ExtractExpr, BvConcatExpr are ignored for now
+ // OldExpr and QuantifierExpr, BvExtractExpr, BvConcatExpr are ignored for now
// LiteralExpr is printed as itself by ToString
if (e is IdentifierExpr) {
string s = e.ToString();
|