debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	changed inlining code so that candidate preconditions and postconditions are ↵	qadeer	2011-11-15
\| \| \| \|	ignored
*	Merge	qadeer	2011-11-14
\|\
* \|	fixed another bug in model parser related to datatype values	qadeer	2011-11-14
\| \| \| \| \| \| \| \|	cleaned up the code related to v1model
\| *	For some reason, these didn't get into the last commit.	Mike Barnett	2011-11-14
\| \|
\| *	Trying to get the generics translation correct...	Mike Barnett	2011-11-14
\|/
*	added the option /inlineDepth:n. This option defaults to -1. If the user ↵	qadeer	2011-11-13
\| \| \| \| \| \|	provides a non-negative number then that number is used to inline procedures not annotated by {:inline n} attribute.
*	Boogie build succeeded	CodeplexBot	2011-11-12
\|
*	Merge	qadeer	2011-11-11
\|\
\| *	moved the addition of selectors and testers to program.Resolve	qadeer	2011-11-11
\| \|
* \|	Produce unsat cores only when enabled (in stratified inlining)	Unknown	2011-11-11
\|/
*	Many, many bug fixes related to generics and some other random problems.	Mike Barnett	2011-11-10
\|
*	Dafny: allow assert/assume expressions in more places	Rustan Leino	2011-11-09
\|
*	Dafny: added assert/assume expressions	Rustan Leino	2011-11-09
\|
*	Merge	qadeer	2011-11-09
\|\
* \|	copied all attributes of the constructor (except for :constructor) to the ↵	qadeer	2011-11-09
\| \| \| \| \| \| \| \|	selector and membership functions
\| *	VCC: remove _vcc_math_type_ from type names	Michal Moskal	2011-11-09
\| \|
\| *	VCC: hide #limited# functions	Michal Moskal	2011-11-09
\| \|
\| *	Merge	Rustan Leino	2011-11-09
\| \|\
\| * \|	Dafny: moved definition of class.array into prelude, anticipating writing ↵	Rustan Leino	2011-11-09
\| \| \| \| \| \| \| \| \| \| \| \|	axioms that use it
\| * \|	Dafny: allow single-quote as a character in identifiers in the VS2010 mode	Rustan Leino	2011-11-09
\| \| \|
\| * \|	Dafny: added "multiset" keyword to syntax highlighting in emacs, vim, latex, VSX	Rustan Leino	2011-11-09
\| \| \|
\| \| *	Refactoring, and work on race checking contracts	Unknown	2011-11-09
\| \|/
\| *	Merge	Rustan Leino	2011-11-09
\| \|\
\| * \|	Dafny: fixed part of a type-inference issue with datatypes and the < ↵	Rustan Leino	2011-11-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	operator on datatypes Dafny: allow the well-formedness check of a function's specification to know that the function, on the current arguments, returns a value of the declared result type
\| \| *	Tagging EMIC CC.NET build 2.1.31109.0	VccBuildServer	2011-11-09
\| \| \|
\| \| *	BVD: don't do the "Duplicate entry exception"; uncomment for debugging	Michal Moskal	2011-11-08
\| \| \|
\| \| *	VCC: show output parameters as roots	Michal Moskal	2011-11-08
\| \|/ \|/\|
* \|	moved GPUVerify into its own solution	qadeer	2011-11-08
\|/
*	Merge	Rustan Leino	2011-11-08
\|\
* \|	Dafny: fixed bug in reads checking of array-to-sequence conversions	Rustan Leino	2011-11-08
\| \|
* \|	Dafny: Cleaned up proof of RevConcat in test case	Rustan Leino	2011-11-08
\| \|
\| *	Merge	Unknown	2011-11-08
\| \|\
\| * \|	Additions to GPU Verify for paper submission.	Unknown	2011-11-08
\| \| \|
\| \| *	some refactoring suggested by Michal	qadeer	2011-11-07
\| \| \|
\| \| *	Merge	qadeer	2011-11-07
\| \| \|\
\| \| * \	Merge	qadeer	2011-11-07
\| \| \|\ \ \| \|_\|/ / \|/\| \| \|
\| \| * \|	change in model parsing with datatype values	qadeer	2011-11-07
\| \| \| \|
* \| \| \|	Dafny: added a new /inductionHeuristic option	Rustan Leino	2011-11-04
\| \| \| \|
* \| \| \|	Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to ↵	Rustan Leino	2011-11-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	a previous lemma
* \| \| \|	Dafny: added options to make Induction Heuristic apply to array index ↵	Rustan Leino	2011-11-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	expressions
* \| \| \|	Merge	Rustan Leino	2011-11-03
\|\ \ \ \
* \| \| \| \|	Added some Dafny and Boogie test cases, including Turing's factorial ↵	Rustan Leino	2011-11-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	program, Hoare's classic FIND, and some induction tests for negative integers
\| \| \| * \|	Merge	qadeer	2011-11-01
\| \| \| \|\ \ \| \| \|_\|/ / \| \|/\| \| \|
\| \| \| * \|	deleted unused code	qadeer	2011-11-01
\| \| \| \| \|
\| * \| \| \|	Don't wipe out existing attributes when adding {:extern}	Mike Barnett	2011-11-01
\| \| \|/ / \| \|/\| \|
\| * \| \|	Boogie build succeeded	CodeplexBot	2011-11-01
\|/ / /
* \| \|	Merge	Rustan Leino	2011-10-31
\|\ \ \
\| * \| \|	File to experiment with type encoding for .NET.	Mike Barnett	2011-10-31
\| \| \| \|
* \| \| \|	Merge	Rustan Leino	2011-10-31
\|\ \ \ \
\| \| * \| \|	Major changes to the translator traversers because they now are based on the	Mike Barnett	2011-10-31
\| \|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	new traversers. (The old ones have been marked as obsolete.) All types are now encoded as "datatypes" in Boogie. So non-generic types are nullary functions and generic types just have at least one type argument. Lots of other fixes: string encoding of names is now done by negating Boogie's regular expression for identifiers, etc.