debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Normalise line endings using a .gitattributes file. Unfortunately	Dan Liew	2015-06-28
\| \| \| \| \| \|	this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
*	Missing braces	akashlal	2015-06-20
\|
*	Updated to Staged Houdini	Ally Donaldson	2015-01-08
\|
*	changed the suffix of the trace file from .bpl to .txt to avoid confusing ↵	qadeer	2014-11-08
\| \| \| \|	the lit tool
*	Did more refactoring.	wuestholz	2014-09-23
\|
*	Did some refactoring.	wuestholz	2014-09-23
\|
*	a bug fix in Houdini (also AbsHoudini)	qadeer	2014-09-19
\|
*	InlineAssume attribute for ensures clauses; if present, the ensures ↵	qadeer	2014-09-18
\| \| \| \|	condition is assumed while inlining.
*	fixed a bug in inlining	qadeer	2014-09-17
\| \| \| \|	changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"
*	fixed a crash	qadeer	2014-09-16
\|
*	Fix nasty bug introduced by commit 61a94f409975.	Dan Liew	2014-07-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
*	Refactored ConcurrentHoudini and Houdini to (significantly) reduce ↵	Ally Donaldson	2014-05-28
\| \| \| \|	duplication of code
*	(Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵	Rustan Leino	2014-02-24
\| \| \| \| \| \|	of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
*	Fixed errors in the use of Code Contracts	Rustan Leino	2014-02-10
\|
*	Option for reversing Houdini worklist (for top-down analysis)	akashlal	2014-01-28
\|
*	small cleanup	Pantazis Deligiannis	2013-10-10
\|
*	fixed bug with the exchange refuted invariants process	Pantazis Deligiannis	2013-10-06
\|
*	changes to support a configured errorLimit	Pantazis Deligiannis	2013-09-30
\|
*	more changes towards parallelisation of Houdini	Pantazis Deligiannis	2013-09-29
\|
*	refactoring + new class ConcurrentHoudini	Pantazis Deligiannis	2013-09-27
\|
*	refuted candidates are exchanged in memory using a concurrent dictionary ↵	Pantazis Deligiannis	2013-09-26
\| \| \| \|	instead of using an IO csv file as before
*	improvements to the refuted annotations exchange process	Pantazis Deligiannis	2013-08-20
\|
*	new option for reversing the topological order - this could potentially help ↵	Pantazis Deligiannis	2013-08-19
\| \| \| \|	to speedup houdini refutation of candidates
*	changes in the parallel houdini script	Pantazis Deligiannis	2013-07-30
\|
*	added script for running the portfolio solver (parallel houdini)	Pantazis Deligiannis	2013-07-30
\|
*	parallel houdini prototype working	Pantazis Deligiannis	2013-07-26
\|
*	CmdSeq: farewell	Ally Donaldson	2013-07-22
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	More refactoring towards replacing PureCollections.Sequence with List	Ally Donaldson	2013-07-22
\|
*	Requires/EnsuresSeq replaced by List<Requires/Ensures>	Ally Donaldson	2013-07-22
\|
*	Large refactoring of Hashtable to Dictionary.	Ally Donaldson	2013-07-22
\|
*	Revamp of staged Houdini, and completion of parallel support.	allydonaldson	2013-07-18
\|
*	Extracted Houdini statistics into a record, and parametersied Houdini class ↵	allydonaldson	2013-07-16
\| \| \| \|	with a statistics object. This means that if one runs multiple Houdini instances, each can record its own statistics.
*	Did some refactoring in the execution engine and worked on the parallelization.	wuestholz	2013-07-01
\|
*	Method in Houdini to allow an expression to be turned into non-candidate form	allydonaldson	2013-06-21
\|
*	Adapted Houdini algorithm to take staging into account	allydonaldson	2013-05-18
\|
*	Staged Houdini	allydonaldson	2013-04-30
\|
*	Refactored MatchCandidate	allydonaldson	2013-03-08
\|
*	MatchCandidate modified to match candidates by variable name, rather than by ↵	allydonaldson	2013-03-08
\| \| \| \|	variable identity. ApplyAssignment method added, which takes a program (not necessarily the same program on which Houdini was invoked, but a program that has the same candidate set), and applies the Houdini assignment to the program.
*	Some code clean-up	Unknown	2013-01-07
\|
*	minor bug fix	Unknown	2012-12-27
\|
*	Bug fix for ExplainHoudini. Made it robust under timeouts.	Unknown	2012-12-20
\|
*	AbstractHoudini: bug fixes	akashlal	2012-12-16
\|
*	Added some comments	akashlal	2012-12-12
\|
*	Merge	akashlal	2012-12-12
\|\
* \|	First implementation of ExplainHoudini	Unknown	2012-12-12
\| \|
\| *	Houdini: allow cross-dependencies between procedures that occurs when assume	Unknown	2012-12-11
\|/ \| \| \|	and assert commands in implementations have existential constants
*	when a query times out, all asserted candidates are dropped	Unknown	2012-11-25
\|
*	bunch of refactorings	Unknown	2012-10-03
\| \| \| \| \| \| \| \| \|	- moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
*	Removed AIFramework from Boogie -- use native trivial or native ↵	boehmes	2012-09-27
\| \| \| \| \| \| \|	interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.