summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Run Boogie code on threads with large stacksGravatar BarryBo2016-07-22
| | | | | | | Replace TaskScheduler.Default by a custom TaskScheduler. The .Default uses threadpool threads whose stack size is controlled by the host EXE header. The new ThreadTaskScheduler give Boogie control over the stack size, and defaults to 16mb.
* Rename DLLs to non-generic names by prefixing "Boogie". Project names andGravatar akashlal2016-04-15
| | | | namespaces remain the same.
* 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 00:48:29 +0000