debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Changed Has method of PureSequence to Contains to make refactoring easier.	Ally Donaldson	2013-07-22
\|
*	Fixed bugs arising from differences between hashtables and dictionaries	Ally Donaldson	2013-07-22
\|
*	Large refactoring of Hashtable to Dictionary.	Ally Donaldson	2013-07-22
\|
*	Merge	allydonaldson	2013-07-22
\|\
\| *	Fixed what looks like a type-related bug in the manipulation of ↵	allydonaldson	2013-07-22
\| \| \| \| \| \| \| \|	newGotoCmdOrigins: this Hashtable is commented as having type TransferCmd -> ReturnCmd, but it was being used here as if the key type was Block.
* \|	Refactored variable2sequenceNumber to use Dictionary	Ally Donaldson	2013-07-22
\|/
*	Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a ↵	Ally Donaldson	2013-07-22
\| \| \| \|	plain Hashtable.
*	Added an attribute to set the time limit for implementations.	wuestholz	2013-07-12
\|
*	Worked on the parallelization.	wuestholz	2013-07-12
\|
*	Worked on the parallelization.	wuestholz	2013-07-11
\|
*	Worked on the parallelization.	wuestholz	2013-07-11
\|
*	Worked on the parallelization.	wuestholz	2013-07-11
\|
*	Worked on the parallelization.	wuestholz	2013-07-10
\|
*	Worked on the parallelization.	wuestholz	2013-07-01
\|
*	Did some refactoring in the execution engine and worked on the parallelization.	wuestholz	2013-07-01
\|
*	Did some refactoring in the execution engine and worked on the parallelization.	wuestholz	2013-06-25
\|
*	Did some refactoring in the execution engine and worked on the parallelization.	wuestholz	2013-06-21
\|
*	Fixed bug in the cutting of back edges (that manifested itself whenever the ↵	Rustan Leino	2013-05-29
\| \| \| \|	first block in a procedure was the target of a back edge)
*	Working on fixedpoint backend	Ken McMillan	2013-05-20
\|
*	Adding fixedpoint engine backend	Ken McMillan	2013-05-07
\|
*	Use the new ProverInterface's Evaluate method in stratified inlinig	Unknown	2013-01-03
\| \| \| \|	(guarded by the flag /useProverEvaluate)
*	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.
*	Fixed issue with uniformity analysis and block merging. Uniformity analysis	Unknown	2012-09-24
\| \| \| \|	now enabled by default.
*	Added functionality for race error reporting.	Egor Kyshtymov	2012-08-20
\|
*	VCGen: add MergeBlocksIntoPredecessors function	Peter Collingbourne	2012-07-09
\|
*	a bug fix	qadeer	2012-06-19
\|
*	another edit for predication	qadeer	2012-06-19
\|
*	integrating predication	qadeer	2012-06-19
\|
*	Removed program argument from VerifyImplementation. It is redundant since ↵	qadeer	2012-05-29
\| \| \| \| \| \|	the constructor of ConditionGeneration takes a program reference and stashes it in a field.
*	more refactoring	qadeer	2012-05-28
\|
*	starting the implementation of the new stratified inlining API	qadeer	2012-05-21
\|
*	some other cleanups	qadeer	2012-05-10
\|
*	eliminated class ErrorModel	qadeer	2012-04-28
\|
*	removed lazy inlining	qadeer	2012-04-28
\|
*	various changes for using unsat cores in Houdini	qadeer	2012-04-17
\|
*	further fixes	qadeer	2012-02-28
\|
*	various cleanup regarding /doNotUseLabels	qadeer	2012-02-28
\|
*	fixing stratified inlining to deal with new path info	qadeer	2012-02-27
\|
*	various fixes related to new error traces	qadeer	2012-02-27
\|
*	further fixes related to using uninterpreted function for error traces	qadeer	2012-02-25
\| \| \| \|	removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
*	using model instead of labels	Unknown	2012-02-23
\|
*	Use DateTime.UtcNow instead of DateTime.Now	stobies	2012-01-11
\| \| \| \|	see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx
*	Boogie: fixed proof-obligation counting	Rustan Leino	2012-01-09
\|
*	Boogie: output number of proof obligations (asserts) along with timing ↵	Rustan Leino	2012-01-09
\| \| \| \|	information when using the /trace option
*	Boogie: Fixed a crash due to old expressions in lambda expressions that were ↵	wuestholz	2011-12-02
\| \| \| \| \| \|	not replaced after lambda expansion. (reported by Florian Egli)
*	Remove invariant that was just wrong	Michal Moskal	2011-11-28
\|
*	refactoring houdini so that it creates only a single instance of z3	qadeer	2011-11-16
\|
*	Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵	Rustan Leino	2011-11-15
\| \| \| \|	CommandLineOptions to separate the options that belong to these 3 tools.
*	partial check in regarding getting states working with stratified inlining	qadeer	2011-09-06
\|