debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵	Rustan Leino	2013-03-05
\| \| \| \|	Codeplex repositories.
*	Chalice: Switch to latest Scala release (there seems to be a compiler bug ↵	stefanheule	2012-09-12
\| \| \| \|	with 2.8.1 that prevents the current code from compiling).
*	Chalice: Remove accidental changes to chalice.bat.	stefanheule	2012-09-05
\|
*	Chalice: reapplied changes from changeset	Unknown	2012-09-03
\| \| \| \|	2648 (ff8bdaa099cd) Chalice: Allow unfolding expressions in predicates (this fixes workitem 10223).
*	Intermediate version of implementation with two masks per predicate. #m_calc ↵	Unknown	2012-08-09
\| \| \| \| \| \|	mask starts out as ZeroPMask and is added to during translation. #m mask starts out havoced, and is assumed to be equal to #m_calc as late as possible. This idea doesn't seem to work out, since the assumes generated come too late in the code for some of the asserts (which depend on framing information) to work. However, given the changes I made to funciton framing recently, I'm wondering if the havoced masks are even necessary any more. Next: try removing them and just using #m_calc for everything..
*	Chalice: Added /boogieOpt:noinfer to chalice.bat in order to run Boogie ↵	mschwerhoff	2012-03-26
\| \| \| \|	without the specification inference component, because the latter is currently causing trouble with one of the AVL-tree examples.
*	Chalice: Fix chalice.bat to work with paths that contain spaces.	stefanheule	2012-02-27
\|
*	Chalice: Fix chalice.bat.	Unknown	2012-02-27
\|
*	Adapted batch file to use larger JVM stack size.	peter mueller peter.mueller@inf.ethz.ch	2011-09-19
\|
*	Chalice: Modified chalice.bat s.t. it checks if all Java classpath elements ↵	mschwerhoff	2011-09-19
\| \| \| \|	exist
*	Chalice: Modified chalice.bat s.t. it uses the Scala libraries downloaded ↵	mschwerhoff	2011-09-16
\| \| \| \|	but Sbt. This releaves the user from having to ensure that he/she has the same Scala version in the path as used by Sbt to build Chalice.
*	Chalice: Improve command line interface. Unknown options are no longer ↵	stefanheule	2011-08-03
\| \| \| \|	silently passed to Boogie (but passing them to Boogie is still possible with /boogieOpt), and Chalice shows a message when it expects input from stdin.
*	Chalice: Chalice is now built using sbt (simple built tool).	stefanheule	2011-08-02
\|
*	Chalice: Fix batch file problem and update reference output.	stefanheule	2011-07-19
\|
*	Chalice: New permission model that provides more abstraction and more ↵	stefanheule	2011-07-01
	flexibility. Details of the model can be found in the paper 'Fractional Permissions without the Fractions', FTfJP 2011 (see http://www.pm.inf.ethz.ch/publications/). This changeset also fixes several bugs not directly related to the permissions model and improves the error handling. The following features have been added or enhanced: - Error handling: If exceptions (e.g. about not supported features) are encountered, a user-friendly message is displayed - Sequence axioms: There is an additional axiom for singleton lists, which is helpful in some cases - Prelude: Chalice's prelude has been split into sections (e.g. one for permission-related stuff, one for sequence axioms, and so on), which are included on demand (less superfluous axioms, etc.) Currently not working - but planned to be updated as well - are the following features: - Stepwise refinements - autoFold - read locks There is a performance issue with permission scaling (i.e., taking non-full versions of predicates that contain read-permissions). Details can be found in the following file: Chalice/tests/permission-model/scaling.chalice. A list of fixed bugs (see http://boogie.codeplex.com/workitem/<workitem number> for details on the individual bugs) - workitem 10200: Issue with the axiom of framing functions - workitem 10197: The translation of old(waitlevel) resultet in Boogie error - workitem 10196: Quantification over empty sequences - workitem 10195: Contradiction when descending sequences are used - workitem 10192: Invalid translation of old-construct in certain cases - workitem 10190: Stack overflow when parsing large comment blocks - workitem 10147: Duplicated method parameters and return values are not detected