debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Dafny: let verifier, not the resolver, check for missing cases in match ↵	Rustan Leino	2011-05-19
\| \| \| \|	expressions/statements
*	Merge	Rustan Leino	2011-05-18
\|\
* \|	Dafny: added set comprehension expressions	Rustan Leino	2011-05-18
\| \|
\| *	Fixed array construction	qadeer	2011-05-17
\| \| \| \| \| \| \| \|	Added a couple more stubs
\| *	added another axiom	Unknown	2011-05-17
\| \|
\| *	Merge	Mike Barnett	2011-05-17
\| \|\
\| * \|	If a method has been translated as a function, generate a function call and	Mike Barnett	2011-05-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	not a procedure call for calls to the method. Use the Location (full path) instead of just the file name for source locations.
\| \| *	Merge	qadeer	2011-05-17
\| \| \|\
\| \| * \|	added spec for GetType	qadeer	2011-05-17
\| \|/ /
\| \| *	Boogie build succeeded	CodeplexBot	2011-05-17
\| \|/ \|/\|
* \|	Merge	Rustan Leino	2011-05-16
\|\\|
* \|	Dafny: Test case for sequence of boxed booleans	Rustan Leino	2011-05-16
\| \|
* \|	Dafny: To help verifications involving sequences of (boxed) booleans along, ↵	Rustan Leino	2011-05-16
\| \| \| \| \| \| \| \|	added function $IsCanonicalBoolBox
\| *	Fix command-line option processing.	Mike Barnett	2011-05-16
\| \|
\| *	bug fixes	qadeer	2011-05-16
\| \|
\| *	Fix break.	Mike Barnett	2011-05-16
\| \|
\| *	new regression output	Mike Barnett	2011-05-16
\| \|\
\| * \	Merge	Mike Barnett	2011-05-16
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	merge	Mike Barnett	2011-05-16
\| \| \|
\| * \|	Merge	Mike Barnett	2011-05-16
\| \| \|
\| \| *	Add extern declarations to procedures.	Mike Barnett	2011-05-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Normalize method bodies so anonymous delegates are gone. Some attempts at simplifying. New regression output.
\| \| *	Mark procedures/functions as "extern" if they are defined in a different	Mike Barnett	2011-05-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	assembly than the one under translation. Normalize method bodies so anonymous delegates do not appear, but instead show up as the nested classes/methods that implement them. Beginning of some simplfication for nested expressions.
* \| \|	Merge	qadeer	2011-05-16
\|\ \ \
* \| \| \|	convert assert to requires	qadeer	2011-05-16
\| \|/ / \|/\| \|
\| * \|	Dafny: added some test cases that use nat	Rustan Leino	2011-05-16
\| \| \|
\| * \|	Dafny: added optional range expressions to logical quantifiers, preparing ↵	Rustan Leino	2011-05-15
\|/ / \| \| \| \| \| \|	for addition other other comprehensions (like set comprehension)
* \|	Merge	Rustan Leino	2011-05-14
\|\ \
* \| \|	Dafny: fixed bug in quantifier bounds discovery	Rustan Leino	2011-05-14
\| \| \|
\| * \|	Boogie build failed	CodeplexBot	2011-05-14
\|/ /
* \|	Dafny: fixed typo in parser code	Rustan Leino	2011-05-13
\| \|
* \|	Merge	Rustan Leino	2011-05-13
\|\ \
* \| \|	Boogie: added features to help with modular verification. In particular, ↵	Rustan Leino	2011-05-13
\| \| \| \| \| \| \| \| \| \| \| \|	define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations.
* \| \|	Cleaner version of ghost loop termination example.	Unknown	2011-05-13
\| \| \|
* \| \|	Add source file (Expression Design) for the BVD icon in case anyone ever ↵	Michal Moskal	2011-05-12
\| \| \| \| \| \| \| \| \| \| \| \|	needs it
* \| \|	Dafny: fixed bugs in resolution of multi-dimensional arrays	Rustan Leino	2011-05-12
\| \| \|
* \| \|	Merge	Rustan Leino	2011-05-12
\|\ \ \
* \| \| \|	Dafny: forbid "decreases *" on ghost loops	Rustan Leino	2011-05-12
\| \| \| \|
\| \| \| *	Merge	Mike Barnett	2011-05-12
\| \| \| \|\ \| \| \|_\|/ \| \|/\| \|
\| \| \| *	Trying to fix the bound expression simplifier.	Mike Barnett	2011-05-12
\| \| \| \|
\| * \| \|	added examples of generics and string support needed by Poirot	10shb	2011-05-12
\|/ / /
* \| \|	Merge	Rustan Leino	2011-05-11
\|\ \ \
* \| \| \|	More files for Hg to ignore	Rustan Leino	2011-05-11
\| \| \| \|
\| * \| \|	first cut at handling generics	qadeer	2011-05-11
\| \| \|/ \| \|/\|
\| \| *	Dafny:	Rustan Leino	2011-05-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword) * check that arrays are not null when accessed * added dafny1/FindZero.dfy test case
* \| \|	Merge	Rustan Leino	2011-05-11
\|\ \ \
* \| \| \|	Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵	Rustan Leino	2011-05-11
\| \|/ / \|/\| \| \| \| \| \| \| \|	avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
\| * \|	Dafny: Fixed non-compiling C# code in DafnyRuntime.cs	Rustan Leino	2011-05-11
\| \| \|
* \| \|	simplified the translation of assignments	qadeer	2011-05-10
\| \| \|
* \| \|	Merge	Mike Barnett	2011-05-10
\|\ \ \
* \| \| \|	Oops. Last checkin did not contain the changes for the catch clause change when	Mike Barnett	2011-05-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	translating a method body.