debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	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
\|
*	<Boogie> Removed the AssemblyInfo.cs file from Isabelle.	tabarbe	2010-07-16
\|
*	<Boogie> Removed references to AssemblyInfo.cs files - unnecessary for the ↵	tabarbe	2010-07-16
\| \| \| \|	building/execution of the program
*	<Boogie> BoogieDriver.csproj was missing a reference to AbsInt. Remedied ↵	tabarbe	2010-07-16
\| \| \| \|	that issue. <\Boogie>
*	Boogie build failed	codeplexbot	2010-07-16
\|
*	Chalice: Removed the restriction that "holds" must occur only in positive ↵	mueller	2010-07-16
\| \| \| \|	positions.
*	Visual Studio 2010 integration for Dafny and Chalice. See the "How to ↵	rustanleino	2010-07-15
\| \| \| \|	install binaries" link from the boogie.codeplex.com home page.
*	Boogie: Generated Code Contracts settings for BoogieDriver.csproj ↵	tabarbe	2010-07-15
\| \| \| \|	(everything disabled).
*	Boogie/Isabelle: Added tags of some places that generate errors when Code ↵	tabarbe	2010-07-15
\| \| \| \|	Contracts checking is on, that should resolve once Core ports
*	<Boogie> This dll is not one that needs to be in the depot. It should be ↵	tabarbe	2010-07-15
\| \| \| \|	added in manually.
*	<Boogie> <Isabelle> Turned off Code Contracts Runtime Checking. Will enable ↵	tabarbe	2010-07-15
\| \| \| \|	on all ports once Core is ported. <\Isabelle> <\Boogie>
*	Chalice: revert minor commit; add cygwin python make script	kyessenov	2010-07-15
\|
*	Oops, reverted my local changes to the build script.	kyessenov	2010-07-15
\|
*	Chalice: fix a bug for boogie print-out of a sequence class	kyessenov	2010-07-15
\|
*	Fix for cyrptographic signing error.	kyessenov	2010-07-14
\|