summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* | Enable Linear inequality lit tests.Gravatar Dan Liew2014-05-07
* | For lit test infrastructure, disable running tests inGravatar Dan Liew2014-05-07
* | Enable the Constant propagation tests as lit tests.Gravatar Dan Liew2014-05-07
* | Enabled "Verify Boogie 2" lit tests. Note the following tests failGravatar Dan Liew2014-05-07
* | Enabled tests for types introduced in Boogie2 as lit tests.Gravatar Dan Liew2014-05-07
* | Enable the VCVariety.BlockNested tests as lit tests.Gravatar Dan Liew2014-05-07
* | Enabled VC Generation lit tests.Gravatar Dan Liew2014-05-07
* | For lit tests running on Windows pass /W flag to the fc toolGravatar Dan Liew2014-05-06
* | Enabled lit tests for test1/ directoryGravatar Dan Liew2014-05-06
| * Merge extra recuresion bound changes for FixedPointVCGravatar Ken McMillan2014-04-21
| |\
* | | Teach the ExecutionEngine to respect the -useBaseNameForFileName commandlineGravatar Dan Liew2014-04-09
* | | Enabled most of the name resolution lit tests. They don't all passGravatar Dan Liew2014-05-05
* | | Converted textbook tests to lit tests.Gravatar Dan Liew2014-04-08
* | | Add lit.local.cfg that instructs not to run any tests in thisGravatar Dan Liew2014-05-05
* | | Pass -useBaseNameForFileName option to Boogie when running tests.Gravatar Dan Liew2014-04-06
* | | Added /useBaseNameForFile command line argument. The ScannerGravatar Dan Liew2014-04-06
* | | Enable houdini lit tests. Note some still fail due to BoogieGravatar Dan Liew2014-05-05
* | | Added basic lit configuration file for running tests.Gravatar Dan Liew2014-04-06
* | | a bug fixGravatar qadeer2014-05-07
* | | added {:aux} attribute to local variablesGravatar qadeer2014-05-07
* | | minor fixGravatar qadeer2014-05-05
* | | third checkpoint (refactored more code)Gravatar qadeer2014-05-05
* | | example for variable introduction addedGravatar qadeer2014-05-04
* | | second checkpointGravatar qadeer2014-05-04
* | | checkpointGravatar qadeer2014-05-03
* | | bug fix in the last updateGravatar qadeer2014-04-25
* | | updated the mover checksGravatar qadeer2014-04-25
* | | Add support for assumption variables.Gravatar wuestholz2014-04-21
* | | added another sampleGravatar qadeer2014-04-20
* | | added simulation relation computation to yield type checkingGravatar qadeer2014-04-20
* | | fixed some bugs in the previous check insGravatar qadeer2014-04-16
* | | added the framing for the refinement checkGravatar qadeer2014-04-16
* | | MergeGravatar qadeer2014-04-16
|\ \ \
* | | | added variable hidingGravatar qadeer2014-04-16
| * | | Minor fix to abshoudiniGravatar akashlal2014-04-16
| * | | Fixed malformed Contracts sectionGravatar Rustan Leino2014-04-15
| | | * Added extra recursion bound and preconditions to FixedpointVC.Gravatar Ken McMillan2014-03-17
| * | | disabled quantifier merging, except when no triggers are provided (as discuss...Gravatar Unknown2014-03-03
|/ / /
* | | MergeGravatar qadeer2014-04-15
|\| |
* | | added more types to constructed expressionsGravatar qadeer2014-04-15
| * | Merge changes for /printFixedPoint optionGravatar Ken McMillan2014-04-14
|/| |
| * | Added /printFixedPoint optionGravatar Ken McMillan2014-04-14
* | | resolved expressions created during generation of procedures for mover checksGravatar qadeer2014-04-14
* | | Fixed abstract interpretation for realsGravatar Rustan Leino2014-04-13
|/ /
* | Fixed bug in abstract interpretation over realsGravatar Rustan Leino2014-04-08
* | Added option to avoid unrolling irreducible loopsGravatar akashlal2014-04-06
* | Fixed class cast issue with type synonymsGravatar Ally Donaldson2014-04-01
* | Fixes to predication. Patch by Jeroen Ketema.Gravatar Ally Donaldson2014-03-18
* | Change class 'LambdaVisitor' to attach checksum to expanded lambda functions.Gravatar wuestholz2014-03-17
* | More exhaustive generation of assertions during predication. Patch by Jeroen...Gravatar Ally Donaldson2014-03-14