Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | Package Boogie programs for experimental | Benjamin Barenblat | 2016-04-01 | |
| | | | | ||||
* | | | | Package Boogie library for experimental | Benjamin Barenblat | 2016-04-01 | |
|/ / / | ||||
* | | | Make DFSG-clean | Benjamin Barenblat | 2016-03-31 | |
| | | | ||||
| | * | 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 | |
| | |\ \ \ \ | | | |_|/ / | | |/| | | | ||||
| | | | * | | Use the EndCurly token when creating the ReturnCmd for unifiedExit | qunyanm | 2015-11-25 | |
| | | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | |||
| | * | | | Teach the TravisCI build to use the ``travis_retry`` command when | Dan Liew | 2015-11-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | using NuGet. The motivation here is that the ``nuget`` command is a little flakey (sometimes it times out) in the legacy TravisCI infrastructure. This command will retry the command passed to it a few times. Hopefully this will stop the random build failures we've been having. | |||
| | * | | | 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 | |
| | | | | | ||||
| | * | | | Update test output after Nikolaj's enhancement in Z3. | Valentin Wüstholz | 2015-11-19 | |
| | | | | | ||||
| | * | | | Add a test. | Valentin Wüstholz | 2015-11-19 | |
| | | | | | ||||
| | * | | | Minor changes | Valentin Wüstholz | 2015-11-19 | |
| | | | | | ||||
| | * | | | Improve experimental support for optimization (requires Z3 changeset ↵ | Valentin Wüstholz | 2015-11-18 | |
| | | | | | | | | | | | | | | | | | | | | 5948013b1b04d8529bce366c0c7b87e1d88a1827 or later). | |||
| | * | | | Add experimental support for optimization (requires Z3 build after changeset ↵ | Valentin Wüstholz | 2015-11-18 | |
| | | | | | | | | | | | | | | | | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | |||
| | * | | | Fix test output. | Valentin Wüstholz | 2015-11-17 | |
| | | | | | ||||
| | * | | | Fix issue #25. | Valentin Wüstholz | 2015-11-17 | |
| | | | | | ||||
| | | * | | Use EndCurly token for the ReturnCmd when creating unifiedExit | qunyanm | 2015-11-16 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | Instead of using NoToken for the ReturnCmd, use the EndCurly, if it exists, when creating unifiedExit |