debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	further refactoring of SI;	qadeer	2012-05-29
\| \| \| \|	removed the program argument to call to VerifyImplementation in Dafny
*	removed lazy inlining	qadeer	2012-04-28
\|
*	Dafny: fixed build error	Rustan Leino	2012-03-09
\|
*	Dafny: changed translation to be sensitive to refinement inheritance; this ↵	Rustan Leino	2012-01-09
\| \| \| \|	feature is now functional, provided the refining module does not add or change anything
*	Boogie: output number of proof obligations (asserts) along with timing ↵	Rustan Leino	2012-01-09
\| \| \| \|	information when using the /trace option
*	Dafny: make /infer:j (the new interval domain) the default abstract interpreter	Rustan Leino	2012-01-05
\|
*	Dafny: compile to .exe only if there is a Main method; otherwise, compile to ↵	Rustan Leino	2011-12-19
\| \| \| \|	a .dll
*	Dafny: Made sure that error locations refer to the Dafny program, even if ↵	wuestholz	2011-12-15
\| \| \| \|	the /print option is used.
*	Merge	Rustan Leino	2011-12-07
\|\
\| *	Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable ↵	wuestholz	2011-12-07
\| \| \| \| \| \| \| \|	wellformedness checks).
* \|	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}
*	Dafny: call C# compiler directly from inside Dafny, and optionally produce a ↵	Rustan Leino	2011-11-22
\| \| \| \|	.cs file with the new /spillTargetCode switch
*	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.
*	Merge	Rustan Leino	2011-09-28
\|\
\| *	Dafny: Added a 'Checked' configuration and fixed some runtime assertion ↵	wuestholz	2011-09-23
\| \| \| \| \| \| \| \|	violations.
* \|	Dafny: generate a compiler error upon encountering an assume statement	Rustan Leino	2011-09-11
\|/ \| \| \|	Dafny: don't compile programs unless all methods have been verified (or a forced compile is requested)
*	Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵	wuestholz	2011-07-15
\| \| \| \|	some trailing whitespace.
*	- fixed a bug in DafnyModelUtils.fs (reading set values from models)	Unknown	2011-07-11
\| \| \| \| \|	- changed Dafny so that it returns an exit code - changed CheckDafnyProgram so that it checks Dafny exit code as well
*	Added option to force Dafny compilation, even if verification fails.	Jason Koenig	2011-06-30
\|
*	Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵	mikebarnett	2011-03-10
\| \| \| \| \| \|	dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
*	Dafny: Non-empty Visual-Studio error messages for related split-expr locations.	rustanleino	2011-02-27
\| \| \| \|	Dafny: Forbid jumps from ghost code.
*	Dafny: Improved scheme for splitting expressions. Also, report each split ↵	rustanleino	2011-02-19
\| \| \| \|	in error messages.
*	Dafny: removed CEV instrumentation	rustanleino	2011-02-03
\|
*	Dafny: white-space deltas in source code	rustanleino	2011-02-02
\|
*	Dafny: Fixed some build issues with duplicated and malformed Code Contracts.	rustanleino	2011-01-13
\|
*	Add functions generated in lambda-expansion of function body to top-level ↵	MichalMoskal	2010-12-17
\| \| \| \|	program declarations.
*	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
\|
*	forgot to check this file in	qadeer	2010-11-28
\|
*	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.
*	Dafny: a partial first crack at a Dafny model-viewer provider, including ↵	rustanleino	2010-11-01
\| \| \| \|	captureState mark-ups in the Boogie code generated from Dafny
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	Dafny:	rustanleino	2010-09-14
\| \| \| \| \| \| \| \|	* Added internal support for multi-dimensional arrays (but not all surface syntax is there yet) * Removed unused variables from Dafny.atg Boogie and Dafny: * Improved error message for postcondition violations
*	Dafny: Made line endings consistent	tabarbe	2010-08-04
\|
*	Dafny: Removed trailing spaces in code	tabarbe	2010-08-04
\|
*	Fixed some infelicities in the project files.	mikebarnett	2010-08-04
\|
*	fixed path to the binaries directory; there was an extra .."	qadeer	2010-08-03
\|
*	Also build Boogie and Dafny projects in 32-bit configurations.	rustanleino	2010-07-30
\| \| \| \|	Don't insist on DafnyDriver picking up the LKG version (1.0.21125.0) of the Spec# runtime (in fact, most builders will probably have 1.0.21126.0).
*	Sign both of the Dafny projects and have Dafny.exe get a version number as well.	mikebarnett	2010-07-30
\|
*	Dafny: DafnyDriver port part 3/3: Updating sources to reference new project.	tabarbe	2010-07-28
\|
*	Dafny: DafnyDriver port part 2/3: Adding new dependent file, removing ↵	tabarbe	2010-07-28
\| \| \| \|	unnecessary one.
*	Dafny: DafnyDriver port part 1/3: Replacing old source files with ported version	tabarbe	2010-07-28
\|
*	Dafny/DafnyDriver: Renaming source files in preparation for port commit	tabarbe	2010-07-28
\|
*	Boogie: Added an additional parameter 'defines' to the method ↵	wuestholz	2010-07-06
\| \| \| \|	'BoogiePL.Parser.Parse'.
*	Updated the frame files to work with the latest Coco/R. This entails not ↵	mikebarnett	2010-06-22
\| \| \| \| \| \|	having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories. Lots of code changes to compensate for the new frame files.
*	Dafny:	rustanleino	2010-05-21
\| \| \| \| \| \| \|	* Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks
*	Dafny:	rustanleino	2010-05-06
\| \| \| \| \| \| \| \|	* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies) * Added "print" statement (to make running compiled programs more interesting) * Changed name of default class from $default to _default Boogie: * Included "lambda" as a keyword in emacs and latex style files
*	Dafny:	rustanleino	2010-03-12
\| \| \| \| \|	* Modifies clause checking is now done with each update, instead of at the end of the method. Not only does this improve error messages, but on some examples, it gives a dramatic speed-up (2x) in proving time. * bugfix: range expressions of foreach statements were previously ignored during Translation
*	Dafny: Added stratosphere tests for datatypes--that is, it is now checked ↵	rustanleino	2010-03-11
\| \| \| \|	that every datatype has some value.
*	Added resolution and translation of algebraic datatypes and (in function ↵	rustanleino	2009-11-20
\| \| \| \| \| \|	bodies) match expressions. Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.