debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Dafny: implemented thresholds for the new interval domain (/infer:j)	Rustan Leino	2011-12-12
\|
*	Dafny: corrected merge snafus	Rustan Leino	2011-12-07
\|
*	Dafny: fixed division in new interval domain	Rustan Leino	2011-12-07
\|
*	Boogie: Added new abstract interpretation harness, which uses native Boogie ↵	Rustan Leino	2011-12-05
\| \| \| \| \| \| \| \|	Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred}
*	Boogie: removed unreachable or unused code	Rustan Leino	2011-10-27
\|
*	ported Houdini to C#, added Houdini project to the Boogie solution	qadeer	2011-08-03
\|
*	Re-enabled quantifier checking in the Checked configuration.	mikebarnett	2011-03-16
\|
*	Turn off quantifier checking in the runtime checking.	mikebarnett	2011-03-14
\|
*	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.
*	Added version.cs as link to those projects that were missing it	stobies	2010-12-06
\| \| \| \|	Select 4.0 client profile on all projects
*	Factored out the ParserHelper class into a separate project and updated the ↵	wuestholz	2010-12-02
\| \| \| \| \| \|	files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
*	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.
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	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.
*	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: Removed an old task comment	tabarbe	2010-08-19
\|
*	Boogie: Added boolean code expressions (sans well-formedness checks on the ↵	rustanleino	2010-08-10
\| \| \| \|	input).
*	Boogie: Sorry about that - no need for the conditional compilation	tabarbe	2010-08-09
\|
*	Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.cs	tabarbe	2010-08-09
\|
*	More line ending fixups.	MichalMoskal	2010-08-06
\|
*	Boogie: Removed trailing spaces in code	tabarbe	2010-08-04
\|
*	Boogie: Code Contracts runtime checking was turned on in AbsInt. I turned ↵	tabarbe	2010-08-04
\| \| \| \|	it back off.
*	Made consistent the way all of the C# projects sign themselves and include ↵	mikebarnett	2010-07-30
\| \| \| \|	the version information.
*	Boogie: Changed references from binary to project references.	tabarbe	2010-07-27
\|
*	Boogie: Fixing incorrect referencing of Microsoft.Contracts (the Code ↵	tabarbe	2010-07-21
\| \| \| \|	Contracts dll) in AbsInt, Isabelle, and Z3
*	Boogie: Changed how the references in AbsInt are referenced, and fixed a ↵	tabarbe	2010-07-19
\| \| \| \|	typo in the Spec# version of Z3's ProverInterface.ssc
*	Boogie: I have successfully ported the AbsInt project. It passes all ↵	tabarbe	2010-07-16
\| \| \| \| \| \|	regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL. Address any error complaints to t-abarbe@microsoft.com
*	Boogie: Renamed the AbsInt sources for use in the port I have done. ↵	tabarbe	2010-07-16
\| \| \| \|	Regressions with the changed code will take ~10 minutes. I hope I don't break anyone's build.
*	* Added "deprecated" comment in help message about /interprocInfer switch. ↵	rustanleino	2010-02-18
\| \| \| \| \| \| \|	The functionality is currently broken. * Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
*	Also sign AbsInt.dll	stobies	2009-08-18
\|
*	Sign assemblies	stobies	2009-08-17
\|
*	Initial set of files.	mikebarnett	2009-07-15