summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* 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
* 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
| * 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
* Fix duplicator so that BVConcatExpr and BVExtractExpr are handled. Patch by ...Gravatar Ally Donaldson2014-03-12
* Fix to predicationGravatar Ally Donaldson2014-03-05
* MergeGravatar Rustan Leino2014-02-28
|\
* | Changed all lambda-expression rewriting to be done as a pre-processing step b...Gravatar Rustan Leino2014-02-28
| * Added a fix to inlining so that it becomes cognizant of procedures that the u...Gravatar qadeer2014-02-28
| * Added /trustNonInterference optionGravatar qadeer2014-02-28
* | Changed return type of VisitLambdaExpr to just ExprGravatar Rustan Leino2014-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 11:36:44 +0000