Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | change to update | Checkmate50 | 2016-06-07 |
| | |||
* | removed an unnecessary type checking addition | Checkmate50 | 2016-06-07 |
| | |||
* | fixed some merging issues | Checkmate50 | 2016-06-07 |
| | |||
* | resolving conflicts | Checkmate50 | 2016-06-06 |
|\ | |||
* | | Merging complete. Everything looks good *crosses fingers* | Checkmate50 | 2016-06-06 |
| | | |||
* | | finished testing, fixed several minor compiler bugs | Checkmate50 | 2016-06-06 |
| | | |||
* | | Initial round of testing works with new syntax. Fixed an error where ↵ | Checkmate50 | 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 | akashlal | 2016-04-15 |
| | | | | | | | | namespaces remain the same. | ||
* | | modified floating point syntax and modified floating point constants to use ↵ | Checkmate50 | 2016-03-17 |
| | | | | | | | | bitvector values | ||
| * | Improve support for identifying unnecessary assumes. | Valentin Wüstholz | 2016-03-09 |
| | | |||
| * | Add support for weights on soft assumes. | Valentin Wüstholz | 2016-03-07 |
| | | |||
| * | Improve support for optimization and identifying unnecessary assumes. | Valentin Wüstholz | 2016-03-03 |
| | | |||
* | | Modified BigFloat and parser to accept correct SMT-LIB syntax | Checkmate50 | 2016-02-20 |
| | | |||
| * | Bug fix in determining whether a type parameter is bounded | qunyanm | 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 | Checkmate50 | 2016-01-04 |
| | | |||
| * | Minor change | Valentin Wüstholz | 2015-12-29 |
| | | |||
| * | Fix issue with ids for assume-statements. | Valentin Wüstholz | 2015-12-28 |
| | | |||
| * | Improve precision of abstract interpreter for modulo operations. | Valentin Wüstholz | 2015-12-28 |
| | | |||
| * | Enable optimization for more prover queries. | Valentin Wüstholz | 2015-12-27 |
| | | |||
| * | Remove unused file. | Valentin Wüstholz | 2015-12-03 |
| | | |||
| * | Remove workaround for older versions of Z3. | Valentin Wüstholz | 2015-12-02 |
| | | |||
| * | Use the EndCurly token when creating the ReturnCmd for unifiedExit | qunyanm | 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 | Checkmate50 | 2015-11-29 |
| | | |||
| * | Add simplified may-unverified analysis and instrumentation. | Valentin Wüstholz | 2015-11-20 |
| | | |||
| * | Fix issue with partially-verified assertions. | Valentin Wüstholz | 2015-11-19 |
| | | |||
| * | Minor changes | Valentin Wüstholz | 2015-11-19 |
| | | |||
| * | Add experimental support for optimization (requires Z3 build after changeset ↵ | Valentin Wüstholz | 2015-11-18 |
| | | | | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
| * | Fix issue #25. | Valentin Wüstholz | 2015-11-17 |
| | | |||
| * | Add support for identifying unnecessary assumes. | Valentin Wüstholz | 2015-11-16 |
| | | |||
| * | Document the new behaviour of the ``-proc:`` command line option | Dan Liew | 2015-10-31 |
| | | | | | | | | in the output of Boogie's help. | ||
| * | Added wild card matching for /proc flag | Shaobo | 2015-10-31 |
| | | |||
| * | Add support for annotating implementations with k-ind. depth. | Valentin Wüstholz | 2015-10-29 |
| | | |||
| * | fix for deterministicExtractLoops for nested loops | Shuvendu Lahiri | 2015-10-27 |
| | | |||
| * | Bug fix for deterministExtractLoops for Shaobo's example | Shuvendu Lahiri | 2015-10-26 |
| | | |||
| * | bug fix in the type checking of calls to atomic procedures | Shaz Qadeer | 2015-10-16 |
| | | |||
* | | Floating point constants given as integers are now translated correctly | Checkmate50 | 2015-10-14 |
| | | |||
* | | Modified translation so that z3 runs with type checking for simple binary ↵ | Checkmate50 | 2015-10-14 |
| | | | | | | | | operations | ||
| * | bug fix | Shaz Qadeer | 2015-10-09 |
| | | |||
| * | removed an extraneous warning | Shaz Qadeer | 2015-10-08 |
| | | |||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | Shaz Qadeer | 2015-10-01 |
| |\ | |||
| * | | added a fix to check all layers: created layer of actions or layers in | Shaz Qadeer | 2015-10-01 |
| | | | | | | | | | | | | requires, ensures, or asserts | ||
| | * | Improve output for diagnosing timeouts. | Valentin Wüstholz | 2015-10-01 |
| |/ | |||
| * | another fix requested by Chris | Shaz Qadeer | 2015-10-01 |
| | | | | | | | | verification is performed now for all created layers | ||
| * | Improve output for diagnosing timeouts. | Valentin Wüstholz | 2015-09-30 |
| | | |||
| * | update | Shaz Qadeer | 2015-09-28 |
| | | |||
| * | cleaned up some names | Shaz Qadeer | 2015-09-28 |
| | | |||
| * | a bug fix | Shaz Qadeer | 2015-09-27 |
| | | |||
| * | fixed a small bug | Shaz Qadeer | 2015-09-27 |
| | | |||
| * | removed a warning | Shaz Qadeer | 2015-09-26 |
| | | |||
| * | added introduced and ghost local variables | Shaz Qadeer | 2015-09-25 |
| | |