debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Minor changes	wuestholz	2014-10-13
\|
*	Minor change	wuestholz	2014-10-13
\|
*	Add '/traceCaching' flag.	wuestholz	2014-10-13
\|
*	Implement ToString() override for TransferCmds. It is overriden for	Dan Liew	2014-10-13
\| \| \| \| \|	Cmd classes but for some reason it wasn't implemented for TransferCmds which seems a little inconsistent.
*	Fix bug in the Duplicator.	Dan Liew	2014-10-08
\| \| \| \| \|	Previously after duplication of an entire program CallCmd.Proc would point to procedures in the old program.
*	Fix typos in the name of a property and method used for handling	Dan Liew	2014-10-08
\| \| \| \| \| \|	Absy metadata. This feature is very new so it is unlikely any out of tree code (apart from my own) is using it so this change shouldn't be disruptive.
*	Fix bug in Duplicator. Previously when cloning an entire Program	Dan Liew	2014-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	a cloned Implementation.Proc would not be the same Procedure in the TopLevelDeclarations. The reason for this is that Procedure would be cloned twice, once when visiting it from the TopLevelDeclarations and once when visiting each Implementation of that Procedure's Implementation.Proc. To fix this a Procedure is only duplicated once by caching it based on reference value (this assumes the original Program has Procedure and Implementation.Proc correctly resolved). This also assumes that Procedure.Equals() and Procedure.GetHashCode() have not been overidden.
*	Improved on my fix to the Duplicator bug fixed in ca82591ab1f8.	Dan Liew	2014-10-06
\| \| \| \| \|	Instead of the Duplicator maintaining state the VisitImplementation() method computes the mapping between old and new Blocks.
*	Fix bug in Duplicator where GotoCmd's LabelTargets and LabelNames	Dan Liew	2014-10-05
\| \| \| \| \| \| \| \| \| \| \|	where not updated during duplication to point to duplicated BasicBlocks. Because the lists weren't being duplicated and resolved to the new basic blocks a duplicated Implementation pointed into Blocks in the old implementation via GotoCmds. This is bad and is not the expected behaviour. Now if VisitImplementation() is called during duplication GotoCmds will be resolved to point to duplicated Blocks.
*	Some fixes to ITP	akashlal	2014-10-04
\|
*	minor fixes to interpolating TP	akashlal	2014-10-03
\|
*	Merge	akashlal	2014-10-01
\|\
\| *	Minor corrections	akashlal	2014-10-01
\| \|
* \|	fixed StackOverflow in TraceCounterexample;	qadeer	2014-09-30
\|/ \| \| \|	converted tail recursion into a loop
*	Added a flag to initialize the interpolating TP	akashlal	2014-09-29
\|
*	SI: VC gen with labels	akashlal	2014-09-29
\|
*	Cleanup: removed unused code	akashlal	2014-09-29
\|
*	Fix to VC gen	akashlal	2014-09-28
\|
*	Merge	akashlal	2014-09-27
\|\
* \|	Fix for boolVC generation	akashlal	2014-09-27
\| \|
* \|	Better fix for the duplicator, thanks to wuestholz	akashlal	2014-09-27
\| \|
\| *	Fixed issue reported by Akash Lal.	wuestholz	2014-09-26
\|/
*	Fix for the duplicator; can't use Clone	akashlal	2014-09-26
\|
*	The setter is better this way	akashlal	2014-09-25
\|
*	Lets have a setter for TopLevelDeclarations as well	akashlal	2014-09-25
\|
*	Merge.	Dan Liew	2014-09-24
\|\
* \|	Remove dead method argument	Dan Liew	2014-09-24
\| \| \| \| \| \| \| \|	Patch by Jeroen Ketema
* \|	Remove dead code	Dan Liew	2014-09-24
\| \| \| \| \| \| \| \|	Patch by Jeroen Ketema
* \|	Let the SMT lib convert models to Z3-like models	Dan Liew	2014-09-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The Model parser for SMT models is broken beyond repair and this by-passes this. The code could be moved to the model parser, but that's a refactoring for another day. Also, the existing version already had multiple reparses going on and this at least removes one of those. Patch by Jeroen Ketema.
\| *	(Subhajit) Added an interface for InterpolatingTheoremProver	akashlal	2014-09-24
\| \|
\| *	minor fix	akashlal	2014-09-24
\| \|
\| *	Simple VC generation for SI	akashlal	2014-09-24
\|/
*	Fixed assertion violation.	wuestholz	2014-09-23
\|
*	Did more refactoring and addressed several todos.	wuestholz	2014-09-23
\|
*	Did more refactoring.	wuestholz	2014-09-23
\|
*	Did some refactoring.	wuestholz	2014-09-23
\|
*	Added a test for the issue that was fixed in changeset 'e972f163bb7c'.	wuestholz	2014-09-23
\|
*	Fixed an issue in the verification result caching (recycled errors).	wuestholz	2014-09-22
\|
*	Add missing run lines (based off Test/doomed/runtest.bat) to doomed	Dan Liew	2014-09-21
\| \| \| \| \| \| \| \|	tests. These are really broken because Boogie just seems to hang when they are executed. So they aren't executed right now. I'm not sure what to do with the other .bpl files. ``schaef`` left them lying around.
*	minor fix to abshoudini's handling of quantifiers	akashlal	2014-09-20
\|
*	a small fix to prefix calculation	qadeer	2014-09-19
\|
*	more tests for houdini /inlineDepth	shuvendu	2014-09-19
\|
*	a bug fix in Houdini (also AbsHoudini)	qadeer	2014-09-19
\|
*	Patch by Jeroen Ketema.	Dan Liew	2014-09-19
\| \| \| \| \| \|	Only set produce-unsat-cores in the case /explainHoudini is passed. This allows contract inference to be used with solvers that do no support unsat cores, as long as no explanation of the Houdini run is required.
*	Fixed minor issue.	wuestholz	2014-09-19
\|
*	additional tests for houdini /inlineDepth	shuvendu	2014-09-18
\|
*	InlineAssume attribute for ensures clauses; if present, the ensures ↵	qadeer	2014-09-18
\| \| \| \|	condition is assumed while inlining.
*	fixed various CodeContracts issues.	qadeer	2014-09-18
\|
*	added a comment	qadeer	2014-09-17
\|
*	fixed a bug in inlining	qadeer	2014-09-17
\| \| \| \|	changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"