debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Make the -mv option use the new Model class.	MichalMoskal	2010-10-12
\|
*	Get rid of some CCI dependencies in Driver	MichalMoskal	2010-10-07
\|
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	Boogie:	rustanleino	2010-09-23
\| \| \| \| \| \|	* Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument
*	Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.	akashlal	2010-09-18
\|
*	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
*	Fix for extractLoops	akashlal	2010-09-04
\|
*	Added a fix to extract loops code so that it returns a more comprehensive ↵	qadeer	2010-09-03
\| \| \| \|	map of block names to original blocks.
*	fixed bug in extract loops by ensuring that loop extraction is done in ↵	qadeer	2010-09-01
\| \| \| \|	nesting order
*	Added a way of recovering counterexample paths after loop extraction. ↵	akashlal	2010-09-01
\| \| \| \|	Stable, but still buggy.
*	added a new api to Z3apiProcessTheoremProver for asserting axioms	qadeer	2010-08-29
\|
*	created a new build target called z3apidebug.	qadeer	2010-08-29
\| \| \| \| \|	only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver.
*	Boogie: Accidentally created a service references folder in Boogie's folder ↵	tabarbe	2010-08-27
\| \| \| \|	tree. Fixed that error.
*	Boogie: Removed some errors with code contracts (commenting out ↵	tabarbe	2010-08-27
\| \| \| \|	doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
*	Boogie: Changed the cce classes into one separate project, which every other ↵	tabarbe	2010-08-27
\| \| \| \|	project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
*	Boogie: Changed a messed-up refference to Z3api back to its previous state.	tabarbe	2010-08-27
\|
*	added some more apis to Z3api	qadeer	2010-08-27
\| \| \| \|	also added a reference from BoogieDriver to z3api
*	Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵	tabarbe	2010-08-27
\| \| \| \|	files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
*	Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵	tabarbe	2010-08-26
\| \| \| \|	Core to jive with recent changes made to the cce class.
*	further fixes to Z3api project trying to make it work; still a long way off.	qadeer	2010-08-23
\|
*	Boogie: Committing changed references	tabarbe	2010-08-20
\|
*	Boogie: Removed a completed task comment	tabarbe	2010-08-19
\|
*	Boogie: Committing changed references	tabarbe	2010-08-13
\|
*	Added the option /extractLoops to extract loops as procedure calls. If ↵	qadeer	2010-08-11
\| \| \| \|	either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
*	Boogie: Sorry about that - no need for the conditional compilation	tabarbe	2010-08-09
\|
*	Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.cs	tabarbe	2010-08-09
\|
*	fixed path to the binaries directory; there was an extra .."	qadeer	2010-08-03
\|
*	Boogie: Changed BoogieDriver.cs to use a copy of cce.cs, rather than an ↵	tabarbe	2010-07-30
\| \| \| \|	internal cce.cs class.
*	Made consistent the way all of the C# projects sign themselves and include ↵	mikebarnett	2010-07-30
\| \| \| \|	the version information.
*	Changed reference to AbsInt from a dll reference to a project reference.	mikebarnett	2010-07-28
\|
*	Boogie: VCGeneration port part 3/3: Updating sources to reference new ↵	tabarbe	2010-07-28
\| \| \| \|	project; making Core work with the port by removing the nonnull requirements on one abstract method.
*	Boogie: Committing my port of simplify, along with the slightly changed ↵	tabarbe	2010-07-23
\| \| \| \|	references of simplify's dependents.
*	Boogie: Committing my port of the SMTLib project	tabarbe	2010-07-22
\|
*	Boogie: Repaired a reentrancy error in Z3/Simplify.	tabarbe	2010-07-22
\|
*	Boogie: The reference to Z3 was dropped during the commit. Here it is back.	tabarbe	2010-07-20
\|
*	Boogie: Forgot to check in this file. Hope no one tried to rebuild without ↵	tabarbe	2010-07-19
\| \| \| \|	it. Sorry.
*	<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: Generated Code Contracts settings for BoogieDriver.csproj ↵	tabarbe	2010-07-15
\| \| \| \|	(everything disabled).
*	Fix for cyrptographic signing error.	kyessenov	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 && Boogie/BoogieDriver: Moved the AssemblyInfo.cs files into ↵	tabarbe	2010-07-14
\| \| \| \|	the required subfolders.
*	<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>
*	Renaming the old boogiedriver sources in preparation for syncing my ported ↵	tabarbe	2010-07-13
\| \| \| \|	changes.
*	/stratifiedInline:n eagerly inlines n times before calling the stratified ↵	akashlal	2010-07-10
\| \| \| \|	inlining algorithm.
*	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.
*	Boogie: Added an additional parameter 'defines' to the method ↵	wuestholz	2010-07-06
\| \| \| \|	'BoogiePL.Parser.Parse'.
*	Boogie: Fixed the build.	wuestholz	2010-07-02
\|
*	These 2 files are remnants of attempting the earlier planned method of ↵	tabarbe	2010-07-01
\| \| \| \| \| \|	renaming the .ssc files to .cs. They are being deleted because my porting work will be done completely on my local disc, until such time that I want to merge ported code into the project. With regards to the renaming problem, Stephan Tobies has found that the logs are kept on the CodePlex server, and are just not provided to the SVN client. He has created a Codeplex work item at http://codeplex.codeplex.com/workitem/25490. If it gets voted up sufficiently, it may get CodePlex to provide that log information, and thus help with future work regarding the Boogie depot.
*	As it turns out, the C# Intellisense compiler takes precedence over the ↵	tabarbe	2010-07-01
\| \| \| \|	Spec# Intellisense compiler during editing of a .cs file. So, in order to allow continued editing of Boogie, during my porting project I will not be renaming the .ssc files to .cs, but rather creating copies of, for example, the BoogieDriver project's files, naming them as .cs versions, and porting them the rest of the way into C#. I will build these projects and run the regression tests on them, and once (and only once) the reg tests are passed, I will commit the compiled C# output as the replacement for the Spec# component.