summaryrefslogtreecommitdiff
path: root/Source/Basetypes
Commit message (Collapse)AuthorAge
* fixed an error where a -0 was not interpreted as a negative numberGravatar Checkmate502016-07-23
|
* Removed automatic exponent shiftingGravatar Checkmate502016-07-22
|
* fixed floatceiling functionGravatar Checkmate502016-07-19
|
* Added and briefly tested the updated syntax. NaN/oo not supported yetGravatar Checkmate502016-07-19
|
* Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
|
* finished testing, fixed several minor compiler bugsGravatar Checkmate502016-06-06
|
* modified floating point syntax and modified floating point constants to use ↵Gravatar Checkmate502016-03-17
| | | | bitvector values
* Modified BigFloat and parser to accept correct SMT-LIB syntaxGravatar Checkmate502016-02-20
|
* Added several test cases and some basic documentation for fp usageGravatar Checkmate502016-01-04
|
* Special fp types (such as infinity and NaN are now translated by boogieGravatar Checkmate502015-11-29
|
* Floating point constants given as integers are now translated correctlyGravatar Checkmate502015-10-14
|
* Modified translation so that z3 runs with type checking for simple binary ↵Gravatar Checkmate502015-10-14
| | | | operations
* Modified BigFloat to avoid evaluating the floating point value before ↵Gravatar Checkmate502015-09-23
| | | | sending it to z3
* Added initial support for float additionGravatar Checkmate502015-09-17
|
* Float type now works correctly for simple variable declaration and comparison.Gravatar Dietrich2015-07-20
|
* added interpretation of floating point constants to the parserGravatar Dietrich2015-05-18
|
* Made significant changes to internal representation of BigFloat. Remains a ↵Gravatar Dietrich2015-05-07
| | | | work in progress
* added decimal reading functionality to the float typeGravatar Dietrich2015-05-05
|
* added general floating point mantissa and exponent managementGravatar Dietrich2015-05-04
|
* renamed fp32 to BigFloatGravatar Dietrich2015-04-20
|
* adding references to the floating point type wherever references to the real ↵Gravatar Dietrich2015-04-17
| | | | type exist. This remains a work in progress
* Added the fp32 class, copied from the previously existing BigDec class. No ↵Gravatar Dietrich2015-04-17
| | | | significant changes from BigDec have been made
* Fix bug in BigDec.FloorCeiling() which gave the wrong answers forGravatar Dan Liew2015-03-10
| | | | | negative numbers. I have decided that this method will floor towards negative infinity rather than zero to match SMT-LIBv2's to_int function.
* Fix bug in BigDec.FromString() which would not parse negativeGravatar Dan Liew2014-06-18
| | | | | | | | numbers correctly. For example BigDec.FromString("-1.5") would be interpreted as -0.5 due to the incorrect way the method handles the fractional part of the string.
* Fixed abstract interpretation for realsGravatar Rustan Leino2014-04-13
|
* Fixed bug in abstract interpretation over realsGravatar Rustan Leino2014-04-08
|
* Fixed bug in printing real literalsGravatar Rustan Leino2014-02-10
|
* Fix Boogie so it compiled with mono. Patch by Dan Liew.Gravatar Ally Donaldson2014-01-14
|
* added the QED build configurationGravatar qadeer2013-12-02
|
* CVC4 ParserGravatar pantazis2013-06-12
|
* MergeGravatar Unknown2012-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)
| * Added BigDec as representation for (floating-point) decimal valuesGravatar boehmes2012-09-27
|/
* MergeGravatar Rustan Leino2011-12-07
|\
| * Fix some bugs in the new SetGravatar 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}
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
|
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
|
* Added a new solution configuration, Checked, that builds the Checked ↵Gravatar mikebarnett2011-03-07
| | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
* Expose ToByteArray()Gravatar MichalMoskal2011-02-18
|
* One more link to version.csGravatar stobies2010-12-06
|
* Get rid of F# dependencies - use System.Numerics and a custom Rational ↵Gravatar MichalMoskal2010-12-02
| | | | structure instead
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* Boogie:Gravatar rustanleino2010-10-12
| | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
* Update to VS2010.Gravatar MichalMoskal2010-10-07
|
* created a new build target called z3apidebug.Gravatar qadeer2010-08-29
| | | | | only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver.
* Boogie: Removed some errors with code contracts (commenting out ↵Gravatar tabarbe2010-08-27
| | | | doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
* Boogie: Changed the cce classes into one separate project, which every other ↵Gravatar tabarbe2010-08-27
| | | | project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
* Boogie: Basetypes port 2/3: Committing new source file, deleting old oneGravatar tabarbe2010-08-27
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 10:21:57 +0000