summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
* 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
|
* 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
|
* strengthened type checkingGravatar qadeer2014-12-26
| | | | | cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions
* changed type checking of yield procedures so that they can only call other ↵Gravatar qadeer2014-12-18
| | | | yielding procedures
* 1. made variable introduction layer explicit in the test casesGravatar qadeer2014-12-15
| | | | 2. if a single layer is specified for a global variable, that layer is the introduction layer
* patched an expected outputGravatar qadeer2014-12-15
|
* Worked on the verification result caching (extracted functions).Gravatar wuestholz2014-11-25
|
* Fixed issues in the verification result caching (old expressions).Gravatar wuestholz2014-11-24
|
* Fixed issue in the verification result caching.Gravatar wuestholz2014-11-10
|
* Worked on the verification result caching.Gravatar wuestholz2014-11-10
|
* Made it never include the statement checksum when printing assert statements.Gravatar wuestholz2014-11-16
|
* updateGravatar qadeer2014-11-14
|
* renamed :phase to :layerGravatar qadeer2014-11-14
|
* added golden outputGravatar qadeer2014-11-08
|
* more minor fix to test case houdini\testUnsatCore.bplGravatar shuvendu2014-11-07
|
* minor fix to test case houdini\testUnsatCore.bplGravatar shuvendu2014-11-07
|
* re-enabling -useUnsatCoreForContractInferGravatar shuvendu2014-11-07
| | | | An example houdini\testUnsatCore.bpl to test out the unsatCore (Currently seems to be not working)
* Worked on the verification result caching.Gravatar wuestholz2014-11-03
|
* Did some refactoring.Gravatar wuestholz2014-11-02
|
* Added a test for the verification result caching.Gravatar wuestholz2014-10-29
|
* MergeGravatar qadeer2014-10-21
|\
* | removed a useless procedureGravatar qadeer2014-10-21
| |
| * Worked on the verification result caching.Gravatar wuestholz2014-10-19
| |
| * Added more tests for the verification result caching.Gravatar wuestholz2014-10-19
| |
| * Worked on the verification result caching.Gravatar wuestholz2014-10-19
| |
| * Did some refactoring.Gravatar wuestholz2014-10-18
| |
| * Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-10-18
| |
| * Worked on the verification result caching.Gravatar wuestholz2014-10-17
| |
| * Worked on the verification result caching.Gravatar wuestholz2014-10-15
|/