debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Added the option /extractLoops to extract loops as procedure calls. If ↵	qadeer	2010-08-11
\| \| \| \|	either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
*	Fixed a contract	akashlal	2010-08-10
\|
*	Boogie: Added boolean code expressions (sans well-formedness checks on the ↵	rustanleino	2010-08-10
\| \| \| \|	input).
*	Boogie: Sorry about that - no need for the conditional compilation	tabarbe	2010-08-09
\|
*	Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.cs	tabarbe	2010-08-09
\|
*	More line ending fixups.	MichalMoskal	2010-08-06
\|
*	Commiting Michal's fix for VC	stobies	2010-08-05
\|
*	Boogie: Removed trailing spaces in code	tabarbe	2010-08-04
\|
*	Made consistent the way all of the C# projects sign themselves and include ↵	mikebarnett	2010-07-30
\| \| \| \|	the version information.
*	Boogie: VCGeneration port part 2/3: Adding new dependent files, removing ↵	tabarbe	2010-07-28
\| \| \| \|	unnecessary one.
*	Boogie: VCGeneration port part 1/3: Replacing old source files with ported ↵	tabarbe	2010-07-28
\| \| \| \|	version
*	Boogie\VCGeneration: Renaming sources in preparation for my addition of the ↵	tabarbe	2010-07-28
\| \| \| \|	ported C# version
*	Boogie: Added interprocedural live variable analysis. Flag to turn it on: ↵	akashlal	2010-07-19
\| \| \| \|	"/liveVariableAnalysis:2"
*	/stratifiedInline:n eagerly inlines n times before calling the stratified ↵	akashlal	2010-07-10
\| \| \| \|	inlining algorithm.
*	Boogie: Bug fix for stratified inlining	akashlal	2010-07-07
\|
*	Boogie: Added stratified inlining. It is enabled using the flag ↵	akashlal	2010-07-07
\| \| \| \|	/stratifiedInline:1.
*	Improved error messages for doomed program points.	schaef	2010-06-15
\|
*	Added another option for lazy inlining based on macro expansion. This ↵	qadeer	2010-05-03
\| \| \| \|	option is activated by /lazyInline:2. The original method is activated by /lazyInline:1.
*	1. Fixed lazy inlining implementation so that inlined procedures use live ↵	qadeer	2010-04-30
\| \| \| \| \| \|	variable analysis as well 2. Separeted model printing from the lazy inlining option
*	1. couple of bug fixes in interprocedural error trace generation	qadeer	2010-04-23
\| \| \| \|	2. added facility for giving weights to the generated quantifiers for lazy inlining; however, left the weights at default 1.
*	Added callee args information to calleeCounterexamples	qadeer	2010-04-21
\|
*	Fixed bug in interprocedural counterexample generation	qadeer	2010-04-19
\|
*	First cut of lazy inlining. The option can be turned on by the flag ↵	qadeer	2010-04-17
\| \| \| \|	/lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.
*	Dafny: Added definedness checks for all statements (previously, some were ↵	rustanleino	2010-03-13
\| \| \| \| \| \|	missing) Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
*	Call program-wide lambda desugaring on axioms only. Call it on procedures in ↵	MichalMoskal	2010-03-12
\| \| \| \|	passive form.
*	Boogie:	rustanleino	2010-02-20
\| \| \| \| \| \| \| \| \| \| \|	* Bug fix: Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case) * Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants. Previously, the only option was to instrument at the beginning and end of every basic block. The new option, which is now the default, is to instrument only at the beginning of loop heads. * Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized * Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1 Boogie refactoring: * Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand * Cleaned up some parsing of command-line options
*	1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a ↵	qadeer	2010-02-16
\| \| \| \| \| \| \|	linear procedure call 2. Inlining requires two fields OriginalBlocks and OriginalLocVars in Implementation. These are set just before inlining is called and now I reset them to null afterwards to help garbage collection. 3. Clear live variables right after passification again to help garbage collection.
*	Implemented block coalescing invoked right after type checking.	qadeer	2010-02-16
\| \| \| \|	Controlled by the option /coalesceBlocks (default is to perform the optimization).
*	Boogie: Peephole optimization to reduce depth of formulas created during VC ↵	rustanleino	2010-02-15
\| \| \| \|	generation. This reduces the chances of Boogie causing a stack overflow.
*	(no commit message)	qadeer	2010-02-12
\|
*	bugfix	schaef	2010-01-28
\|
*	Added experimental feature /DoomDebug. Can be test using ↵	schaef	2010-01-28
\| \| \| \|	Test/doomed/doomdebug.bpl
*	Doomed checking now uses the counterexample trace to minimize the number of ↵	schaef	2009-12-18
\| \| \| \|	theorem prover calls (See useCE in notdoomed.bpl).
*	Added code to (once again) print out prover warnings (under the ↵	rustanleino	2009-11-26
\| \| \| \|	/proverWarning switch).
*	(no commit message)	schaef	2009-11-20
\|
*	Support {:PossiblyUnreachable} attribute on asserts	MichalMoskal	2009-11-20
\|
*	doomed stuff: minor bug fixes / improved output / more test cases	schaef	2009-11-19
\|
*	modified the doom checking. It is now able to report only the relevant ↵	schaef	2009-11-18
\| \| \| \|	statements and writes them the stdout. Line numbers are only displayed for bpl input.
*	Fixes crash when modifies set includes a variable twice.	mkawa	2009-11-07
\|
*	vc:doomed does not use the console anymore to report results	schaef	2009-11-02
\| \| \| \| \| \|	added first test cases for doomed (including the ones from smoke) minor bug fixes minor speed-ups
*	Optimized the number of Z3 queries in doomed program point detection.	schaef	2009-09-25
\|
*	* Boogie and Dafny: added /cev:<file> option	rustanleino	2009-09-15
\| \| \| \| \|	* SscBoogie: changed default setting for /modifiesOnLoop (we really should move this SscBoogie-specific code to the Spec# codeplex)
*	Dafny:	rustanleino	2009-09-14
\| \| \| \| \| \| \| \|	* Added DeclType(f)==C axioms, which for each field f says which class declares it. Boogie: * Changed behavior of free loop invariants. Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures. The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior. * NOTE: I did NOT yet make the corresponding change for loop unrolling, but it is needed.
*	Report prover warnings during smoke test via the VerifierCallback	stobies	2009-09-07
\|
*	Use callback mechanism to report prover warnings; do not just write them to ↵	stobies	2009-09-07
\| \| \| \|	stdout/stderr
*	Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other ↵	stobies	2009-09-07
\| \| \| \|	bitvector operations
*	Sign assemblies	stobies	2009-08-17
\|
*	Fixed bug where the remove-empty-blocks optimization had not updated the ↵	rustanleino	2009-08-13
\| \| \| \|	start block. Now it does. After the remove-empty-blocks optimization, the only possibly empty block is the start block. That is, the optimization does not change the name of the start block.
*	Initial set of files.	mikebarnett	2009-07-15