summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)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
* rebuilt scanner and parser via cocoGravatar Checkmate502016-07-16
* change to updateGravatar Checkmate502016-06-07
* removed an unnecessary type checking additionGravatar Checkmate502016-06-07
* fixed some merging issuesGravatar Checkmate502016-06-07
* resolving conflictsGravatar Checkmate502016-06-06
|\
* | Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
* | finished testing, fixed several minor compiler bugsGravatar Checkmate502016-06-06
* | Initial round of testing works with new syntax. Fixed an error where floatin...Gravatar Checkmate502016-05-31
| * Rename DLLs to non-generic names by prefixing "Boogie". Project names andGravatar akashlal2016-04-15
* | modified floating point syntax and modified floating point constants to use b...Gravatar Checkmate502016-03-17
* | Modified BigFloat and parser to accept correct SMT-LIB syntaxGravatar Checkmate502016-02-20
* | Special fp types (such as infinity and NaN are now translated by boogieGravatar Checkmate502015-11-29
| * Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
| * Fix issue with partially-verified assertions.Gravatar Valentin Wüstholz2015-11-19
| * Add experimental support for optimization (requires Z3 build after changeset ...Gravatar Valentin Wüstholz2015-11-18
| * Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
| * Document the new behaviour of the ``-proc:`` command line optionGravatar Dan Liew2015-10-31
| * Added wild card matching for /proc flagGravatar Shaobo2015-10-31
| * fix for deterministicExtractLoops for nested loopsGravatar Shuvendu Lahiri2015-10-27
| * Bug fix for deterministExtractLoops for Shaobo's exampleGravatar Shuvendu Lahiri2015-10-26
* | Modified translation so that z3 runs with type checking for simple binary ope...Gravatar Checkmate502015-10-14
| * updateGravatar Shaz Qadeer2015-09-28
* | Modified BigFloat to avoid evaluating the floating point value before sending...Gravatar Checkmate502015-09-23
* | Added initial support for float additionGravatar Checkmate502015-09-17
| * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2015-08-28
| |\
| * | Added /verifySnapshots:3, which prints recycled errors messages with the sour...Gravatar Rustan Leino2015-08-28
* | | Float type now works correctly for simple variable declaration and comparison.Gravatar Dietrich2015-07-20
| | * fix for /deterministicExtractLoops sed in SymDiffGravatar Shuvendu Lahiri2015-07-19
* | | Modified internal abstract float representation to allow user-defined mantiss...Gravatar Dietrich2015-07-13
| | * Update URL to boogie-partners to its new location on GitHub.Gravatar Dan Liew2015-06-28
| | * Fix issue #16 reported by @crazyktGravatar Dan Liew2015-06-28
| | * Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| | * Remove dead file.Gravatar Dan Liew2015-06-28
| | * fixed bug reported by ChrisGravatar qadeer2015-06-15
| | * adding z3name optionGravatar Ken McMillan2015-06-15
| | * Minor changesGravatar Valentin Wüstholz2015-06-12
| | * Fix issue with computation of statement checksums for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
| | * Fix issue in checksum computation for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
| | * various changes for duality from dead codeplex repoGravatar U-REDMOND\kenmcmil2015-06-09
| |/
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-08
| * Fix minor issue.Gravatar Valentin Wüstholz2015-06-05
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-05
* | added interpretation of floating point constants to the parserGravatar Dietrich2015-05-18
| * Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
| * Minor refactoringGravatar Valentin Wüstholz2015-05-17
| * Make caching of verification results more fine-grained for changes that affec...Gravatar Valentin Wüstholz2015-05-17
* | added decimal reading functionality to the float typeGravatar Dietrich2015-05-05
* | added general floating point mantissa and exponent managementGravatar Dietrich2015-05-04