debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Chalice: pretty printer now prints element type for sequences; fixed a bug ↵	kyessenov	2010-07-27
\| \| \| \|	in copying resolved member in sequence accesses; added graph closure (DSW) verification example
*	Boogie build failed	codeplexbot	2010-07-24
\|
*	Also traverse bodies of function definitions when performing lambda expansion.	sboehme	2010-07-23
\|
*	Boogie: AssemblyInfo.cs is no longer required for the build; cce.cs is.	tabarbe	2010-07-23
\|
*	Boogie: Committing my port of simplify, along with the slightly changed ↵	tabarbe	2010-07-23
\| \| \| \|	references of simplify's dependents.
*	Boogie: Renaming Simplify.sscproj and source files in preparation for ↵	tabarbe	2010-07-23
\| \| \| \|	committing my port of Simplify.csproj.
*	Boogie build succeeded	codeplexbot	2010-07-23
\|
*	Boogie: One last file to add for the port commit. Also, AssemblyInfo.ssc is ↵	tabarbe	2010-07-22
\| \| \| \|	no longer necessarry.
*	Boogie: Committing my port of the SMTLib project	tabarbe	2010-07-22
\|
*	Boogie: Renaming the source files for the SMTLib project in preparation for ↵	tabarbe	2010-07-22
\| \| \| \|	commiting my port of the project.
*	Boogie: This file is no longer necessary, with how the csproj file is ↵	tabarbe	2010-07-22
\| \| \| \|	structured.
*	Boogie: Repaired a reentrancy error in Z3/Simplify.	tabarbe	2010-07-22
\|
*	Boogie build succeeded, 25 test(s) failed	codeplexbot	2010-07-22
\|
*	Boogie: Looks like the default namespace should be Microsoft.Boogie.Z3, ↵	tabarbe	2010-07-22
\| \| \| \|	rather than Provers.Z3. I updated that.
*	Boogie: Changed the assembly name for the Z3 project to Provers.Z3.dll, so ↵	tabarbe	2010-07-22
\| \| \| \|	that it matches the namespace.
*	Boogie build succeeded, 25 test(s) failed	codeplexbot	2010-07-22
\|
*	Chalice: bug -- permissions were implicity converted to Booge expressions ↵	kyessenov	2010-07-22
\| \| \| \|	(due to "implicit def")
*	Chalice: bug -- expression substitution should preserve typing	kyessenov	2010-07-22
\|
*	Chalice: sequence access wildcards a[]. and a[*].f have been implemented ↵	kyessenov	2010-07-22
\| \| \| \|	(sans checking for epsilon going beyond infinity and rd(...,*) permissions)
*	Chalice: introduced proper AST nodes for permission expressions and ↵	kyessenov	2010-07-21
\| \| \| \|	permissions. This gets of redundancy in treating acc and rd in many places and should hopefully make permissions code more comprehensible
*	Boogie: Fixing incorrect referencing of Microsoft.Contracts (the Code ↵	tabarbe	2010-07-21
\| \| \| \|	Contracts dll) in AbsInt, Isabelle, and Z3
*	Boogie: Forgot this file when I checked in the port of Z3. (cce = Code ↵	tabarbe	2010-07-21
\| \| \| \|	Contracts Extensions - utility methods for the port that are not present in Code Contracts.)
*	Boogie build failed	codeplexbot	2010-07-21
\|
*	Chalice: fixed typos in strings; trying out committing with TFS	kyessenov	2010-07-21
\|
*	Boogie: The reference to Z3 was dropped during the commit. Here it is back.	tabarbe	2010-07-20
\|
*	Boogie: Committing ported version of Z3.	tabarbe	2010-07-20
\|
*	Chalice: added surface syntax for acc(s[].) and acc(s[*].f); extended AST, ↵	kyessenov	2010-07-20
\| \| \| \|	resolver, printer; translation is not yet done
*	Boogie: Typo with the renaming. Fixed	tabarbe	2010-07-20
\|
*	Boogie: Let's try that rename again, shall we?	tabarbe	2010-07-20
\|
*	Boogie: Rename didn't work. Resetting to try again	tabarbe	2010-07-20
\|
*	Boogie/Z3: Renaming the sources for Z3 in preparation for commit of my port ↵	tabarbe	2010-07-20
\| \| \| \|	of the project.
*	Chalice: fixed a bug with permission operations treating AccessAll not as a ↵	kyessenov	2010-07-20
\| \| \| \|	permission expression; refactored Translator my moving prelude/implicits into TranslatorHelper for consistency
*	Boogie build succeeded	codeplexbot	2010-07-20
\|
*	Chalice: added type information for sequences ("where" clauses in local ↵	kyessenov	2010-07-20
\| \| \| \|	variable declarations and method/function formals); the clause says that every element in a sequence is either null or its dtype is the element type
*	Chalice: adding support for sequence local variables; removed ClassType from ↵	kyessenov	2010-07-20
\| \| \| \|	Boogie since it was maskng bad job done by Translator; fixing warnings in case we ever decide to switch to newer Scala compiler
*	Boogie/Isabelle: implemented missing translation of if-then-else expressions	sboehme	2010-07-20
\|
*	Chalice: extended substitutor to handle "exists" quantifier and sequence ↵	kyessenov	2010-07-20
\| \| \| \|	containment; refactoring and preparing to extend wild card permissions to sequences
*	VS2010 integration: fixed typo in Boogie mode (install for .bpl files, not ↵	rustanleino	2010-07-19
\| \| \| \| \| \|	.dfy file; duh!) Chalice tests: removed machine-specific path from test.bat (replacing the file reference with just 'scala', which in some ways is machine-specific too)
*	Chalice: added sequence containment surface syntax ("in" comparison ↵	kyessenov	2010-07-19
\| \| \| \|	operator); cleaned up some deprecation warnings; resolved ambiguity with "unfolding ... in" expression
*	Boogie: Changed how the references in AbsInt are referenced, and fixed a ↵	tabarbe	2010-07-19
\| \| \| \|	typo in the Spec# version of Z3's ProverInterface.ssc
*	Chalice: Introduced '[[ S ]]' as a shorthand syntax for 'lock (this) { S ↵	rustanleino	2010-07-19
\| \| \| \| \| \| \|	}'. Think of the new brackets as atomicity brackets (see PetersonsAlgorithm.chalice) Chalice: Added Peterson's algorithm to test suite (safety properties only) VS 2010 integration: Updated Chalice and Dafny modes, added keyword highlighting for a new Boogie mode
*	Boogie: Forgot to check in this file. Hope no one tried to rebuild without ↵	tabarbe	2010-07-19
\| \| \| \|	it. Sorry.
*	Boogie: Whoops, forgot to check this in. Sorry if it broke the build.	tabarbe	2010-07-19
\|
*	Chalice: added "exists" quantifier; changed surface syntax for quantifier ↵	kyessenov	2010-07-19
\| \| \| \|	expressions
*	Boogie: Added interprocedural live variable analysis. Flag to turn it on: ↵	akashlal	2010-07-19
\| \| \| \|	"/liveVariableAnalysis:2"
*	Chalice: Re-designed lockchange on methods and loops. The lockchange clause ↵	mueller	2010-07-18
\| \| \| \|	is now required to list all objects whose held or rdheld field has changed since the _method_ prestate. It seems desirable to exclude objects that were not allocated in the prestate, but this feature is not implemented yet.
*	Boogie build succeeded	codeplexbot	2010-07-17
\|
*	Boogie: I have successfully ported the AbsInt project. It passes all ↵	tabarbe	2010-07-16
\| \| \| \| \| \|	regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL. Address any error complaints to t-abarbe@microsoft.com
*	Boogie: Renamed the AbsInt sources for use in the port I have done. ↵	tabarbe	2010-07-16
\| \| \| \|	Regressions with the changed code will take ~10 minutes. I hope I don't break anyone's build.
*	<Boogie> Final removal of Isabelle's mention of a Properties.cs file	tabarbe	2010-07-16
\|