debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3	MichalMoskal	2011-02-18
\|
*	Accomodate for recent changes in Z3 V2 model format	MichalMoskal	2011-02-18
\|
*	Ask Z3 to generate models, in V2 format, when needed	MichalMoskal	2011-02-18
\| \| \| \| \|	Add supported :prover commands Minor fixes
*	Don't stop when some test fails	MichalMoskal	2011-02-18
\|
*	Handle /useArrayTheory	MichalMoskal	2011-02-18
\|
*	Add tickleBool	MichalMoskal	2011-02-18
\|
*	Allow for running Boogie and Dafny testcases separately	MichalMoskal	2011-02-18
\|
*	Remove a testcase for bvInt (feature to be killed soon)	MichalMoskal	2011-02-18
\|
*	Allow for passing flags to test runs	MichalMoskal	2011-02-18
\|
*	Intercept Z3 warnings and pass them on	MichalMoskal	2011-02-18
\|
*	Boogie build succeeded, 4 test(s) failed	codeplexbot	2011-02-18
\|
*	Remove workaround for Z3 scanner problems (fixed now); fix one comment	MichalMoskal	2011-02-18
\|
*	Recognize () as identifier terminators	MichalMoskal	2011-02-18
\|
*	Handle bitvectors	MichalMoskal	2011-02-18
\|
*	Expose ToByteArray()	MichalMoskal	2011-02-18
\|
*	Dafny:	rustanleino	2011-02-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case). * Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.) * Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type. * More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal") * Add axioms about idempotence of set union and intersection * The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one * In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase * Fixed error in translation of while(*)
*	Boogie: Fixed problem with binding power of .[.] versus type coercions in ↵	rustanleino	2011-02-17
\| \| \| \|	pretty printing
*	Use explicit mechanism for skipping to the next assertion	MichalMoskal	2011-02-17
\|
*	Disable MBQI and AUTO_CONFIG	MichalMoskal	2011-02-17
\|
*	Kill the solver process when ctrl-c is pressed	MichalMoskal	2011-02-17
\|
*	Provide /p: as the short form of /proverOpt:.	MichalMoskal	2011-02-17
\| \| \| \| \|	Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT. Add default Z3 options when using Z3.
*	Read prover responses; handle labels	MichalMoskal	2011-02-17
\|
*	Make it possible to run Z3 on pipe; use generic PROVER_LOG options	MichalMoskal	2011-02-17
\|
*	Add IEnumerable.Iter	MichalMoskal	2011-02-17
\|
*	Kill {:prover "..."} attribute support; no one ever used this stuff	MichalMoskal	2011-02-17
\|
*	Don't use Simplify's LogProverInterface	MichalMoskal	2011-02-17
\|
*	Indentation.	MichalMoskal	2011-02-17
\|
*	Start implementation of pipe communication in SMTLIB backend	MichalMoskal	2011-02-17
\|
*	Stratified inlining: Added concrete values to error traces. Added an extra ↵	akashlal	2011-02-17
\| \| \| \|	flag "inferLeastForUnsat".
*	Dafny: added test harness to Test/dafny1/ExtensibleArray.dfy	rustanleino	2011-02-16
\|
*	Dafny: added ExtensibleArray program as a test	rustanleino	2011-02-16
\|
*	Fix some deprecation warnings from scalac 2.8.0.	kyessenov	2011-02-16
\| \| \| \| \|	Check for Boogie.exe only on Windows. Fix parser (_ is a keyword, not a delimiter)
*	Fix printing of type-proxies	MichalMoskal	2011-02-16
\|
*	Bugfixes in select-of-store axioms	MichalMoskal	2011-02-16
\|
*	Skip "(assert true)" in output; skip "Linearing..." messages when they are fast	MichalMoskal	2011-02-16
\|
*	Fix let scoping	MichalMoskal	2011-02-15
\|
*	Workaround bug in Z3 SMT parser	MichalMoskal	2011-02-15
\|
*	Background predicate for SMT2	MichalMoskal	2011-02-15
\|
*	Use SMT2 top-level syntax	MichalMoskal	2011-02-15
\|
*	Use the new UniformArguments property; formatting	MichalMoskal	2011-02-15
\|
*	Add VCExprNAry.UniformArguments property to return arguments of nested ↵	MichalMoskal	2011-02-15
\| \| \| \|	And/Or nodes.
*	Add some extension methods to IEnumberable<T>	MichalMoskal	2011-02-15
\|
*	Print terms in SMT2 syntax (drop term/formula distinction)	MichalMoskal	2011-02-15
\|
*	Move name-quoting (already for SMT2 not SMT1) into a seprate class	MichalMoskal	2011-02-15
\|
*	Dafny: added alternate version of PriorityQueue	rustanleino	2011-02-15
\|
*	Boogie build succeeded, 4 test(s) failed	codeplexbot	2011-02-15
\|
*	Boogie build succeeded, 26 test(s) failed	codeplexbot	2011-02-15
\|
*	Fix with timeout	akashlal	2011-02-12
\|
*	Better support for timeout	akashlal	2011-02-12
\|
*	Boogie build succeeded, 4 test(s) failed	codeplexbot	2011-02-12
\|