summaryrefslogtreecommitdiff
path: root/Source/Core/AbsyExpr.cs
Commit message (Collapse)AuthorAge
...
* Removed old comments about "BASEMOVE" and other constructor calls, where the ↵Gravatar Unknown2013-01-07
| | | | conversion from Spec# into C# moved a constructor call
* Minor refactorings for integrating corralGravatar Unknown2012-11-18
|
* Fixed the build.Gravatar wuestholz2012-09-28
|
* 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)
* Boogie: new syntax for integer division and modulus: use div and mod instead ↵Gravatar boehmes2012-09-27
| | | | of / and %
* Removed AIFramework from Boogie -- use native trivial or native ↵Gravatar boehmes2012-09-27
| | | | | | | interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
* Boogie: Changed Expr.Not to keep swap arguments rather change direction of ↵Gravatar Rustan Leino2011-12-12
| | | | operator when negating <, <=, >=, or >
* MergeGravatar Rustan Leino2011-12-07
|\
| * Fix atg file and add comment about Set/*Variable*/Gravatar Michal Moskal2011-12-07
| |
| * Make set iteration order deterministicGravatar Michal Moskal2011-12-07
| | | | | | | | Make the set class generic
* | 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}
* Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵Gravatar Rustan Leino2011-10-27
| | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
|
* Boogie: Fixed problem with binding power of .[.] versus type coercions in ↵Gravatar rustanleino2011-02-17
| | | | pretty printing
* Added a new method StratifiedVC for refinement.Gravatar akashlal2011-02-08
| | | | Added a method to copy a FunctionCall.
* Boogie: Commented out all occurences of repeated inherited contracts - makes ↵Gravatar tabarbe2010-08-27
| | | | fewer error messages when compiling with runtime checking on.
* Boogie: Committing changed source filesGravatar tabarbe2010-08-20
|
* Boogie: Renaming core sources in preparation for port commitGravatar tabarbe2010-08-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 07:51:57 +0000