summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
* removed an unnecessary type checking additionGravatar Checkmate502016-06-07
|
* resolving conflictsGravatar Checkmate502016-06-06
|\
* | minor changesGravatar Checkmate502016-06-06
| |
* | Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
| |
* | spacing changeGravatar Checkmate502016-06-06
| |
* | Polished up the floats test folder. Preparing to rebaseGravatar Checkmate502016-06-06
| |
* | finished testing, fixed several minor compiler bugsGravatar Checkmate502016-06-06
| |
* | moved all the tests to the testing folderGravatar Checkmate502016-05-31
| |
| * Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
| |
| * Merge pull request #30 from qunyanm/type-parameter-bug-fixGravatar RustanLeino2016-02-12
| |\ | | | | | | Bug fix in determining whether a type parameter is bounded
| * | 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
| |
| * Improve precision of abstract interpreter for modulo operations.Gravatar Valentin Wüstholz2015-12-28
| |
| * 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.
| * Update test output for Z3 4.4.1.Gravatar Valentin Wüstholz2015-12-01
| |
| * 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
| |
| * 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
| |
| * Added test cases for the new asterisk wildcard behaviour of theGravatar Dan Liew2015-10-31
| | | | | | | | ``-proc`` command line argument.
| * 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
| |
| * another fix requested by ChrisGravatar Shaz Qadeer2015-10-01
| | | | | | | | verification is performed now for all created layers
| * fixed a small bugGravatar Shaz Qadeer2015-09-27
| |
| * added introduced and ghost local variablesGravatar Shaz Qadeer2015-09-25
| |
| * 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.
| | * Added another test.Gravatar Valentin Wüstholz2015-07-20
| | |
| | * Added more tests.Gravatar Valentin Wüstholz2015-07-20
| | |
| | * Try to unbreak the tests added inGravatar Dan Liew2015-06-28
| | | | | | | | | | | | 7f4e6b0fab58bb3028cd0f1734fc97b3feafefdf under Windows.
| | * 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.
| | * updated with Serdar's changesGravatar qadeer2015-06-25
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 07:57:25 +0000