diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-05 23:07:06 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-05 23:07:06 -0800 |
| commit | 95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd (patch) | |
| tree | 014162d0766bdec9922ea6d314ac05bc2d9a065e /Source/Basetypes | |
| parent | 9e18c32b3fda7b377f095e8ee865424c51af1e73 (diff) | |
Boogie: Added new abstract interpretation harness, which uses native Boogie Expr's, not the more abstract AIExpr's.
Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false.
Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals
Boogie: Mark all inferred conditions with attribute {:inferred}
Diffstat (limited to 'Source/Basetypes')
| -rw-r--r-- | Source/Basetypes/BigNum.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs index 73840482..ff676bc6 100644 --- a/Source/Basetypes/BigNum.cs +++ b/Source/Basetypes/BigNum.cs @@ -75,6 +75,12 @@ namespace Microsoft.Basetypes { }
}
+ public BIM ToBigInteger {
+ get {
+ return val;
+ }
+ }
+
// Convert to int; assert that no overflows occur
public int ToIntSafe {
get {
|