debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Fixed a postcondition.	wuestholz	2014-12-26
\|
*	strengthened type checking	qadeer	2014-12-26
\| \| \| \| \|	cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions
*	changed type checking of yield procedures so that they can only call other ↵	qadeer	2014-12-18
\| \| \| \|	yielding procedures
*	more work on reducing call stack consumption	qadeer	2014-12-18
\|
*	some refactoring to separate the concept of shared variables under ↵	qadeer	2014-12-17
\| \| \| \|	refinement checking with all global variables
*	Merge	qadeer	2014-12-16
\|\
* \|	patched two occurrences of StackOverflowException on benchmarks from IronClad	qadeer	2014-12-16
\| \|
\| *	Added an annotation, :split_here, for predicate statements.	Bryan Parno	2014-12-16
\|/ \| \| \| \| \|	The annotation allows the programmer to manually indicate where the verification of a procedure implementation should be split into pieces.
*	Fixed a precondition.	wuestholz	2014-12-16
\|
*	patched last check in	qadeer	2014-12-15
\|
*	1. made variable introduction layer explicit in the test cases	qadeer	2014-12-15
\| \| \| \|	2. if a single layer is specified for a global variable, that layer is the introduction layer
*	systematic renaming of phase to layer	qadeer	2014-12-15
\|
*	Reverted a change to CreateTempVariable for FixedPointVC only.	Ken McMillan	2014-12-08
\|
*	Merge some FixpointVC changes that got left behind	Ken McMillan	2014-12-08
\|\
* \|	Optimized the VC generation for assumption variables.	wuestholz	2014-12-07
\| \|
* \|	fixed bug due to incomplete erasure of :linear attribute	qadeer	2014-12-05
\| \|
* \|	Patch by Jeroen Ketema	Dan Liew	2014-12-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix some of the interfacing with Z3 4.3.2 in SMTLib. In particular: * It makes the useSmtOutputFormat usable * It fixes parsing of bit vectors that occur in the models returned by Z3 Similar stuff might be broken in the other interfaces to Z3, but it shouldn’t be more broken than it already was.
* \|	Added todos.	wuestholz	2014-11-26
\| \|
* \|	Fixed issue with resolution of function calls.	wuestholz	2014-11-26
\| \|
* \|	Fix FunctionCall.Resolve() so that when the function is resolved the type ↵	Dan Liew	2014-11-25
\| \| \| \| \| \| \| \| \| \| \| \|	becomes availble via ShallowType(). This fixes the ExprTypeChecking.FunctionCallTypeResolved() unit test.
* \|	Add unit test to catch another bug in Boogie where FunctionCall ShallowType	Dan Liew	2014-11-25
\| \| \| \| \| \| \| \| \| \| \| \|	is not correctly set. This is related to the bug fixed in cea703affa29. That commit fixed the ShallowType when it was set using the constructor that takes a Function but the parser uses the other constructor which has the same bug.
* \|	Fix bug in FunctionCall that caused the ExprTypeChecking.FunctionCall()	Dan Liew	2014-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	unit test to fail. The issue was that one of FunctionCall constructors created a new IdentifierExpr without associating a type with it. To fix this we now set the type of the IdentifierExpr to the return type of the Function passed into the constructor.
* \|	Added a unit test to catch a bug in Boogie where a NAryExpr.ShallowType	Dan Liew	2014-11-25
\| \| \| \| \| \| \| \|	fails when the Function is a FunctionCall
* \|	Worked on the verification result caching (extracted functions).	wuestholz	2014-11-25
\| \|
* \|	Fixed issues in the verification result caching (old expressions).	wuestholz	2014-11-24
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-23
\| \|
* \|	Change the ToolsVersion attribute of the Project tag in the recently	Dan Liew	2014-11-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	added unit tests csproj files from 12.0 to 4.0. This done so that Monodevelop 5.0.1 can import these projects (it can't handle the newer ToolsVersion). This didn't seem to break anything in Visual Studio 2013
* \|	Patch by Jeroen Ketema	Dan Liew	2014-11-17
\| \| \| \| \| \| \| \|	Fix interfacing with CVC4 1.5
* \|	Make run-unittests.py executable under Linux/OSX. This	Dan Liew	2014-11-17
\| \| \| \| \| \| \| \| \| \|	required changing the line endings so that it uses unix line endings.
* \|	Introduce unit tests which use NUnit. NUnit is now a dependency	Dan Liew	2014-11-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	so developers need to install it via NuGet. There aren't many tests yet. Just a few for Core and Basetypes but hopefully more will be added in the future. More information can be found in Source/UnitTests/README.md
* \|	Fixed issue in the verification result caching.	wuestholz	2014-11-10
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-10
\| \|
* \|	Made it never include the statement checksum when printing assert statements.	wuestholz	2014-11-16
\| \|
* \|	renamed :phase to :layer	qadeer	2014-11-14
\| \|
* \|	a fix to type checking	qadeer	2014-11-09
\| \|
* \|	changed the suffix of the trace file from .bpl to .txt to avoid confusing ↵	qadeer	2014-11-08
\| \| \| \| \| \| \| \|	the lit tool
* \|	re-enabling -useUnsatCoreForContractInfer	shuvendu	2014-11-07
\| \| \| \| \| \| \| \|	An example houdini\testUnsatCore.bpl to test out the unsatCore (Currently seems to be not working)
* \|	Minor refactoring	wuestholz	2014-11-05
\| \|
* \|	Minor change to make some regression tests work with Z3 4.3.2	wuestholz	2014-11-05
\| \|
* \|	Let attributes live on during inlining	akashlal	2014-11-05
\| \|
* \|	Logging for SMTLib prover	akashlal	2014-11-05
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-05
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-03
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-03
\| \|
* \|	Fixed minor issue.	wuestholz	2014-11-02
\| \|
* \|	Made it produce more trace output for the verification result caching.	wuestholz	2014-11-02
\| \|
* \|	Did some refactoring.	wuestholz	2014-11-02
\| \|
* \|	Fixed an issue (reported by Akash Lal).	wuestholz	2014-10-30
\| \|
* \|	SI: print if a bound was reached.	akashlal	2014-10-29
\| \|
* \|	Fixed minor issue (reported by Alex Summers).	wuestholz	2014-10-28
\| \|