summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
* White space deltas. (I'm not sure why git thought I had changes in these ↵Gravatar Rustan Leino2016-08-17
| | | | files, but I suspect it has to do with line endings.)
* Merge pull request #35 from Checkmate50/masterGravatar RustanLeino2016-08-17
|\ | | | | Floating Point Support
| * fixed an error where a -0 was not interpreted as a negative numberGravatar Checkmate502016-07-23
| |
| * corrected minor error in testGravatar Checkmate502016-07-22
| |
| * fixed the syntax on former tests and added two fp constant translation testsGravatar Checkmate502016-07-22
| |
| * fixed an issue with parsing floating pointsGravatar Checkmate502016-07-19
| |
| * Modified the float tests to match the updated syntaxGravatar Checkmate502016-07-19
| |
| * Added and briefly tested the updated syntax. NaN/oo not supported yetGravatar Checkmate502016-07-19
| |
* | updateGravatar Shaz Qadeer2016-07-19
| |
* | updateGravatar Shaz Qadeer2016-07-18
| |
| * Changed the syntax reading of the float typeGravatar Checkmate502016-07-16
| |
| * 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