summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
...
* | 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
| | |
| * | added another sampleGravatar qadeer2015-06-17
| | |
| * | modified desugaring so that in commutatitivity checks copies of originalGravatar qadeer2015-06-17
| | | | | | | | | | | | codeexpr is made.
| * | fixed bug reported by ChrisGravatar qadeer2015-06-15
| | |
| * | Fix issue with computation of statement checksums for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
| | |
| * | Add a test case.Gravatar Valentin Wüstholz2015-06-12
| | |
| * | relaxed the check for created and hidden layers for skip actionsGravatar qadeer2015-06-10
| | |
| * | fixed crashGravatar qadeer2015-06-10
|/ /
* | bug fix in popGravatar qadeer2015-05-27
| |
* | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar qadeer2015-05-20
|\ \
* | | added more specificationsGravatar qadeer2015-05-20
| | |
| * | Make caching of verification results more fine-grained for changes that ↵Gravatar Valentin Wüstholz2015-05-17
| | | | | | | | | | | | affect preconditions.
| * | SecureVC: exampleGravatar Akash Lal2015-05-07
| | |
| * | Make it preserve the fact that the value of an assumption variable never ↵Gravatar Valentin Wüstholz2015-05-06
| | | | | | | | | | | | becomes logically weaker after a havoc.
| * | Add support for 'verified_under' attributes on procedure calls and invariants.Gravatar Valentin Wüstholz2015-04-29
| | |
| | * Began adding the float type to VC expressionGravatar Dietrich2015-04-27
| | |
| * | Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has aGravatar Dan Liew2015-04-26
|/ / | | | | | | | | variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error
* | renamed og to civlGravatar qadeer2015-04-22
| |
* | added more examplesGravatar qadeer2015-04-18
| |
* | patched ghost checkingGravatar qadeer2015-04-18
| |
* | changed aux attribute to ghostGravatar qadeer2015-04-18
| |
| * Added the fp32 class, copied from the previously existing BigDec class. No ↵Gravatar Dietrich2015-04-17
| | | | | | | | significant changes from BigDec have been made
* | first check inGravatar qadeer2015-04-16
|/
* Disable test is ``Test/Secure``. They aren't set up properly.Gravatar Dan Liew2015-04-05
|
* Some test cases for SecureVCGen (disabled for lit currently)Gravatar akashlal2015-04-05
|
* Fix ``Test/test15/CaptureState.bpl`` test under Linux.Gravatar Dan Liew2015-04-03
|
* Fix ``livevars/daytona_bug2_ioctl_example_2.bpl`` test under Linux.Gravatar Dan Liew2015-04-03
|
* updated the example to include atomic specifications (sent by Suha)Gravatar qadeer2015-03-29
|
* fixed crash reported by Dan.Gravatar qadeer2015-03-02
| | | | DoModSetAnalysis needs to run before the linear and mover type checking.
* fix from Serdar and SuhaGravatar qadeer2015-02-24
|
* moved some things aroundGravatar qadeer2015-02-11
|
* minor fix to the golden fileGravatar qadeer2015-01-28
|
* added lit stuff at the top of the file and the golden outputGravatar qadeer2015-01-28
|
* Work stealing queue (PLDI '12 Vechev et al.)Gravatar Unknown2015-01-28
|
* MergeGravatar qadeer2015-01-27
|\
* | removed unused functions and axioms to make the verification fasterGravatar qadeer2015-01-27
| |
| * Worked on the verification result caching (use weights for extracted functions).Gravatar wuestholz2015-01-24
| |
| * Worked on the verification result caching (use native support for partially ↵Gravatar wuestholz2015-01-16
|/ | | | verified assertions).
* Added a test and a todo.Gravatar wuestholz2015-01-02
|
* Minor change in verification result caching (extracted functions)Gravatar wuestholz2014-12-28
|