summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* 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
|
* 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.
* 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
|
* Remove unused file.Gravatar Valentin Wüstholz2015-12-03
|
* Remove workaround for older versions of Z3.Gravatar Valentin Wüstholz2015-12-02
|
* 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.
* 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
|
* Minor changesGravatar Valentin Wüstholz2015-11-19
|
* Add experimental support for optimization (requires Z3 build after changeset ↵Gravatar Valentin Wüstholz2015-11-18
| | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
* Fix issue #25.Gravatar Valentin Wüstholz2015-11-17
|
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
|
* Document the new behaviour of the ``-proc:`` command line optionGravatar Dan Liew2015-10-31
| | | | in the output of Boogie's help.
* 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
|
* 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
|
* a bug fixGravatar Shaz Qadeer2015-09-27
|
* fixed a small bugGravatar Shaz Qadeer2015-09-27
|
* removed a warningGravatar Shaz Qadeer2015-09-26
|
* added introduced and ghost local variablesGravatar Shaz Qadeer2015-09-25
|
* fixed my earlier to make it nicerGravatar Shaz Qadeer2015-09-03
|
* fixed a crash when there is no collectorGravatar Shaz Qadeer2015-09-02
|
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2015-08-28
|\ | | | | | | | | | | | | | | | | | | Conflicts: Source/Core/CommandLineOptions.cs Source/ExecutionEngine/ExecutionEngine.cs Source/ExecutionEngine/VerificationResultCache.cs Source/VCGeneration/VC.cs Test/snapshots/runtest.snapshot Test/snapshots/runtest.snapshot.expect
* | Added /verifySnapshots:3, which prints recycled errors messages with the ↵Gravatar Rustan Leino2015-08-28
| | | | | | | | source locations of the new code.
| * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Shuvendu Lahiri2015-07-20
| |\
| | * Minor additions to VC genGravatar Akash Lal2015-07-20
| | |
| * | fix for /deterministicExtractLoops sed in SymDiffGravatar Shuvendu Lahiri2015-07-19
| |/
| * Update URL to boogie-partners to its new location on GitHub.Gravatar Dan Liew2015-06-28
| |
| * Fix issue #16 reported by @crazyktGravatar Dan Liew2015-06-28
| | | | | | | | | | | | | | | | | | | | Previously when Boogie was passed the ``-proc:<NAME>`` argument on the command line it would verify any procedure whose name contained ``<NAME>`` which doesn't seem like correct behaviour. Now Boogie only tries to verify a procedure only if its name matches ``<NAME>`` exactly. I've added several test cases to check Boogie behaves as expected.
| * Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| | | | | | | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
| * Remove dead file.Gravatar Dan Liew2015-06-28
| |
| * removed a stray Console.WriteLine that Ken had earlier checked in byGravatar qadeer2015-06-25
| | | | | | | | mistake.
| * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar akashlal2015-06-20
| |\
| * | Fix for reading fixpoint back into boogie exprsGravatar akashlal2015-06-20
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 20:17:14 +0000