summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* VS 2010 mode for Chalice: some errors didn't show up in the window because po...Gravatar kyessenov2010-08-20
* Boogie: Fixed a few contracts errorsGravatar tabarbe2010-08-19
* Boogie: Removed and completed a task commentGravatar tabarbe2010-08-19
* Boogie: Removed and completed a task commentGravatar tabarbe2010-08-19
* Boogie: Removed a completed task comment, added a forgotten Contract.EnsuresO...Gravatar tabarbe2010-08-19
* Boogie: Removed a completed task commentGravatar tabarbe2010-08-19
* Boogie: Removed a completed task commentGravatar tabarbe2010-08-19
* Boogie: Removed an old task commentGravatar tabarbe2010-08-19
* Chalice: more regression tests; cosmetic changes to codeGravatar kyessenov2010-08-19
* Added recursion-bound-guided search for stratified inliningGravatar akashlal2010-08-19
* Chalice: added finite differencing refinementGravatar kyessenov2010-08-19
* Chalice:Gravatar kyessenov2010-08-19
* Chalice:Gravatar kyessenov2010-08-19
* Boogie build succeededGravatar codeplexbot2010-08-19
* Simplified grammar for Chalice VS 2010 integration. It should now work and be...Gravatar kyessenov2010-08-19
* Chalice: turn asserts into assumes for method refinements (use -noFreeAssume ...Gravatar kyessenov2010-08-19
* Chalice:Gravatar kyessenov2010-08-18
* Chase type synonyms in arguments/results of map types when generating name (w...Gravatar MichalMoskal2010-08-18
* Some reformatting and refactoringGravatar akashlal2010-08-18
* Don't set monomorphize with typeEncoding:m, not neccessary.Gravatar MichalMoskal2010-08-18
* Added option for displaying stratified inlining's searchGravatar akashlal2010-08-18
* Chalice:Gravatar kyessenov2010-08-18
* Change Synonym type printing to what it was, use a workaround in TypeToString...Gravatar MichalMoskal2010-08-18
* Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m us...Gravatar MichalMoskal2010-08-18
* Make /typeEncoding:m work with arraysGravatar MichalMoskal2010-08-18
* Chalice: added surface syntax for transform, AST matching algorithmGravatar kyessenov2010-08-17
* Boogie build succeededGravatar codeplexbot2010-08-17
* Chalice: refactored AST code for class hierarchy (no need for caches since Sc...Gravatar kyessenov2010-08-17
* Chalice: bug fixes -- "check termination" flag was not properly preserved (i....Gravatar kyessenov2010-08-16
* Boogie: Removed mistaken duplication of a type parameterGravatar tabarbe2010-08-16
* Stratified inlining: Changed recursion into a loop.Gravatar akashlal2010-08-16
* Bug fix for stratified inlining trace generationGravatar akashlal2010-08-16
* Added more options for stratified inliningGravatar akashlal2010-08-16
* Boogie build succeededGravatar codeplexbot2010-08-14
* Boogie: Fixed test 'bitvectors'.Gravatar wuestholz2010-08-14
* Chalice: add pre-conditions to specification statements; semantically spec st...Gravatar kyessenov2010-08-13
* Chalice: add specification statement ( ghost? (const|var) (x (:T)?)+ [P(x)] )Gravatar kyessenov2010-08-13
* Boogie build succeeded, 1 test(s) failedGravatar codeplexbot2010-08-13
* Boogie: Committing changed referencesGravatar tabarbe2010-08-13
* Boogie: Adding 1 more necessary source file for VCExpr, removing an unnecessa...Gravatar tabarbe2010-08-13
* Boogie: Committing new source code for VCExprGravatar tabarbe2010-08-13
* Boogie: Renaming VCExpr sources in preparation for port commitGravatar tabarbe2010-08-13
* Chalice: accept many input files at once; read from stdin if no input file sp...Gravatar kyessenov2010-08-12
* Updated answer to this regression to reflect the fact that it is now verified.Gravatar tabarbe2010-08-12
* Boogie: This reg test was not running verification.Gravatar tabarbe2010-08-12