summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Added the heap representation I was supposed to have started with... A genera...Gravatar mikebarnett2011-01-21
* Forgot to add file with last checkin.Gravatar mikebarnett2011-01-21
* Added a better options parsing by using functionality from MemberHelper.Gravatar mikebarnett2011-01-21
* Boogie: Made the algorithm for finding Z3 more robust.Gravatar wuestholz2011-01-21
* Boogie: Eliminated a couple of warnings by removing unused variable declarati...Gravatar wuestholz2011-01-21
* Fix order of getting the instance and the field from the expression heap so t...Gravatar mikebarnett2011-01-21
* Put back the prelude for the split fields heap that had been there before.Gravatar mikebarnett2011-01-21
* Use the interned key of field references, now that they have one.Gravatar mikebarnett2011-01-21
* Added a test for the split fields option.Gravatar mikebarnett2011-01-20
* Renamed outside of SVN, so added the renamed file and deleting this.Gravatar mikebarnett2011-01-20
* Moved the parts of the Prelude that depend on the heap representation into th...Gravatar mikebarnett2011-01-20
* Boogie build succeeded, 4 test(s) failedGravatar codeplexbot2011-01-20
* Make the SMTLIB backend work again, particularly with /typeEncoding:mGravatar MichalMoskal2011-01-19
* Ignore TPTP dllsGravatar MichalMoskal2011-01-19
* Fix a bug in distinct() encodingGravatar MichalMoskal2011-01-19
* More structuring of the different heap representations. Now each heap represe...Gravatar mikebarnett2011-01-19
* Removed HeapVariable from everywhere now that it is encapsulated in the Heap ...Gravatar mikebarnett2011-01-19
* Boogie build succeeded, 4 test(s) failedGravatar codeplexbot2011-01-19
* Removing resolution: there's no need to resolve field references in order to ...Gravatar mikebarnett2011-01-18
* The TPTP backend works for some very limited examplesGravatar MichalMoskal2011-01-18
* Copy SMTLib "prover" as a basis for TPTP "prover".Gravatar MichalMoskal2011-01-18
* The beginning of the encapsulation of the Heap representation so that we can ...Gravatar mikebarnett2011-01-17
* More user-friendly canonical namesGravatar MichalMoskal2011-01-17
* Fix translation of "null" so that it produces a type-correct value.Gravatar mikebarnett2011-01-16
* Don't use local variable names as canonical namesGravatar MichalMoskal2011-01-14
* Make the filename length limit be 30 (as in VCC)Gravatar MichalMoskal2011-01-14
* Boogie build succeeded, 4 test(s) failedGravatar codeplexbot2011-01-13
* Add description of {:selective_checking} to the /attrHelp. Fix the testcase.Gravatar MichalMoskal2011-01-13
* Display globals. Improve naming of function nodes in long ids.Gravatar MichalMoskal2011-01-13
* Display full name of node in tooltipGravatar MichalMoskal2011-01-13
* Dafny: Fixed some build issues with duplicated and malformed Code Contracts.Gravatar rustanleino2011-01-13
* Chalice: Applied patch 7685, this fixes a small bug that duplicated members a...Gravatar alexanderjsummers2011-01-12
* Applied patch 7636 - this fixes workitem 9978Gravatar alexanderjsummers2011-01-12
* Dafny: Fixed error in printing an error message. Changed "function method" ...Gravatar rustanleino2011-01-11
* Boogie build succeeded, 5 test(s) failedGravatar codeplexbot2011-01-11
* Boogie build succeeded, 1 test(s) failedGravatar codeplexbot2011-01-10
* Boogie: Updated 'PrepareBoogieZip.ba?t'.Gravatar wuestholz2011-01-10
* Boogie build succeeded, 1 test(s) failedGravatar codeplexbot2011-01-10
* Display casted pointersGravatar MichalMoskal2011-01-04
* 1. Converted assume to assert for the source infoGravatar qadeer2010-12-21
* stratified inlining: minor fix to the call tree being savedGravatar akashlal2010-12-21
* Changed attribute names in the BPL for source context assumption statements.Gravatar mikebarnett2010-12-21
* Use an explicit PdbReader instead of the more general ISourceLocationProvider...Gravatar mikebarnett2010-12-21
* added support for array translation.Gravatar qadeer2010-12-20
* fixed a small bug in inline codeGravatar qadeer2010-12-20
* Generate "assume {:filename "foo.cs"}{:line 3} true" statements for each stat...Gravatar mikebarnett2010-12-20
* Translate boolean types into Bpl.Type.Bool.Gravatar mikebarnett2010-12-20
* stratified inlining: record the name of the main procedure.Gravatar akashlal2010-12-18
* Improve handling of arrays embedded in structsGravatar MichalMoskal2010-12-17
* Add new feature: {:selective_checking} on procedures. See testcase for a desc...Gravatar MichalMoskal2010-12-17