debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge pull request #35 from Checkmate50/master	RustanLeino	2016-08-17
\|\ \| \| \| \|	Floating Point Support
* \|	Fix deadlock in the new thread scheduler	BarryBo	2016-08-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix deadlock where a Boogie task schedules a task and waits on it. The .NET threadpool creates more threads than cores, up to a limit, which hides the issue. The new policy did not account for recursion and caused the newly-created tasks to wait forever for the earlier ones to complete.
\| *	fixed an error where a -0 was not interpreted as a negative number	Checkmate50	2016-07-23
\| \|
* \|	Run Boogie code on threads with large stacks	BarryBo	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Replace TaskScheduler.Default by a custom TaskScheduler. The .Default uses threadpool threads whose stack size is controlled by the host EXE header. The new ThreadTaskScheduler give Boogie control over the stack size, and defaults to 16mb.
\| *	Removed automatic exponent shifting	Checkmate50	2016-07-22
\| \|
\| *	fixed an issue with parsing floating points	Checkmate50	2016-07-19
\| \|
\| *	fixed floatceiling function	Checkmate50	2016-07-19
\| \|
\| *	Added and briefly tested the updated syntax. NaN/oo not supported yet	Checkmate50	2016-07-19
\| \|
\| *	Changed the syntax reading of the float type	Checkmate50	2016-07-16
\| \|
\| *	rebuilt scanner and parser via coco	Checkmate50	2016-07-16
\| \|
\| *	change to update	Checkmate50	2016-06-07
\| \|
\| *	removed an unnecessary type checking addition	Checkmate50	2016-06-07
\| \|
\| *	fixed some merging issues	Checkmate50	2016-06-07
\| \|
\| *	resolving conflicts	Checkmate50	2016-06-06
\| \|\ \| \|/ \|/\|
\| *	Merging complete. Everything looks good crosses fingers	Checkmate50	2016-06-06
\| \|
\| *	finished testing, fixed several minor compiler bugs	Checkmate50	2016-06-06
\| \|
\| *	Initial round of testing works with new syntax. Fixed an error where ↵	Checkmate50	2016-05-31
\| \| \| \| \| \| \| \|	floating points could not be given as a function argument
* \|	Rename DLLs to non-generic names by prefixing "Boogie". Project names and	akashlal	2016-04-15
\| \| \| \| \| \| \| \|	namespaces remain the same.
\| *	modified floating point syntax and modified floating point constants to use ↵	Checkmate50	2016-03-17
\| \| \| \| \| \| \| \|	bitvector values
* \|	Improve support for identifying unnecessary assumes.	Valentin Wüstholz	2016-03-09
\| \|
* \|	Add support for weights on soft assumes.	Valentin Wüstholz	2016-03-07
\| \|
* \|	Improve support for optimization and identifying unnecessary assumes.	Valentin Wüstholz	2016-03-03
\| \|
\| *	Modified BigFloat and parser to accept correct SMT-LIB syntax	Checkmate50	2016-02-20
\| \|
* \|	Bug fix in determining whether a type parameter is bounded	qunyanm	2016-01-19
\| \| \| \| \| \| \| \| \| \| \| \|	When checking whether a type parameter could be determined from the bound variable types, we mistakenly compare equality between a TypeVarable and a VCExprVar, instead of between two VCExprVars.
\| *	Added several test cases and some basic documentation for fp usage	Checkmate50	2016-01-04
\| \|
* \|	Minor change	Valentin Wüstholz	2015-12-29
\| \|
* \|	Fix issue with ids for assume-statements.	Valentin Wüstholz	2015-12-28
\| \|
* \|	Improve precision of abstract interpreter for modulo operations.	Valentin Wüstholz	2015-12-28
\| \|
* \|	Enable optimization for more prover queries.	Valentin Wüstholz	2015-12-27
\| \|
* \|	Remove unused file.	Valentin Wüstholz	2015-12-03
\| \|
* \|	Remove workaround for older versions of Z3.	Valentin Wüstholz	2015-12-02
\| \|
* \|	Use the EndCurly token when creating the ReturnCmd for unifiedExit	qunyanm	2015-12-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block.
\| *	Special fp types (such as infinity and NaN are now translated by boogie	Checkmate50	2015-11-29
\| \|
* \|	Add simplified may-unverified analysis and instrumentation.	Valentin Wüstholz	2015-11-20
\| \|
* \|	Fix issue with partially-verified assertions.	Valentin Wüstholz	2015-11-19
\| \|
* \|	Minor changes	Valentin Wüstholz	2015-11-19
\| \|
* \|	Add experimental support for optimization (requires Z3 build after changeset ↵	Valentin Wüstholz	2015-11-18
\| \| \| \| \| \| \| \|	9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
* \|	Fix issue #25.	Valentin Wüstholz	2015-11-17
\| \|
* \|	Add support for identifying unnecessary assumes.	Valentin Wüstholz	2015-11-16
\| \|
* \|	Document the new behaviour of the ``-proc:`` command line option	Dan Liew	2015-10-31
\| \| \| \| \| \| \| \|	in the output of Boogie's help.
* \|	Added wild card matching for /proc flag	Shaobo	2015-10-31
\| \|
* \|	Add support for annotating implementations with k-ind. depth.	Valentin Wüstholz	2015-10-29
\| \|
* \|	fix for deterministicExtractLoops for nested loops	Shuvendu Lahiri	2015-10-27
\| \|
* \|	Bug fix for deterministExtractLoops for Shaobo's example	Shuvendu Lahiri	2015-10-26
\| \|
* \|	bug fix in the type checking of calls to atomic procedures	Shaz Qadeer	2015-10-16
\| \|
\| *	Floating point constants given as integers are now translated correctly	Checkmate50	2015-10-14
\| \|
\| *	Modified translation so that z3 runs with type checking for simple binary ↵	Checkmate50	2015-10-14
\| \| \| \| \| \| \| \|	operations
* \|	bug fix	Shaz Qadeer	2015-10-09
\| \|
* \|	removed an extraneous warning	Shaz Qadeer	2015-10-08
\| \|
* \|	Merge branch 'master' of https://github.com/boogie-org/boogie	Shaz Qadeer	2015-10-01
\|\ \