summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
| | | * | 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
| |/ /
| | * Floating point constants given as integers are now translated correctlyGravatar Checkmate502015-10-14
| | |
| | * Modified translation so that z3 runs with type checking for simple binary ↵Gravatar Checkmate502015-10-14
| | | | | | | | | | | | operations
| * | 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
| | |
| | * Modified BigFloat to avoid evaluating the floating point value before ↵Gravatar Checkmate502015-09-23
| | | | | | | | | | | | sending it to z3
| | * Added initial support for float additionGravatar Checkmate502015-09-17
| | |
| * | 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.
| | | * Float type now works correctly for simple variable declaration and comparison.Gravatar Dietrich2015-07-20
| | | |
| | * | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Shuvendu Lahiri2015-07-20
| | |\ \
| | | * | Added another test.Gravatar Valentin Wüstholz2015-07-20
| | | | |
| | | * | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Akash Lal2015-07-20
| | | |\ \
| | | * | | Minor additions to VC genGravatar Akash Lal2015-07-20
| |_|/ / / |/| | | |
| | | * | Added more tests.Gravatar Valentin Wüstholz2015-07-20
| |_|/ / |/| | |
| | * | fix for /deterministicExtractLoops sed in SymDiffGravatar Shuvendu Lahiri2015-07-19
| |/ / |/| |
| | * Modified internal abstract float representation to allow user-defined ↵Gravatar Dietrich2015-07-13
| | | | | | | | | | | | mantissa and exponent
* | | Try to unbreak the tests added inGravatar Dan Liew2015-06-28
| | | | | | | | | | | | 7f4e6b0fab58bb3028cd0f1734fc97b3feafefdf under Windows.
* | | 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.
* | | Add travis file to gitattributes file.Gravatar Dan Liew2015-06-28
| | |
* | | 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.
* | | updated with Serdar's changesGravatar qadeer2015-06-25
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 19:16:14 +0000