Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Added and briefly tested the updated syntax. NaN/oo not supported yet | 2016-07-19 | |
| | |||
* | Changed the syntax reading of the float type | 2016-07-16 | |
| | |||
* | rebuilt scanner and parser via coco | 2016-07-16 | |
| | |||
* | change to update | 2016-06-07 | |
| | |||
* | removed an unnecessary type checking addition | 2016-06-07 | |
| | |||
* | fixed some merging issues | 2016-06-07 | |
| | |||
* | resolving conflicts | 2016-06-06 | |
|\ | |||
* | | Merging complete. Everything looks good *crosses fingers* | 2016-06-06 | |
| | | |||
* | | finished testing, fixed several minor compiler bugs | 2016-06-06 | |
| | | |||
* | | Initial round of testing works with new syntax. Fixed an error where ↵ | 2016-05-31 | |
| | | | | | | | | floating points could not be given as a function argument | ||
| * | Rename DLLs to non-generic names by prefixing "Boogie". Project names and | 2016-04-15 | |
| | | | | | | | | namespaces remain the same. | ||
* | | modified floating point syntax and modified floating point constants to use ↵ | 2016-03-17 | |
| | | | | | | | | bitvector values | ||
| * | Improve support for identifying unnecessary assumes. | 2016-03-09 | |
| | | |||
| * | Add support for weights on soft assumes. | 2016-03-07 | |
| | | |||
| * | Improve support for optimization and identifying unnecessary assumes. | 2016-03-03 | |
| | | |||
* | | Modified BigFloat and parser to accept correct SMT-LIB syntax | 2016-02-20 | |
| | | |||
| * | Bug fix in determining whether a type parameter is bounded | 2016-01-19 | |
| | | | | | | | | | | | | When checking whether a type parameter could be determined from the bound variable types, we mistakenly compare equality between a TypeVarable and a VCExprVar, instead of between two VCExprVars. | ||
* | | Added several test cases and some basic documentation for fp usage | 2016-01-04 | |
| | | |||
| * | Minor change | 2015-12-29 | |
| | | |||
| * | Fix issue with ids for assume-statements. | 2015-12-28 | |
| | | |||
| * | Improve precision of abstract interpreter for modulo operations. | 2015-12-28 | |
| | | |||
| * | Enable optimization for more prover queries. | 2015-12-27 | |
| | | |||
| * | Remove unused file. | 2015-12-03 | |
| | | |||
| * | Remove workaround for older versions of Z3. | 2015-12-02 | |
| | | |||
| * | Use the EndCurly token when creating the ReturnCmd for unifiedExit | 2015-12-02 | |
| | | | | | | | | | | | | | | | | When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block. | ||
* | | Special fp types (such as infinity and NaN are now translated by boogie | 2015-11-29 | |
| | | |||
| * | Add simplified may-unverified analysis and instrumentation. | 2015-11-20 | |
| | | |||
| * | Fix issue with partially-verified assertions. | 2015-11-19 | |
| | | |||
| * | Minor changes | 2015-11-19 | |
| | | |||
| * | Add experimental support for optimization (requires Z3 build after changeset ↵ | 2015-11-18 | |
| | | | | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
| * | Fix issue #25. | 2015-11-17 | |
| | | |||
| * | Add support for identifying unnecessary assumes. | 2015-11-16 | |
| | | |||
| * | Document the new behaviour of the ``-proc:`` command line option | 2015-10-31 | |
| | | | | | | | | in the output of Boogie's help. | ||
| * | Added wild card matching for /proc flag | 2015-10-31 | |
| | | |||
| * | Add support for annotating implementations with k-ind. depth. | 2015-10-29 | |
| | | |||
| * | fix for deterministicExtractLoops for nested loops | 2015-10-27 | |
| | | |||
| * | Bug fix for deterministExtractLoops for Shaobo's example | 2015-10-26 | |
| | | |||
| * | bug fix in the type checking of calls to atomic procedures | 2015-10-16 | |
| | | |||
* | | Floating point constants given as integers are now translated correctly | 2015-10-14 | |
| | | |||
* | | Modified translation so that z3 runs with type checking for simple binary ↵ | 2015-10-14 | |
| | | | | | | | | operations | ||
| * | bug fix | 2015-10-09 | |
| | | |||
| * | removed an extraneous warning | 2015-10-08 | |
| | | |||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-10-01 | |
| |\ | |||
| * | | added a fix to check all layers: created layer of actions or layers in | 2015-10-01 | |
| | | | | | | | | | | | | requires, ensures, or asserts | ||
| | * | Improve output for diagnosing timeouts. | 2015-10-01 | |
| |/ | |||
| * | another fix requested by Chris | 2015-10-01 | |
| | | | | | | | | verification is performed now for all created layers | ||
| * | Improve output for diagnosing timeouts. | 2015-09-30 | |
| | | |||
| * | update | 2015-09-28 | |
| | | |||
| * | cleaned up some names | 2015-09-28 | |
| | | |||
| * | a bug fix | 2015-09-27 | |
| | |