debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	DafnyExtension: new color (violet) for buffer snapshot sent to the verifier	Unknown	2012-09-07
\|
*	Merge	Unknown	2012-09-05
\|\
* \|	Dafny: fixed typo in latex mode	Unknown	2012-09-05
\| \|
\| *	Moved point at which preprocessed output is shown.	Unknown	2012-08-31
\| \|
\| *	Shared state is now properly abstracted in requires clauses.	Unknown	2012-08-31
\| \|
* \|	DafnyExtension: don't duplicate names of inherited identifiers	Unknown	2012-08-30
\| \|
* \|	Dafny: for refinements, don't consider a newly provided predicate body to be ↵	Unknown	2012-08-30
\| \| \| \| \| \| \| \|	an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be
* \|	DafnyExtension: changed how "_" is displayed (now display as a keyword, not ↵	Unknown	2012-08-30
\| \| \| \| \| \| \| \|	as an identifier definition)
* \|	Dafny: allow "_" as don't-care variable name	Unknown	2012-08-30
\| \|
\| *	Merge	Unknown	2012-08-30
\| \|\ \| \|/ \|/\|
\| *	Barriers now handled uniformly via bugle_barrier.	Unknown	2012-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Improved loop invariant inference so that procedure formal parameters are treated as constants. (This involved fixing a bug where a Formal was being dualised to a LocalVariable.) Fixed problem in GPUVerifyBoogieDriver where source location information was being looked for via a file name, rather than a full path. Cleaned up some code in GPUVerifyBoogieDriver.
* \|	Dafny: fixed bug in checking postconditions of functions that mention the ↵	Unknown	2012-08-29
\| \| \| \| \| \| \| \|	result the function itself
* \|	DafnyExtension: fixed bug (omitted case: VarDeclStmt has no Update component)	Unknown	2012-08-29
\| \|
* \|	Dafny: fixed contract violation in parser (for non-parsing Lhs production)	Unknown	2012-08-29
\|/
*	A small fix in variable definition analysis.	Unknown	2012-08-29
\|
*	Added generation of invariants to restrict source location to sensible values.	Egor Kyshtymov	2012-08-28
\| \| \| \| \|	Refactored Make...Variable() and FindOrCreate...Variable() functions to take a variable name as a parameter rather than the variable itself.
*	DafnyExtension: don't reverify a buffer with no changes	Rustan Leino	2012-08-27
\|
*	Dafny: fixed contract bug in resolver	Rustan Leino	2012-08-27
\|
*	Fix the whole-program translator so that exception handling is done	Unknown	2012-08-23
\| \| \| \| \| \| \| \| \| \|	correctly for virtual method calls. Changed the whole-program override for VisitMethodCall so that it creates a new CodeModel expression that does not contain virtual method calls and then translate that newly built expression. Treat type equality (and inequality) specially: translate it directly to a type test instead. But do it just for the idiom: "o.GetType == typeof(T)". In that case, turn it into "is#T$T($DynamicType(o))".
*	Make the modelExceptions option an integer.	Unknown	2012-08-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	0 means no modeling at all. 1 (which can be specified only if also specifying whole program translation) means that a fixpoint analysis will be done on all of the translated assemblies to compute the set of exceptions that each method can throw (even though we're using only the fact that a method throws anything at all, not the specific exceptions it can throw) so only calls to methods that can throw an exception have a branch after the call that checks to see if an exception has been thrown. Methods that are defined outside of the set of translated assemblies are assumed to not throw any exceptions! 2 means that every method is considered to be one that can throw an exception.
*	Added group information to race error reporting.	Egor Kyshtymov	2012-08-22
\|
*	Boogie build succeeded	CodeplexBot	2012-08-22
\|
*	Merge	Rustan Leino	2012-08-21
\|\
* \|	DafnyExtensions: better error handling	Rustan Leino	2012-08-21
\| \|
\| *	Extra debugging output for Houdini	Unknown	2012-08-21
\|/
*	Dafny and Boogie: get rid of 'static' fields in parser	Rustan Leino	2012-08-21
\|
*	Fixed problem where SOURCE variables were not being generated.	Unknown	2012-08-20
\|
*	Added functionality for race error reporting.	Egor Kyshtymov	2012-08-20
\|
*	DafnyExtension: fixed bad merge	Rustan Leino	2012-08-17
\|
*	Merge	Rustan Leino	2012-08-17
\|\
* \|	DafnyExtension: improved concurrency behavior	Unknown	2012-08-17
\| \|
\| *	DafnyExtension: report out-of-time and out-of-memory errors	Rustan Leino	2012-08-17
\|/
*	DafnyExtension: toward some fixes	Unknown	2012-08-17
\|
*	DafnyExtension: simplified display of type names and field names	Unknown	2012-08-17
\|
*	DafnyExtension: various improvements	Unknown	2012-08-16
\|
*	Fixed bug where source location attributes are not being attached to a CHECK	Unknown	2012-08-16
\| \| \| \|	call, and refactored code to avoid the duplication which caused this error.
*	DafnyExtension: improvements	Rustan Leino	2012-08-15
\|
*	DafnyExtension: do verification in a non-UI thread	Rustan Leino	2012-08-15
\|
*	DafnyExtension: fixed more missing cases for hover texts	Unknown	2012-08-15
\|
*	Dafny: fixed some bugs in the newly added DafnyExtension code	Unknown	2012-08-15
\|
*	Merge	Unknown	2012-08-15
\|\
* \|	Dafny: added Statement.SubExpressions getter	Unknown	2012-08-15
\| \| \| \| \| \| \| \|	DafnyExtension: added hover text for identifiers
* \|	Dafny: added Statement.SubExpressions getter	Unknown	2012-08-15
\| \| \| \| \| \| \| \|	DafnyExtension: added hover text for identifiers
* \|	Dafny: removed the defunct "havoc" keyword from various source-code highlighters	Unknown	2012-08-15
\| \|
\| *	Boogie build succeeded	CodeplexBot	2012-08-15
\| \|
* \|	Merge	Unknown	2012-08-14
\|\\|
* \|	Dafny emacs mode: changed a menu name (Does anyone ever use this menu anyhow?)	Unknown	2012-08-14
\| \|
* \|	Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension ↵	Unknown	2012-08-14
\| \| \| \| \| \| \| \|	crashing after certain deletes)
\| *	Also updated test15	Rustan Leino	2012-08-14
\| \|
\| *	Update test suite for commit 8a59fbb7ee34.	Peter Collingbourne	2012-08-14
\| \|