debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵	mikebarnett	2011-03-10
\| \| \| \| \| \|	dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
*	Added a new solution configuration, Checked, that builds the Checked ↵	mikebarnett	2011-03-07
\| \| \| \|	configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
*	Fix some more contracts.	mikebarnett	2011-03-07
\|
*	Fix contracts so runtime checking can be turned on.	mikebarnett	2011-03-07
\|
*	Kill {:prover "..."} attribute support; no one ever used this stuff	MichalMoskal	2011-02-17
\|
*	Boogie: Yet another refinement of how Z3 is found. Previously, it would ↵	rustanleino	2011-02-09
\| \| \| \|	only look in one of "c:\Program Files\Microsoft Research" and "c:\Program Files (x86)\Microsoft Research", even if both existed (which meant that it might have looked in the wrong one). Now, both are considered.
*	Look for z3.exe in the prover plugin directory first.	MichalMoskal	2011-02-02
\|
*	Boogie: Made the algorithm for finding Z3 more robust.	wuestholz	2011-01-21
\|
*	Use a made-up name when Context.Lookup() cannot find a name	MichalMoskal	2010-12-10
\|
*	Don't crash in Context.Lookup when the namer has never seen the name. This ↵	MichalMoskal	2010-12-10
\| \| \| \|	happens when the name is never used in the VC (e.g. it gets peep-hole optimized).
*	Added version.cs as link to those projects that were missing it	stobies	2010-12-06
\| \| \| \|	Select 4.0 client profile on all projects
*	Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln	qadeer	2010-12-01
\|
*	Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵	qadeer	2010-11-27
\| \| \| \|	Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
*	Boogie: Look for Z3 versions up to 2.20.	wuestholz	2010-11-23
\|
*	Boogie: Changed the trace output formatting of the prover version slightly.	wuestholz	2010-11-11
\|
*	Boogie:	rustanleino	2010-10-12
\| \| \| \| \| \|	* enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	Boogie:	rustanleino	2010-09-23
\| \| \| \| \| \|	* Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument
*	created a new build target called z3apidebug.	qadeer	2010-08-29
\| \| \| \| \|	only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver.
*	Added a constructor to a contract class otherwise the compiler complained ↵	mikebarnett	2010-08-28
\| \| \| \|	about the default nullary one calling its base class nullary ctor, and there wasn't one.
*	Boogie: Simplify: Added a contracts class that I forgot in the initial porting.	tabarbe	2010-08-27
\|
*	Boogie: Commented out all occurences of repeated inherited contracts - makes ↵	tabarbe	2010-08-27
\| \| \| \|	fewer error messages when compiling with runtime checking on.
*	Boogie: Removed some errors with code contracts (commenting out ↵	tabarbe	2010-08-27
\| \| \| \|	doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
*	Boogie: Changed the cce classes into one separate project, which every other ↵	tabarbe	2010-08-27
\| \| \| \|	project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
*	Boogie: Basetypes port 3/3: Committing changed references	tabarbe	2010-08-27
\| \| \| \|	Z3api.csproj shouldn't get in the way this time 'round.
*	Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵	tabarbe	2010-08-27
\| \| \| \|	files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
*	Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵	tabarbe	2010-08-26
\| \| \| \|	Core to jive with recent changes made to the cce class.
*	Boogie: Committing changed references	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Removed a completed task comment	tabarbe	2010-08-19
\|
*	Boogie: Committing changed references	tabarbe	2010-08-13
\|
*	Fixup line-endings.	MichalMoskal	2010-08-06
\|
*	Boogie: added /z3bv option that overrides the current setting of Z3 options ↵	stobies	2010-08-06
\| \| \| \|	for better performance on VCs that are heavy on bitvector arithmetic
*	Boogie: Removed trailing spaces in code	tabarbe	2010-08-04
\|
*	Boogie: The deletion of those files did not hold, lemme try again.	tabarbe	2010-07-30
\|
*	Boogie: Removed cce.cs's from the provers, because they all reference ↵	tabarbe	2010-07-30
\| \| \| \|	projects which have a (more up-to-date) copy of cce.cs.
*	Made consistent the way all of the C# projects sign themselves and include ↵	mikebarnett	2010-07-30
\| \| \| \|	the version information.
*	Boogie: VCGeneration port part 3/3: Updating sources to reference new ↵	tabarbe	2010-07-28
\| \| \| \|	project; making Core work with the port by removing the nonnull requirements on one abstract method.
*	Fixed reference to VCGeneration project. Mistakenly checked in project files ↵	mikebarnett	2010-07-28
\| \| \| \|	were pointing to the yet-to-exist C# version.
*	Boogie Provers: Changed the references from binary to project references.	tabarbe	2010-07-27
\|
*	Boogie: AssemblyInfo.cs is no longer required for the build; cce.cs is.	tabarbe	2010-07-23
\|
*	Boogie: Committing my port of simplify, along with the slightly changed ↵	tabarbe	2010-07-23
\| \| \| \|	references of simplify's dependents.
*	Boogie: Renaming Simplify.sscproj and source files in preparation for ↵	tabarbe	2010-07-23
\| \| \| \|	committing my port of Simplify.csproj.
*	Boogie: Repaired a reentrancy error in Z3/Simplify.	tabarbe	2010-07-22
\|
*	Boogie: Added stratified inlining. It is enabled using the flag ↵	akashlal	2010-07-07
\| \| \| \|	/stratifiedInline:1.
*	Boogie:	rustanleino	2010-06-08
\| \| \| \| \| \| \| \| \|	* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it). * Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it). Dafny: * Split off some tests from Test/dafny0 into Test/dafny1. * Added Test/dafny1/UltraFilter.dfy.
*	Updated to find the latest version of Z3 (2.7) and made the algorithm ↵	wuestholz	2010-05-28
\| \| \| \|	slightly more robust.
*	Updated to find the latest version of Z3 (2.6).	wuestholz	2010-05-02
\|
*	First cut of lazy inlining. The option can be turned on by the flag ↵	qadeer	2010-04-17
\| \| \| \|	/lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.