debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	VS 2010 mode for Chalice: some errors didn't show up in the window because ↵	kyessenov	2010-08-20
\| \| \| \|	positions were negative
*	Boogie: Fixed a few contracts errors	tabarbe	2010-08-19
\|
*	Boogie: Removed and completed a task comment	tabarbe	2010-08-19
\|
*	Boogie: Removed and completed a task comment	tabarbe	2010-08-19
\|
*	Boogie: Removed a completed task comment, added a forgotten ↵	tabarbe	2010-08-19
\| \| \| \|	Contract.EnsuresOnThrow<>()
*	Boogie: Removed a completed task comment	tabarbe	2010-08-19
\|
*	Boogie: Removed a completed task comment	tabarbe	2010-08-19
\|
*	Boogie: Removed an old task comment	tabarbe	2010-08-19
\|
*	Chalice: more regression tests; cosmetic changes to code	kyessenov	2010-08-19
\|
*	Added recursion-bound-guided search for stratified inlining	akashlal	2010-08-19
\|
*	Chalice: added finite differencing refinement	kyessenov	2010-08-19
\|
*	Chalice:	kyessenov	2010-08-19
\| \| \| \| \|	* support multi-step refinement (convert refinement blocks into normal sequences of statements) * added tests
*	Chalice:	kyessenov	2010-08-19
\| \| \| \| \| \|	* added loop transform pattern * implemented translation of refined loops to Boogie (only assert new loop invariants) * refactored loop target computation code (async call was not handled as maybe some other statement)
*	Boogie build succeeded	codeplexbot	2010-08-19
\|
*	Simplified grammar for Chalice VS 2010 integration. It should now work and ↵	kyessenov	2010-08-19
\| \| \| \|	be easily extensible.
*	Chalice: turn asserts into assumes for method refinements (use -noFreeAssume ↵	kyessenov	2010-08-19
\| \| \| \|	to disable)
*	Chalice:	kyessenov	2010-08-18
\| \| \| \| \| \|	* transforms are now callable * resolve transform specs * implement translation for refinement blocks (correct for manipulating locals, not globals)
*	Chase type synonyms in arguments/results of map types when generating name ↵	MichalMoskal	2010-08-18
\| \| \| \|	(with tE:m).
*	Some reformatting and refactoring	akashlal	2010-08-18
\|
*	Don't set monomorphize with typeEncoding:m, not neccessary.	MichalMoskal	2010-08-18
\|
*	Added option for displaying stratified inlining's search	akashlal	2010-08-18
\|
*	Chalice:	kyessenov	2010-08-18
\| \| \| \| \| \| \|	* print type checked program (use -print -noTypecheck if you want old behavior) * refactored program context in Resolver ('errors' is kept as a ListBuffer and shared) * added resolver for refinement blocks (no loops yet) * pretty printer should work now for transforms
*	Change Synonym type printing to what it was, use a workaround in ↵	MichalMoskal	2010-08-18
\| \| \| \|	TypeToString() instead. Add test for /typeEncoding:m.
*	Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m ↵	MichalMoskal	2010-08-18
\| \| \| \|	use separate Z3 type per Boogie type
*	Make /typeEncoding:m work with arrays	MichalMoskal	2010-08-18
\|
*	Chalice: added surface syntax for transform, AST matching algorithm	kyessenov	2010-08-17
\|
*	Boogie build succeeded	codeplexbot	2010-08-17
\|
*	Chalice: refactored AST code for class hierarchy (no need for caches since ↵	kyessenov	2010-08-17
\| \| \| \|	Scala uses structural equality for case classes); landed first piece of refinement code
*	Chalice: bug fixes -- "check termination" flag was not properly preserved ↵	kyessenov	2010-08-16
\| \| \| \|	(i.e. if function app was inside old, the flag was ignored); != was not properly translated for sequences
*	Boogie: Removed mistaken duplication of a type parameter	tabarbe	2010-08-16
\|
*	Stratified inlining: Changed recursion into a loop.	akashlal	2010-08-16
\|
*	Bug fix for stratified inlining trace generation	akashlal	2010-08-16
\|
*	Added more options for stratified inlining	akashlal	2010-08-16
\|
*	Boogie build succeeded	codeplexbot	2010-08-14
\|
*	Boogie: Fixed test 'bitvectors'.	wuestholz	2010-08-14
\|
*	Chalice: add pre-conditions to specification statements; semantically spec ↵	kyessenov	2010-08-13
\| \| \| \|	statement is just like a call statement now
*	Chalice: add specification statement ( ghost? (const\|var) (x (:T)?)+ [P(x)] )	kyessenov	2010-08-13
\|
*	Boogie build succeeded, 1 test(s) failed	codeplexbot	2010-08-13
\|
*	Boogie: Committing changed references	tabarbe	2010-08-13
\|
*	Boogie: Adding 1 more necessary source file for VCExpr, removing an ↵	tabarbe	2010-08-13
\| \| \| \|	unnecessary one
*	Boogie: Committing new source code for VCExpr	tabarbe	2010-08-13
\|
*	Boogie: Renaming VCExpr sources in preparation for port commit	tabarbe	2010-08-13
\|
*	Chalice: accept many input files at once; read from stdin if no input file ↵	kyessenov	2010-08-12
\| \| \| \|	specified
*	Updated answer to this regression to reflect the fact that it is now verified.	tabarbe	2010-08-12
\|
*	Boogie: This reg test was not running verification.	tabarbe	2010-08-12
\|