debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Refactoring of VariableSeq and TypeSeq	Ally Donaldson	2013-07-22
\|
*	Requires/EnsuresSeq replaced by List<Requires/Ensures>	Ally Donaldson	2013-07-22
\|
*	Refactored RequiresSeq and EnsuresSeq so that they wrap List<Requires> and ↵	Ally Donaldson	2013-07-22
\| \| \| \|	List<Ensures>, respectively, as a first step towards simply using the List versions.
*	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
\|
*	Revamp of staged Houdini, and completion of parallel support.	allydonaldson	2013-07-18
\|
*	Merge	allydonaldson	2013-07-16
\|\
* \|	Reworking of Staged Houdini in preparation for parallelising it.	allydonaldson	2013-07-16
\| \|
\| *	end atomic actions at async and parallel calls	qadeer	2013-07-15
\| \|
\| *	1. changed values passed to additional parameters to procedures; async and ↵	qadeer	2013-07-14
\| \| \| \| \| \| \| \| \| \| \| \|	parallel calls treated exactly the same now 2. fixed bug in collection of available linear vars for parallel calls; added more test cases to regression
\| *	Added an attribute to set the time limit for implementations.	wuestholz	2013-07-12
\|/
*	Worked on the parallelization (task cancellation).	wuestholz	2013-07-09
\|
*	Added an option to verify each input file separately.	wuestholz	2013-07-05
\|
*	Added support in the abstract interpreter for an attribute {:identity}, ↵	Rustan Leino	2013-07-05
\| \| \| \|	which says that a function is an identity function.
*	Addressed some \n versus \r\n issues	Rustan Leino	2013-06-29
\|
*	Merge	allydonaldson	2013-06-18
\|\
\| *	Did some refactoring in the execution engine.	wuestholz	2013-06-14
\| \|
\| *	Added /help and /attrHelp output for program snapshot verification.	wuestholz	2013-06-12
\| \|
\| *	Worked on improving program snapshot verification.	wuestholz	2013-06-10
\| \|
* \|	Merge	allydonaldson	2013-06-07
\|\ \
* \| \|	Some work on staged Houdini	allydonaldson	2013-06-07
\| \| \|
\| \| *	Worked on improving program snapshot verification.	wuestholz	2013-06-05
\| \|/
\| *	Did some refactoring in the Boogie driver.	wuestholz	2013-06-03
\| \|
\| *	Did some refactoring in the Boogie driver.	wuestholz	2013-06-03
\| \|
\| *	Added a feature for verifying several program snapshots (incl. result ↵	wuestholz	2013-06-02
\| \| \| \| \| \| \| \|	caching and prioritization).
\| *	Merge changes to support Corral in fixedpoint backend	Ken McMillan	2013-05-29
\|/\|
\| *	Getting fixed point backend to work with Corral.	Ken McMillan	2013-05-29
\| \|
* \|	Improvements to Staged Houdini	allydonaldson	2013-05-29
\| \|
* \|	Staged Houdini can now take a path to a file of ignored variables	allydonaldson	2013-05-27
\|/
*	deleted some commented code	Unknown	2013-05-20
\|
*	further bug fixes in og; global copies of global variables are now thread local	Unknown	2013-05-19
\|
*	reworked the linear and og implementation based on available variables theory	Unknown	2013-05-18
\|
*	merging changes for fixedpoint engine backend	Ken McMillan	2013-05-07
\|\
* \|	Adding fixedpoint engine backend	Ken McMillan	2013-05-07
\| \|
\| *	havocs and updates to globals added only if they are non-null	Unknown	2013-05-06
\| \|
\| *	fixed bug (reported by Akash) in treatment of linear parameters to calls	Unknown	2013-05-06
\| \|
\| *	In the typecheck method of HavocCmd, added calls to typecheck the havoced vars	Unknown	2013-05-04
\| \|
\| *	Merge	Unknown	2013-05-04
\| \|\
\| * \|	fixed bug reported by Akash	Unknown	2013-05-04
\|/ /
\| *	Print "\n" after a YieldCmd	akashlal	2013-05-03
\|/
*	Merge	allydonaldson	2013-04-30
\|\
* \|	Staged Houdini	allydonaldson	2013-04-30
\| \|
\| *	Added a little bit of virtual-ness to the Inliner class. This is so that I can	akashlal	2013-04-28
\| \| \| \| \| \| \| \|	subclass it to implement my own inlining policy.
\| *	added free ensures to each procedure to compensate for havocing of allocator	Unknown	2013-04-19
\| \|
\| *	Made OG-Desugared parsable as a Boogie program.	akashlal	2013-04-19
\| \|
\| *	Fix mod-set traversal to do visit code inside code expressions.	Rustan Leino	2013-04-18
\| \|
\| *	refactored og and fixed latest bug reported by chris	Unknown	2013-03-20
\| \|
\| *	the allocator corresponding to every linear variable	Unknown	2013-03-13
\| \| \| \| \| \| \| \| \| \|	in the modset of a procedure is now put into the modset itself (in addition to the allocators for the output parameters)
\| *	Added explicit mod set analysis calls to OG transform and linear transform	Unknown	2013-03-13
\| \|
\| *	added mod set checking to the linear type checker	Unknown	2013-03-13
\| \|