debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	<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
\|
*	Missing file needed for new C# projects.	mikebarnett	2010-07-14
\|
*	Syntax file for Chalice.	kyessenov	2010-07-14
\|
*	Fixed reference to InterimKey.snk.	mikebarnett	2010-07-14
\|
*	Fixed project files to point to references correctly and also to remove ↵	mikebarnett	2010-07-14
\| \| \| \|	assembly signing information from AssemblyInfo.cs files (which since that was the only thing in BoogieDriver's assembly info, deleted that file). Now signing information is specified in the project files.
*	Boogie/Isabelle: Had to redirect some references required for building.	tabarbe	2010-07-14
\|
*	Boogie/Isabelle && Boogie/BoogieDriver: Moved the AssemblyInfo.cs files into ↵	tabarbe	2010-07-14
\| \| \| \|	the required subfolders.
*	Chalice: No longer use Mask for "held" field; instead, only use the value ↵	rustanleino	2010-07-14
\| \| \| \|	of the "held" field in the heap
*	Isabelle: No need for this file anymore.	tabarbe	2010-07-14
\|
*	Boogie/Isabelle: Yet again trying to get Prover.cs committing.	tabarbe	2010-07-14
\|
*	Boogie: As the filename suggests, I am trying to give Tortoise a kick in the ↵	tabarbe	2010-07-14
\| \| \| \|	pants here.
*	Boogie/Isabelle: Committing Isabelle port	tabarbe	2010-07-14
\|
*	Boogie/Isabelle: Committing Isabelle port	tabarbe	2010-07-14
\|
*	Tortoise SVN screwed up previous commit.	kyessenov	2010-07-14
\|
*	Boogie: More rename snafu fixing	tabarbe	2010-07-14
\|
*	<Boogie> More rename fixing </Boogie>	tabarbe	2010-07-14
\|
*	<Boogie> <Isabelle> Fixing rename error <\Isabelle> <\Boogie>	tabarbe	2010-07-14
\|
*	<Boogie> <Isabelle> Renaming the source files of the Isabelle project in ↵	tabarbe	2010-07-14
\| \| \| \|	preparation for integrating my ported copies of that project. <\Isabelle> <\Boogie>
*	<Boogie> <BoogieDriver> Committing my porting of BoogieDriver.cs and the ↵	tabarbe	2010-07-14
\| \| \| \| \| \| \|	changes made to the .csproj and Boogie.sln file that are necessary for the port. My Microsoft alias is t-abarbe, so if any of this stuff breaks for you, you can contact me. </BoogieDriver> </Boogie>
*	<Boogie> <BoogieDriver> Committing my porting of BoogieDriver.cs and the ↵	tabarbe	2010-07-14
\| \| \| \| \| \| \|	changes made to the .csproj and Boogie.sln file that are necessary for the port. My Microsoft alias is t-abarbe, so if any of this stuff breaks for you, you can contact me. </BoogieDriver> </Boogie>
*	Dafny: added comments for refinements assertions.	kyessenov	2010-07-14
\|
*	Dafny: better error reporting on resolution of refinements. Replace ↵	kyessenov	2010-07-14
\| \| \| \|	assertions with "if"s to handle errors gently and add cycle detection check.
*	Renaming the old boogiedriver sources in preparation for syncing my ported ↵	tabarbe	2010-07-13
\| \| \| \|	changes.
*	[Aste] Success: Committing summary due to changes.	codeplexbot	2010-07-10
\|
*	/stratifiedInline:n eagerly inlines n times before calling the stratified ↵	akashlal	2010-07-10
\| \| \| \|	inlining algorithm.
*	Dafny: Axiom about inverting a set union operation, similar to the recent ↵	rustanleino	2010-07-09
\| \| \| \|	ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.
*	Another part of the testing with that file.	tabarbe	2010-07-08
\|
*	Another test using that Multilingual Greetings file	tabarbe	2010-07-08
\|
*	Removed a few unnecessary nonnull type declarations, as I also removed some ↵	tabarbe	2010-07-07
\| \| \| \|	unnecessarry "Contract.Assert"s from my porting of Boogie.
*	[Aste] Success: Committing summary due to changes.	codeplexbot	2010-07-07
\|
*	Boogie: Bug fix for stratified inlining	akashlal	2010-07-07
\|
*	Boogie: Added stratified inlining. It is enabled using the flag ↵	akashlal	2010-07-07
\| \| \| \|	/stratifiedInline:1.
*	Dafny: keep counters for loops, temporary variables across two ↵	kyessenov	2010-07-07
\| \| \| \|	implementations in the refinement VC
*	[Aste] Success: Committing summary due to changes.	codeplexbot	2010-07-06
\|
*	Dafny:	rustanleino	2010-07-06
\| \| \| \| \|	* changed rule about scoping of out-parameters * added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
*	[Aste] Added summary.log	codeplexbot	2010-07-06
\|
*	Added a comment noting that this test fails with Z3 2.4.	mschwerhoff	2010-07-06
\|
*	Boogie: Added an additional parameter 'defines' to the method ↵	wuestholz	2010-07-06
\| \| \| \|	'BoogiePL.Parser.Parse'.
*	General hygiene: introduced (fixed) a helper method that creates Boogie ↵	mikebarnett	2010-07-05
\| \| \| \|	tokens. Made it an extension method that takes any object implementing IObjectWithLocations. Much easier to use within the translator.
*	Cleaned up the sink: removed the OutVars, which was state the sink needed ↵	mikebarnett	2010-07-05
\| \| \| \|	only for assigning the local copy of a method's parameter to the out parameter of the Boogie procedure. But now that is simplified: instead of three versions of each parameter (in, local, and out), there are only two: in and out. For a parameter that is not by reference and is not an out parameter (i.e., just a plain pass-by-value parameter), the "out" version is a local variable. Otherwise it is an out parameter of the Boogie procedure.
*	Forgotten file: Sink.cs	mikebarnett	2010-07-05
\| \| \| \|	Added an override of ToString so MethodParameters show up nicer in the debugger.
*	Chalice: Changed definition of waitlevel to take into account rdlock. ↵	mueller	2010-07-03
\| \| \| \|	Adapted definition of IsGoodInhaleState and an axiom.
*	Dafny: added assertions in the refinement obligation necessitating that the ↵	kyessenov	2010-07-03
\| \| \| \|	return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call.
*	Dafny: Support class type parameters in refinements. Added another ↵	kyessenov	2010-07-02
\| \| \| \|	regression test -- a sequence refined by a singly linked list.
*	Introduction of the Sink: a global object that is threaded through all of ↵	mikebarnett	2010-07-02
\| \| \| \|	the traversers and which contains the information that they need to share with each other.
*	Dafny: added Carrol Morgan's calculator regression test.	kyessenov	2010-07-02
\|