Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | rebuilt scanner and parser via coco | Checkmate50 | 2016-07-16 |
| | |||
* | 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 |
|\ | |||
* | | minor changes | Checkmate50 | 2016-06-06 |
| | | |||
* | | Merging complete. Everything looks good *crosses fingers* | Checkmate50 | 2016-06-06 |
| | | |||
* | | spacing change | Checkmate50 | 2016-06-06 |
| | | |||
* | | removed an unnecessary text file | Checkmate50 | 2016-06-06 |
| | | |||
* | | Polished up the floats test folder. Preparing to rebase | Checkmate50 | 2016-06-06 |
| | | |||
* | | finished testing, fixed several minor compiler bugs | Checkmate50 | 2016-06-06 |
| | | |||
* | | moved all the tests to the testing folder | Checkmate50 | 2016-05-31 |
| | | |||
* | | 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 | ||
| * | Add links to new documentation (not yet complete). | Dan Liew | 2016-04-20 |
| | | |||
| * | 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 |
| | | |||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | Rustan Leino | 2016-02-12 |
| |\ | |||
| | * | Merge pull request #30 from qunyanm/type-parameter-bug-fix | RustanLeino | 2016-02-12 |
| | |\ | | | | | | | | | Bug fix in determining whether a type parameter is bounded | ||
| * | | | Merge branch 'master' of https://github.com/boogie-org/boogie | Rustan Leino | 2016-02-12 |
| |\| | | |||
| * | | | (Honestly, I don't know what I'm doing. I'm trying to revert these changes, ↵ | Rustan Leino | 2016-02-12 |
| | | | | | | | | | | | | | | | | but Git doesn't actually say what sort of commit I'm doing. Well, here goes.) | ||
| | * | | added an example | Shaz Qadeer | 2016-02-09 |
| | | | | |||
| | * | | another fix | Shaz Qadeer | 2016-01-26 |
| | | | | |||
| | * | | improved some of the annotations | Shaz Qadeer | 2016-01-21 |
| | | | | |||
| | * | | some fixes | Shaz Qadeer | 2016-01-19 |
| | | | | |||
| | | * | 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. | ||
| | * | updated the example to implement the allocation of thread identifiers; | Shaz Qadeer | 2016-01-17 |
| | | | | | | | | | | | | | | | this example provides another illustration of abstracting ordinary variables by linear variables | ||
| | * | fixed a small problem in the precondition for FreeLinear | Shaz Qadeer | 2016-01-10 |
| | | | |||
| | * | added Free code | Shaz Qadeer | 2016-01-08 |
| | | | |||
* | | | 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 |
| | | | |||
| | * | Merge branch 'master' of https://github.com/boogie-org/boogie | qunyanm | 2015-12-15 |
| | |\ | |||
| | | * | Remove unused file. | Valentin Wüstholz | 2015-12-03 |
| | | | | |||
| | | * | Remove unused directory. | Valentin Wüstholz | 2015-12-03 |
| | | | | |||
| | | * | Remove workaround for older versions of Z3. | Valentin Wüstholz | 2015-12-02 |
| | | | | |||
| | | * | TravisCI build icon should only show build status for master branch, not | Dan Liew | 2015-12-02 |
| | | | | | | | | | | | | | | | | all branches. | ||
| | | * | Merge pull request #24 from boogie-org/dafny-bug-fix | Dan Liew | 2015-12-02 |
| | | |\ | | | | | | | | | | | Dafny bug fix | ||
| | | | * | 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. | ||
| | | * | Merge pull request #27 from boogie-org/update_recommended_Z3_version | Valentin Wüstholz | 2015-12-01 |
| | | |\ | | | | | | | | | | | Update recommended z3 version | ||
| | | | * | Update test output for Z3 4.4.1. | Valentin Wüstholz | 2015-12-01 |
| | | | | | |||
| | | | * | Teach TravisCI to use Z3 4.4.1 from repositories that I'm currently | Dan Liew | 2015-12-01 |
| | | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | maintaining on the OpenSUSE build service. See https://build.opensuse.org/package/show/home:delcypher:z3/z3 | ||
* | | | | Special fp types (such as infinity and NaN are now translated by boogie | Checkmate50 | 2015-11-29 |
| | | | | |||
| | * | | Merge remote-tracking branch 'refs/remotes/origin/dafny-bug-fix' | qunyanm | 2015-11-25 |
| | |\ \ | |||
| | * \ \ | Merge remote-tracking branch 'refs/remotes/origin/dafny-bug-fix' | qunyanm | 2015-11-25 |
| | |\ \ \ | | | |_|/ | | |/| | |