summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* 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
* Added methods to read a file from any Stream objectGravatar akashlal2010-08-12
* Boogie build succeeded, 1 test(s) failedGravatar codeplexbot2010-08-12
* Chalice: example proving a simple identity (for refinement demonstration), re...Gravatar kyessenov2010-08-12
* Chalice: put classes and objects into package "chalice"Gravatar kyessenov2010-08-11
* Added the option /extractLoops to extract loops as procedure calls. If eithe...Gravatar qadeer2010-08-11
* Chalice: fix "assume false" in the example (intended a spec statement)Gravatar kyessenov2010-08-11
* Chalice: finite differences with recursion instead of loopsGravatar kyessenov2010-08-10
* Chalice: added uninterpreted functions; attempting to re-verify Celebrity in ...Gravatar kyessenov2010-08-10
* Fix the test to use new name for /z3bv option.Gravatar MichalMoskal2010-08-10
* Fixed a contractGravatar akashlal2010-08-10
* Boogie build succeeded, 1 test(s) failedGravatar codeplexbot2010-08-10
* Boogie: Added boolean code expressions (sans well-formedness checks on the in...Gravatar rustanleino2010-08-10
* Chalice: forcefully kill Boogie with taskkill /T /F on terminationGravatar kyessenov2010-08-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-03 23:57:26 +0000