debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge	Rustan Leino	2011-11-22
\|\
\| *	Merge	Rustan Leino	2011-11-22
\| \|\
\| * \|	DafnyExtension: fix up compilation (once again)	Rustan Leino	2011-11-22
\| \| \|
\| * \|	Dafny: call C# compiler directly from inside Dafny, and optionally produce a ↵	Rustan Leino	2011-11-22
\| \| \| \| \| \| \| \| \| \| \| \|	.cs file with the new /spillTargetCode switch
\| \| *	Merge	qadeer	2011-11-22
\| \| \|\ \| \| \|/ \| \|/\|
\| * \|	Boogie: don't resolve ignored types (that is, "extern" types that have been ↵	Rustan Leino	2011-11-22
\| \| \| \| \| \| \| \| \| \| \| \|	thrown out)
\| \| *	Merge	qadeer	2011-11-22
\| \| \|\ \| \| \|/ \| \|/\|
\| \| *	added support for handling duplicate axioms	qadeer	2011-11-22
\| \| \|
\| * \|	fixes to summary computation	Unknown	2011-11-22
\| \| \|
* \| \|	Dafny: Added "type" declaration (syntax: "type X;"), which introduces an ↵	Rustan Leino	2011-11-21
\| \| \| \| \| \| \| \| \| \| \| \|	arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
\| * \|	Refactored translator so it can be called programmatically and return the	Mike Barnett	2011-11-21
\| \|/ \| \| \| \| \| \|	translated program in memory without writing it to disk.
\| *	Automated merge with https://hg01.codeplex.com/boogie	Mike Barnett	2011-11-21
\| \|\
\| \| *	BCT: Initialize Boogie's command-line options object correctly before using	Mike Barnett	2011-11-21
\| \| \| \| \| \| \| \| \| \| \| \|	Boogie.
\| * \|	Merge	Unknown	2011-11-21
\| \|\ \
\| * \| \|	Generating useful, and guarateed by construction, postconditions and loop ↵	Unknown	2011-11-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	invariants for kenrel procedures.
\| \| * \|	Boogie build succeeded	CodeplexBot	2011-11-21
\| \| \| \|
\| \| * \|	Added lazy summary computation to stratified inlining (not finished yet)	akashlal	2011-11-20
\| \| \|/
\| \| *	commented calls to GC.Collect()	qadeer	2011-11-18
\| \| \|
\| \| *	changed the semantics of requires and ensures for inlined procedures	qadeer	2011-11-17
\| \| \|
\| \| *	Boogie build succeeded	CodeplexBot	2011-11-17
\| \|/ \|/\|
* \|	Merge	Rustan Leino	2011-11-16
\|\ \
* \| \|	Dafny: fixed bad Code Contracts	Rustan Leino	2011-11-16
\| \| \|
\| * \|	Boogie build failed	CodeplexBot	2011-11-17
\|/ /
* \|	Merge	qadeer	2011-11-16
\|\ \
* \| \|	/contractInfer always prints the computed assignment now	qadeer	2011-11-16
\| \| \| \| \| \| \| \| \| \| \| \|	enabled the houdini regressions
* \| \|	refactoring houdini so that it creates only a single instance of z3	qadeer	2011-11-16
\| \| \|
\| * \|	Translate AddressOf expressions correctly.	Mike Barnett	2011-11-16
\| \| \| \| \| \| \| \| \| \| \| \|	Fixes for problems when translating generic type parameters.
\| * \|	Boogie: fixed build error (incorrect type in Contract.Result)	Rustan Leino	2011-11-16
\| \| \|
* \| \|	Eliminated unused argument in the constructor for Checker	qadeer	2011-11-16
\| \| \|
\| * \|	Tagging EMIC CC.NET build 2.1.31116.0	VccBuildServer	2011-11-16
\| \| \|
\| * \|	Merge	Michal Moskal	2011-11-16
\| \|\\|
* \| \|	Merge	qadeer	2011-11-16
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	simple fix in houdini	qadeer	2011-11-16
\| \| \|
\| * \|	Merge	Unknown	2011-11-16
\| \|\ \
\| * \| \|	Small fix.	Unknown	2011-11-16
\| \| \| \|
\| \| * \|	Load all assemblies before doing anything else so that the unification for	Mike Barnett	2011-11-16
\| \|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the Core Assembly identity can happen correctly. Cache things in the sink based on the mangled name rather than the interned key: this prevents clashes in the Boogie program, but might mask some errors due to different types/members with the same full name (minus the assembly name of course). Translate generic parameters as Ref instead of Box if they are constrained to be a reference or struct (since we translate structs as Ref). [Experimental]
\| * \|	Merge	Unknown	2011-11-16
\| \|\ \
\| * \| \|	Better support for race-checking contracts	Unknown	2011-11-16
\| \| \| \|
\| \| * \|	Boogie build failed	CodeplexBot	2011-11-16
\| \| \| \|
\| \| * \|	Merge	akashlal	2011-11-16
\| \| \|\ \
\| \| \| * \|	Debugging output for stratified inlining. Emit attribute on Ensures while	Unknown	2011-11-16
\| \|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \|	printing it.
\| \| \| *	BVD: Fix display bug	Michal Moskal	2011-11-15
\| \| \| \|
\| \| \| *	VCC: Further data type improvements	Michal Moskal	2011-11-15
\| \| \| \|
\| \| \| *	VCC: Better display of data type values	Michal Moskal	2011-11-15
\| \| \| \|
\| \| * \|	DafnyExtension: fixed build problems	Rustan Leino	2011-11-15
\| \| \| \|
\| \| * \|	Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵	Rustan Leino	2011-11-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	CommandLineOptions to separate the options that belong to these 3 tools.
\| \| \| *	VCC: Recognize $result	Michal Moskal	2011-11-15
\| \|_\|/ \|/\| \|
\| \| *	Merge	Rustan Leino	2011-11-15
\| \| \|\ \| \|_\|/ \|/\| \|
\| \| *	Added Dafny solutions to the VSTTE 2012 program verification competition	Rustan Leino	2011-11-15
\| \| \|
* \| \|	Merge	qadeer	2011-11-15
\|\\| \|