summaryrefslogtreecommitdiff
path: root/Source/AbsInt/IntervalDomain.cs
Commit message (Collapse)AuthorAge
* Added and briefly tested the updated syntax. NaN/oo not supported yetGravatar Checkmate502016-07-19
|
* Changed the syntax reading of the float typeGravatar Checkmate502016-07-16
|
* Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
|
* modified floating point syntax and modified floating point constants to use ↵Gravatar Checkmate502016-03-17
| | | | bitvector values
* Added several test cases and some basic documentation for fp usageGravatar Checkmate502016-01-04
|
* added decimal reading functionality to the float typeGravatar Dietrich2015-05-05
|
* renamed fp32 to BigFloatGravatar Dietrich2015-04-20
|
* added float tipe to AbsyExpr and IntervalDomain. The methods added may ↵Gravatar Dietrich2015-04-20
| | | | require later modification
* Change the return type of StandardVisitor.VisitLiteralExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | LiteralExpr to Expr. Enforcing the return type be LiteralExpr is too restrictive. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitBvExtractExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | BvExtractExpr to Expr. Enforcing the return type be BvExtractExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitBvConcatExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | BvConcatExpr to Expr. Enforcing the return type be BvConcatExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type.
* Fixed abstract interpretation for realsGravatar Rustan Leino2014-04-13
|
* Fixed bug in abstract interpretation over realsGravatar Rustan Leino2014-04-08
|
* (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵Gravatar Rustan Leino2014-02-24
| | | | | | of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
* Fixed errors in the use of Code ContractsGravatar Rustan Leino2014-02-10
|
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
|
* Added support in the abstract interpreter for an attribute {:identity}, ↵Gravatar Rustan Leino2013-07-05
| | | | which says that a function is an identity function.
* Fixed bug in Interval abstract domain (pertaining to unary negation)Gravatar Rustan Leino2013-05-30
|
* Fixed some type bugs in the interval domain.Gravatar Rustan Leino2013-02-19
|
* Boogie: added type 'real' with overloaded arithmetic operations plus real ↵Gravatar boehmes2012-09-27
| | | | | | | | | 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)
* Dafny: implemented thresholds for the new interval domain (/infer:j)Gravatar Rustan Leino2011-12-12
|
* Dafny: fixed division in new interval domainGravatar Rustan Leino2011-12-07
|
* Boogie: Added new abstract interpretation harness, which uses native Boogie ↵Gravatar Rustan Leino2011-12-05
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}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 04:36:04 +0000