summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* 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
* Boogie: Sorry about that - no need for the conditional compilationGravatar tabarbe2010-08-09
* Boogie: That file should not have been in the depot, but rather be created lo...Gravatar tabarbe2010-08-09
* Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.csGravatar tabarbe2010-08-09
* Boogie build succeeded, 1 test(s) failedGravatar codeplexbot2010-08-08
* Boogie: Fixed a few line endingsGravatar tabarbe2010-08-06
* Dafny: Fixed VS 2010 mode to really include all Dafny keywordsGravatar rustanleino2010-08-06
* Chalice: refinement of a list with nodes (instead of lists pointing to sublists)Gravatar kyessenov2010-08-06
* Chalice: terminate Boogie subprocess manually on interrupt; Z3 still stays al...Gravatar kyessenov2010-08-06
* Remove -z3DebugTraces and -z3Mam options (no longer working). Rename the -z3b...Gravatar MichalMoskal2010-08-06
* More line ending fixups.Gravatar MichalMoskal2010-08-06
* Fixup line-endings.Gravatar MichalMoskal2010-08-06
* Boogie: added /z3bv option that overrides the current setting of Z3 options f...Gravatar stobies2010-08-06
* Reverting accidental check-inGravatar stobies2010-08-06
* Remove support for Z3 V1 and clean up parameter processing code for Z3Gravatar stobies2010-08-06
* Chalice: still cannot verify refinement of List.get (Z3 goes out of memory); ...Gravatar kyessenov2010-08-06
* Combine version file creation into a single task so we run it for both filesGravatar stobies2010-08-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-25 05:51:56 +0000