debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	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
\|
*	Fix a bug in cloning of nested lambda expressions in AI engine	MichalMoskal	2011-02-11
\|
*	Add USE_PREDICATES option to TPTP and SMT provers	MichalMoskal	2011-02-11
\|
*	Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP ↵	MichalMoskal	2011-02-11
\| \| \| \|	provers. Add handling of help message about /proverOpt.
*	Get rid of some warnings.	MichalMoskal	2011-02-11
\|
*	Moved the creation of Boogie procedures from the MetadataTraverser to the ↵	mikebarnett	2011-02-11
\| \| \| \|	Sink because a procedure needs to be created for every method called in the translated program and not just the methods defined in the assembly being translated. This means the contract provider is needed only in the sink and not by any of the traversers.
*	Minor change to stratified inlining	akashlal	2011-02-11
\|
*	If a method definition has any custom attributes, translate them into BPL ↵	mikebarnett	2011-02-09
\| \| \| \|	attributes on the associated procedure.
*	Changed the API for Declaration.AddAttribute so it takes a params argument ↵	mikebarnett	2011-02-09
\| \| \| \|	so multiple parameters can be added to an attribute at one go. No calls had to be changed because of the way params arguments work.
*	Boogie: Yet another refinement of how Z3 is found. Previously, it would ↵	rustanleino	2011-02-09
\| \| \| \|	only look in one of "c:\Program Files\Microsoft Research" and "c:\Program Files (x86)\Microsoft Research", even if both existed (which meant that it might have looked in the wrong one). Now, both are considered.
*	Added support for translating delegates	qadeer	2011-02-08
\|
*	Added a new method StratifiedVC for refinement.	akashlal	2011-02-08
\| \| \| \|	Added a method to copy a FunctionCall.
*	implemented /UseUnsatCoreForInlining option for use in stratified inlining	qadeer	2011-02-06
\|
*	deleted debugging statement	akashlal	2011-02-05
\|
*	Fix to counterexample generation for over-approx query	akashlal	2011-02-05
\|
*	Boogie build succeeded, 4 test(s) failed	codeplexbot	2011-02-05
\|
*	Dafny: Answer file to go with previously updated test file	rustanleino	2011-02-04
\|
*	Boogie build succeeded, 5 test(s) failed	codeplexbot	2011-02-04
\|
*	Dafny: every decreases clause implicitly ends with a never-ending sequence ↵	rustanleino	2011-02-03
\| \| \| \|	of TOP elements; this reduces the need for manually supplied decreases clauses (see the Outer/Inner example in Test/dafny0/Termination.dfy and the Substitute/SubstSeq example in Test/dafny1/Substitution.dfy).
*	Dafny: allow self-calls in function postconditions--these simply refer to ↵	rustanleino	2011-02-03
\| \| \| \|	the result value of the current call
*	Dafny: implemented a more precise scheme for allowing use of a function's ↵	rustanleino	2011-02-03
\| \| \| \|	rep axiom
*	Dafny: replaced the user-defined $ite function with Boogie's built-in ↵	rustanleino	2011-02-03
\| \| \| \|	if-then-else expression
*	Dafny: removed CEV instrumentation	rustanleino	2011-02-03
\|
*	Dafny: removed unused Position argument from CheckWellformed	rustanleino	2011-02-03
\|
*	Dafny: white-space deltas in source code	rustanleino	2011-02-02
\|
*	BVD Dafny: support Skolem constants	rustanleino	2011-02-02
\|
*	Dafny: added ensures clauses to functions	rustanleino	2011-02-02
\|
*	Don't treat "Inconclusive" answer as fatal when splitting.	MichalMoskal	2011-02-02
\|
*	Look for z3.exe in the prover plugin directory first.	MichalMoskal	2011-02-02
\|
*	Improve display of sets; add \now "variable";	MichalMoskal	2011-01-29
\|
*	Fix a bug with previous state display	MichalMoskal	2011-01-28
\|
*	Display stack-allocated structs, as_array types, and *ID in tooltips	MichalMoskal	2011-01-28
\|
*	Display integers in decimal and hexadecimal in tooltip	MichalMoskal	2011-01-27
\|
*	Speedup the number display algorithm, what was I thinking?	MichalMoskal	2011-01-27
\|
*	Display numbers within +-%0.1 of a power of two as 2^N+M	MichalMoskal	2011-01-27
\|
*	Improve colors in source view	MichalMoskal	2011-01-26
\|
*	Simplify state name selection	MichalMoskal	2011-01-26
\|
*	VCC-BVD: display qualifiers of VCC-generated copies of local variables; hide ↵	MichalMoskal	2011-01-26
\| \| \| \| \| \| \|	states that do not update "$s" (heap). Fix some bugs in source view. Rename SourceLocation to SourceViewState.
*	Double-click in state list brings up source view	MichalMoskal	2011-01-26
\|
*	Allow the provider to skip some states when generating SourceLocations	MichalMoskal	2011-01-26
\|
*	Introduce new NamedState base class to reduce code duplication	MichalMoskal	2011-01-26
\|
*	Fix the generation of procedure names so that array types are encoded properly.	mikebarnett	2011-01-26
\| \| \| \| \| \| \|	Translate "default value" expressions. Fix translation of non-trivial conditional expressions and added two more optimizations for trivial ones (trivial ones are where either the true branch or the false branch are constants). Fix translation of array length expressions. Fix translation of logical negation expressions.
*	Display line numbers (useful for finding what the error message refers to)	MichalMoskal	2011-01-26
\|
*	Right-clicking on a state allows to display the source code for it	MichalMoskal	2011-01-26
\|
*	Fix handling of addresses of fields	MichalMoskal	2011-01-24
\|