diff options
| author |  boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
|---|---|---|
| committer | boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
| commit | 43b80b13bd24bb789849aac3385df6ac4a8233be (patch) | |
| tree | 499b3dffd74fd84fdf8aedffacbca424d25680b2 /Source/AbsInt | |
| parent | dfb77ee06c82cf8b9c465f3a2acbc5ceb035c6e5 (diff) | |
Boogie: added type 'real' with overloaded arithmetic operations plus real division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 33 |
1 files changed, 31 insertions, 2 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 247a357d..51391105 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -632,6 +632,10 @@ namespace Microsoft.Boogie.AbstractInterpretation var n = ((BigNum)node.Val).ToBigInteger;
Lo = n;
Hi = n + 1;
+ } else if (node.Val is BigDec) {
+ var n = ((BigDec)node.Val).Floor(-BigInteger.Pow(10, 12), BigInteger.Pow(10, 12));
+ Lo = n;
+ Hi = n + 1;
} else if (node.Val is bool) {
if ((bool)node.Val) {
// true
@@ -646,7 +650,7 @@ namespace Microsoft.Boogie.AbstractInterpretation return node;
}
public override Expr VisitIdentifierExpr(IdentifierExpr node) {
- if (node.Type.IsBool || node.Type.IsInt) {
+ if (node.Type.IsBool || node.Type.IsInt || node.Type.IsReal) {
Node.GetBounds(N, node.Decl, out Lo, out Hi);
}
return node;
@@ -655,7 +659,18 @@ namespace Microsoft.Boogie.AbstractInterpretation if (node.Fun is UnaryOperator) {
var op = (UnaryOperator)node.Fun;
Contract.Assert(node.Args.Length == 1);
- if (op.Op == UnaryOperator.Opcode.Not) {
+ if (op.Op == UnaryOperator.Opcode.Neg) {
+ BigInteger? lo, hi;
+ VisitExpr(node.Args[0]);
+ lo = Lo; hi = Hi;
+ if (hi != null) {
+ Lo = 1 - hi;
+ }
+ if (lo != null) {
+ Hi = -lo;
+ }
+ }
+ else if (op.Op == UnaryOperator.Opcode.Not) {
VisitExpr(node.Args[0]);
Contract.Assert((Lo == null && Hi == null) ||
(Lo == null && (BigInteger)Hi == 1) ||
@@ -803,6 +818,20 @@ namespace Microsoft.Boogie.AbstractInterpretation Hi = hi1;
}
break;
+ case BinaryOperator.Opcode.RealDiv:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = new BigInteger(0);
+ Hi = hi1;
+ }
+ break;
+ case BinaryOperator.Opcode.Pow:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = new BigInteger(0);
+ Hi = hi1;
+ }
+ break;
default:
break;
}
|