debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Made it collect more statistics about the more advanced verification result ↵	wuestholz	2014-07-01
\| \| \| \|	caching.
*	Made it collect some statistics about the more advanced verification result ↵	wuestholz	2014-06-30
\| \| \| \|	caching.
*	a fix in Inline method; it should look for inline attribute only on ↵	qadeer	2014-06-28
\| \| \| \|	procedures and implementations
*	Added a program cache (used by the more advanced verification result caching).	wuestholz	2014-06-28
\|
*	Minor refactoring	wuestholz	2014-06-28
\|
*	Changed the verification result cache to use the built-in 'MemoryCache' class.	wuestholz	2014-06-28
\|
*	OnModel now carries the result of the prover call	akashlal	2014-06-28
\|
*	Fix in SI while dealing with timeouts	akashlal	2014-06-27
\|
*	Optimized the way that assertions are marked as partially verified.	wuestholz	2014-06-26
\|
*	Fixed issue in verification result caching.	wuestholz	2014-06-26
\|
*	Optimized the way that dependency checkums are computed.	wuestholz	2014-06-26
\|
*	Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"	Dan Rosén	2014-06-24
\| \| \| \| \| \|	When running boogie form the command line, this should be on by default. On the other hand, the TokenTextWriter constructors and PrintBplFile now have an argument for this, but by default it is off.
*	Worked on an extension of the existing verification result caching.	wuestholz	2014-06-23
\|
*	Changed the 'verifySnapshots' command-line option to accept a numeric ↵	wuestholz	2014-06-20
\| \| \| \|	argument instead of a boolean one.
*	Fixed crash in resolver	Rustan Leino	2014-06-19
\|
*	Fix bug in BigDec.FromString() which would not parse negative	Dan Liew	2014-06-18
\| \| \| \| \| \| \| \|	numbers correctly. For example BigDec.FromString("-1.5") would be interpreted as -0.5 due to the incorrect way the method handles the fractional part of the string.
*	Added mechanism for getting the variables referenced by a loop (not just the ↵	Ally Donaldson	2014-06-09
\| \| \| \|	modified vars)
*	Fixed a bug in revised mod set analysis	Ally Donaldson	2014-06-06
\|
*	Refactored modset analysis to avoid the use of static fields. Static fields ↵	Ally Donaldson	2014-06-06
\| \| \| \|	cause data races when we run parts of Boogie that both do mod set analysis at the same time.
*	Merge	Ally Donaldson	2014-06-06
\|\
* \|	Small refactoring	Ally Donaldson	2014-06-06
\| \|
* \|	Made VarsAssignedInLoop public, since it can be useful in computing modifies ↵	Ally Donaldson	2014-06-06
\| \| \| \| \| \| \| \|	sets elsewhere.
\| *	Merge	qadeer	2014-06-02
\| \|\
\| * \|	various fixes	qadeer	2014-06-02
\| \| \|
\| \| *	Add isBvConst and asBvConst accessors to LiteralExpr to match the	Dan Liew	2014-05-28
\| \| \| \| \| \| \| \| \| \| \| \|	others already present for bool, BigNum and BigDec.
\| \| *	Fixed minor issue.	wuestholz	2014-05-28
\| \|/ \|/\|
* \|	Refactored ConcurrentHoudini and Houdini to (significantly) reduce ↵	Ally Donaldson	2014-05-28
\| \| \| \| \| \| \| \|	duplication of code
* \|	Removed printing code from candidate dependence analyser	Ally Donadlson	2014-05-28
\| \|
* \|	Small cleanup in Staged Houdini	Ally Donaldson	2014-05-28
\| \|
* \|	Fixed state capture concurrency bug with Staged Houdini	Ally Donaldson	2014-05-27
\| \|
* \|	Merge	Ally Donaldson	2014-05-27
\|\ \
* \| \|	Undid accidental commit	Ally Donaldson	2014-05-27
\| \| \|
\| * \|	Implemented an additional type check for assumption variables.	wuestholz	2014-05-27
\| \| \|
* \| \|	Merge	Ally Donaldson	2014-05-27
\| \| \|
* \| \|	Added key check to uniformity analysis	Ally Donaldson	2014-05-27
\|/ /
* \|	Merge duality changes	Ken McMillan	2014-05-26
\|\ \
\| * \|	Conjecture printing for duality and child user time tracking.	Ken McMillan	2014-05-26
\| \| \|
\| \| *	Merge	qadeer	2014-05-21
\| \| \|\ \| \|_\|/ \|/\| \|
\| \| *	a small fix	qadeer	2014-05-21
\| \| \|
* \| \|	Made the Boogie driver return an exit code.	wuestholz	2014-05-19
\| \| \|
* \| \|	keep some stats for debugging	akashlal	2014-05-15
\| \|/ \|/\|
* \|	Simplify Z3 executable discovery.	wuestholz	2014-05-12
\| \|
* \|	Added stack bounding	akashlal	2014-05-10
\| \|
\| *	Merge extra recuresion bound changes for FixedPointVC	Ken McMillan	2014-04-21
\| \|\
* \| \|	Teach the ExecutionEngine to respect the -useBaseNameForFileName commandline	Dan Liew	2014-04-09
\| \| \| \| \| \| \| \| \| \| \| \|	option when reporting the number of errors.
* \| \|	Added /useBaseNameForFile command line argument. The Scanner	Dan Liew	2014-04-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	and Parser constructors have been modified to take an optional argument specifying this and the ExecutionEngine passes for that value CommandLineOptions.Clo.UseBaseNameForFileName This option when true causes the basename of file to be used inside created Tokens instead of what the user passed on the command line which might be a relative or absolute path. The motivation for adding this option is that it is needed for the lit driven tests so that the output of Boogie can be reliably checked.
* \| \|	a bug fix	qadeer	2014-05-07
\| \| \|
* \| \|	added {:aux} attribute to local variables	qadeer	2014-05-07
\| \| \|
* \| \|	third checkpoint (refactored more code)	qadeer	2014-05-05
\| \| \|
* \| \|	second checkpoint	qadeer	2014-05-04
\| \| \|