debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Boogie: removed unreachable or unused code	Rustan Leino	2011-10-27
\|
*	Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵	Rustan Leino	2011-10-27
\| \| \| \|	as if the old /bv:z were used
*	Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵	Rustan Leino	2011-10-27
\| \| \| \|	The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
*	Boogie: Changed default /prover to SMTLIB	Rustan Leino	2011-10-27
\|
*	Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" ↵	Rustan Leino	2011-10-26
\| \| \| \|	statement)
*	Dafny: removed support for assigning to an array-range (that is, an ↵	Rustan Leino	2011-10-26
\| \| \| \|	assignment statement where the LHS has the form a[lo..hi])
*	Merge	Rustan Leino	2011-10-26
\|\
* \|	Dafny: Commented out SnapshotableTrees.Node.FunctionalInsert while ↵	Rustan Leino	2011-10-26
\| \| \| \| \| \| \| \|	performance issues with the prover and going into SMTLib2 mode are being investigated.
* \|	BVD: fixed two basic but damning problems with the Dafny provider, and ↵	Rustan Leino	2011-10-26
\| \| \| \| \| \| \| \|	elided some temporary variables
\| *	Added batch script to run tests for datatypes tests.	Mike Barnett	2011-10-26
\| \|
\| *	VCC: Detect wrong model files	Michal Moskal	2011-10-26
\| \|
* \|	Dafny: implemented compilation of parallel statements	Rustan Leino	2011-10-25
\| \| \| \| \| \| \| \|	Dafny: beefed up resolution of parallel statements
\| *	VCC: improvements in showing arrays, addresses, and embeddings	Michal Moskal	2011-10-24
\| \|
* \|	Dafny: check subrange restriction in parallel Assign statement	Rustan Leino	2011-10-24
\|/ \| \| \| \|	Dafny: verify parallel Call statement Dafny: fixed some bugs: handle all cases of comprehension expressions in resolver's UsesSpecFeatures, check target of method calls to be non-null (duh!)
*	Merge	Rustan Leino	2011-10-24
\|\
* \|	Dafny: continued translation of "parallel" statements (Assign and Proof ↵	Rustan Leino	2011-10-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	forms are mostly there, Call is missing and so is compilation) Dafny: included some test cases for the "parallel" statement Dafny: starting changing old "foreach" statements to the new "parallel" statement
\| *	Don't let /s be specified for stub files. (But keep the old code in case we	Mike Barnett	2011-10-23
\| \| \| \| \| \| \| \|	go back to it.)
* \|	Dafny: added translation of Assign case of the parallel statement	Rustan Leino	2011-10-22
\|/ \| \| \|	Dafny: discovered and fixed bug in no-overlap check of multi-dimensional array update, and changed previously incorrect MatrixFun.dfy test case (the new version is also a more efficient program)
*	Merge	Rustan Leino	2011-10-21
\|\
* \|	Dafny: changed triggers (which are never really used, anyhow) from having a ↵	Rustan Leino	2011-10-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	special syntactic form to being just an attribute Dafny: added "parallel" statement (so far, only parsing and resolving) Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them)
\| *	Tagging EMIC CC.NET build 2.1.31022.0	VccBuildServer	2011-10-22
\| \|
\| *	Sync timeout messages with Z3 prover interface	Michal Moskal	2011-10-21
\| \|
\| *	Don't pass /T: option to Z3 - it kills Z3 prematurely when there are ↵	Michal Moskal	2011-10-21
\| \| \| \| \| \| \| \|	multiple queries
\| *	Improve logging when -proverOpt:VERBOSITY=1 or 2 is specified	Michal Moskal	2011-10-21
\| \|
\| *	Boogie build succeeded	CodeplexBot	2011-10-20
\| \|
\| *	Merge	Michal Moskal	2011-10-19
\| \|\ \| \|/ \|/\|
\| *	VCC: support some more _(blob ...) buisness	Michal Moskal	2011-10-19
\| \|
* \|	Merge	Rustan Leino	2011-10-19
\|\ \
* \| \|	Dafny: fixed performance-buggy translation of exists, and also added some ↵	Rustan Leino	2011-10-19
\| \| \| \| \| \| \| \| \| \| \| \|	other features in SplitExpr (such as induction on existential quantifiers)
\| \| *	BVD: Default to expert view; Only VCC uses that stuff now, and all VCC users ↵	Michal Moskal	2011-10-19
\| \| \| \| \| \| \| \| \| \| \| \|	are clearly experts
\| * \|	Tagging EMIC CC.NET build 2.1.31020.0	VccBuildServer	2011-10-20
\| \|/
\| *	Merge	Michal Moskal	2011-10-19
\| \|\ \| \|/ \|/\|
\| *	Performance improvements in BVD	Michal Moskal	2011-10-19
\| \|
* \|	Merge	Rustan Leino	2011-10-19
\|\\|
* \|	Jennisys: added "ensures" to emacs mode	Rustan Leino	2011-10-19
\| \|
\| *	Tagging EMIC CC.NET build 2.1.31019.0	VccBuildServer	2011-10-19
\| \|
\| *	VCC: Fix problem with booleans being displayed as maps	Michal Moskal	2011-10-19
\| \|
\| *	Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)	Unknown	2011-10-19
\| \|
\| *	Boogie build succeeded	CodeplexBot	2011-10-18
\| \|
\| *	added houdini to regression	qadeer	2011-10-17
\| \| \| \| \| \| \| \|	changed houdini so that the initial worklist is created by queueing downstream Sccs first
\| *	Boogie build succeeded	CodeplexBot	2011-10-17
\| \|
\| *	Merge	qadeer	2011-10-16
\| \|\
\| * \|	revised implementation of proc copy bounding	qadeer	2011-10-16
\| \| \|
\| \| *	Boogie build succeeded	CodeplexBot	2011-10-14
\| \|/ \|/\|
* \|	Jennisys: changed the fixpoint solver to pick only the true clause in a ↵	Unknown	2011-10-10
\| \| \| \| \| \| \| \|	disjunction (if there is one that is true)
* \|	Jennisys: implemented minimization of inferred guards	Unknown	2011-10-10
\| \|
* \|	Jennisys: added some more simple methods in Simple.jen, implemented a couple of	Unknown	2011-10-08
\| \| \| \| \| \| \| \|	optimiations/exensions
* \|	Merge	Aleksandar Milicevic	2011-10-07
\|\ \
\| * \|	Dafny: added COST Verification Competition challenge programs to test suite	Rustan Leino	2011-10-07
\| \|/
* \|	Merge	Aleksandar Milicevic	2011-10-07
\|\\|