diff options
Diffstat (limited to 'Source/VCExpr/VCExprASTPrinter.cs')
| -rw-r--r-- | Source/VCExpr/VCExprASTPrinter.cs | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index adb3b27e..00e6fb9c 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -290,12 +290,22 @@ namespace Microsoft.Boogie.VCExprAST { public bool VisitDivOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
- return PrintNAry("/", node, wr);
+ return PrintNAry("div", node, wr);
}
public bool VisitModOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
- return PrintNAry("%", node, wr);
+ return PrintNAry("mod", node, wr);
+ }
+ public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("/", node, wr);
+ }
+ public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("**", node, wr);
}
public bool VisitLtOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
@@ -327,6 +337,16 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null);
return PrintNAry("<::", node, wr);
}
+ public bool VisitToIntOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("int", node, wr);
+ }
+ public bool VisitToRealOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("real", node, wr);
+ }
public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
|