summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Merge branch 'upstream' into dfsg_freeGravatar Benjamin Barenblat2016-06-05
|\
* | Make DFSG-cleanGravatar Benjamin Barenblat2016-03-31
| |
| * Improve support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-09
| |
| * Add support for weights on soft assumes.Gravatar Valentin Wüstholz2016-03-07
| |
| * Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
| |
| * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2016-02-12
| |\
| | * Merge pull request #30 from qunyanm/type-parameter-bug-fixGravatar RustanLeino2016-02-12
| | |\ | | | | | | | | Bug fix in determining whether a type parameter is bounded
| * | | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2016-02-12
| |\| |
| * | | (Honestly, I don't know what I'm doing. I'm trying to revert these changes, ↵Gravatar Rustan Leino2016-02-12
| | | | | | | | | | | | | | | | but Git doesn't actually say what sort of commit I'm doing. Well, here goes.)
| | * | added an exampleGravatar Shaz Qadeer2016-02-09
| | | |
| | * | another fixGravatar Shaz Qadeer2016-01-26
| | | |
| | * | improved some of the annotationsGravatar Shaz Qadeer2016-01-21
| | | |
| | * | some fixesGravatar Shaz Qadeer2016-01-19
| | | |
| | | * Bug fix in determining whether a type parameter is boundedGravatar qunyanm2016-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;Gravatar Shaz Qadeer2016-01-17
| | | | | | | | | | | | | | | this example provides another illustration of abstracting ordinary variables by linear variables
| | * fixed a small problem in the precondition for FreeLinearGravatar Shaz Qadeer2016-01-10
| | |
| | * added Free codeGravatar Shaz Qadeer2016-01-08
| | |
| | * Minor changeGravatar Valentin Wüstholz2015-12-29
| | |
| | * Fix issue with ids for assume-statements.Gravatar Valentin Wüstholz2015-12-28
| | |
| | * Improve precision of abstract interpreter for modulo operations.Gravatar Valentin Wüstholz2015-12-28
| | |
| | * Enable optimization for more prover queries.Gravatar Valentin Wüstholz2015-12-27
| | |
| | * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar qunyanm2015-12-15
| | |\
| | | * Remove unused file.Gravatar Valentin Wüstholz2015-12-03
| | | |
| | | * Remove unused directory.Gravatar Valentin Wüstholz2015-12-03
| | | |
| | | * Remove workaround for older versions of Z3.Gravatar Valentin Wüstholz2015-12-02
| | | |
| | | * TravisCI build icon should only show build status for master branch, notGravatar Dan Liew2015-12-02
| | | | | | | | | | | | | | | | all branches.
| | | * Merge pull request #24 from boogie-org/dafny-bug-fixGravatar Dan Liew2015-12-02
| | | |\ | | | | | | | | | | Dafny bug fix
| | | | * Use the EndCurly token when creating the ReturnCmd for unifiedExitGravatar qunyanm2015-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_versionGravatar Valentin Wüstholz2015-12-01
| | | |\ | | | | | | | | | | Update recommended z3 version
| | | | * Update test output for Z3 4.4.1.Gravatar Valentin Wüstholz2015-12-01
| | | | |
| | | | * Teach TravisCI to use Z3 4.4.1 from repositories that I'm currentlyGravatar Dan Liew2015-12-01
| | | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | maintaining on the OpenSUSE build service. See https://build.opensuse.org/package/show/home:delcypher:z3/z3
| | * | Merge remote-tracking branch 'refs/remotes/origin/dafny-bug-fix'Gravatar qunyanm2015-11-25
| | |\ \
| | * \ \ Merge remote-tracking branch 'refs/remotes/origin/dafny-bug-fix'Gravatar qunyanm2015-11-25
| | |\ \ \ | | | |_|/ | | |/| |
| | | | * Use the EndCurly token when creating the ReturnCmd for unifiedExitGravatar qunyanm2015-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 whenGravatar Dan Liew2015-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.Gravatar Valentin Wüstholz2015-11-20
| | | |
| | * | Fix issue with partially-verified assertions.Gravatar Valentin Wüstholz2015-11-19
| | | |
| | * | Update test output after Nikolaj's enhancement in Z3.Gravatar Valentin Wüstholz2015-11-19
| | | |
| | * | Add a test.Gravatar Valentin Wüstholz2015-11-19
| | | |
| | * | Minor changesGravatar Valentin Wüstholz2015-11-19
| | | |
| | * | Improve experimental support for optimization (requires Z3 changeset ↵Gravatar Valentin Wüstholz2015-11-18
| | | | | | | | | | | | | | | | 5948013b1b04d8529bce366c0c7b87e1d88a1827 or later).
| | * | Add experimental support for optimization (requires Z3 build after changeset ↵Gravatar Valentin Wüstholz2015-11-18
| | | | | | | | | | | | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
| | * | Fix test output.Gravatar Valentin Wüstholz2015-11-17
| | | |
| | * | Fix issue #25.Gravatar Valentin Wüstholz2015-11-17
| | | |
| | | * Use EndCurly token for the ReturnCmd when creating unifiedExitGravatar qunyanm2015-11-16
| | | | | | | | | | | | | | | | | | | | Instead of using NoToken for the ReturnCmd, use the EndCurly, if it exists, when creating unifiedExit
| | | * Use EndCurly token for the ReturnCmd when creating unifiedExitGravatar qunyanm2015-11-16
| | | | | | | | | | | | | | | | | | | | Instead of using NoToken for the ReturnCmd, use the EndCurly when creating unifiedExit.
| | * | Add a test.Gravatar Valentin Wüstholz2015-11-16
| | |/
| | * Add a test.Gravatar Valentin Wüstholz2015-11-16
| | |
| | * Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
| | |
| | * Merge pull request #22 from delcypher/proc_flag_fixGravatar Dan Liew2015-11-02
| | |\ | | | | | | | | Proc flag fix which addresses #16
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 10:21:46 +0000