summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* 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
| * Document the new behaviour of the ``-proc:`` command line optionGravatar Dan Liew2015-10-31
| | | | | | | | in the output of Boogie's help.
| * Added test cases for the new asterisk wildcard behaviour of theGravatar Dan Liew2015-10-31
| | | | | | | | ``-proc`` command line argument.
| * Added wild card matching for /proc flagGravatar Shaobo2015-10-31
|/
* Add support for annotating implementations with k-ind. depth.Gravatar Valentin Wüstholz2015-10-29
|
* fix for deterministicExtractLoops for nested loopsGravatar Shuvendu Lahiri2015-10-27
|
* fixedGravatar Shaz Qadeer2015-10-26
|
* Bug fix for deterministExtractLoops for Shaobo's exampleGravatar Shuvendu Lahiri2015-10-26
|
* bug fix in the type checking of calls to atomic proceduresGravatar Shaz Qadeer2015-10-16
|
* bug fixGravatar Shaz Qadeer2015-10-09
|
* removed an extraneous warningGravatar Shaz Qadeer2015-10-08
|
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Shaz Qadeer2015-10-01
|\
* | added a fix to check all layers: created layer of actions or layers inGravatar Shaz Qadeer2015-10-01
| | | | | | | | requires, ensures, or asserts
| * Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-10-01
|/
* another fix requested by ChrisGravatar Shaz Qadeer2015-10-01
| | | | verification is performed now for all created layers
* Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-09-30
|
* updateGravatar Shaz Qadeer2015-09-28
|
* cleaned up some namesGravatar Shaz Qadeer2015-09-28
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-12 13:48:03 +0000