debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Chalice:	kyessenov	2010-08-22
\| \| \| \|	* coupling invariants work (with certain restrictions as described in TODO comments)
*	Boogie build failed	codeplexbot	2010-08-21
\|
*	Chalice:	kyessenov	2010-08-21
\| \| \| \| \|	* fix a compilation problem (scalac relied on old binaries) * combinator parser and state don't work well together -- added higher-order parser for method transform
*	server-side rename	kyessenov	2010-08-21
\|
*	Boogie: Changed reference of Z3api.csproj to the differently-GUIDded ↵	tabarbe	2010-08-20
\| \| \| \|	Core.csproj, rather than Core.sscproj's old GUID.
*	Boogie: Committing changed references	tabarbe	2010-08-20
\|
*	Boogie: Adding required source file, deleting no-longer-necessarry one	tabarbe	2010-08-20
\|
*	Boogie: Committing changed source files	tabarbe	2010-08-20
\|
*	Boogie: Renaming core sources in preparation for port commit	tabarbe	2010-08-20
\| \| \| \|	*The deletion part of the rename did not occur
*	Boogie: Renaming core sources in preparation for port commit	tabarbe	2010-08-20
\|
*	Added the port of Z3api. It is simply a port to the latest version of ↵	qadeer	2010-08-20
\| \| \| \|	Microsoft.Z3.dll and to C#. It does not work yet.
*	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
\|
*	Added user option for bounding inlining depth	akashlal	2010-08-20
\|
*	Chalice: added syntax, printer and resolver for coupling invariants	kyessenov	2010-08-20
\|
*	Boogie build succeeded	codeplexbot	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
\|
*	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
\|