debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	Boogie:	rustanleino	2010-09-24
\| \| \| \| \|	* Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators. * Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time.
*	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
*	bunch of fixes related to Boogie error model generation from the Z3 error ↵	qadeer	2010-09-03
\| \| \| \|	model generation
*	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.
*	BeginCheck now adds context.Axioms as well as the conjecture to the context.	qadeer	2010-08-29
\| \| \| \|	Also started using the new quantifier api.
*	Added a constructor to a contract class otherwise the compiler complained ↵	mikebarnett	2010-08-28
\| \| \| \|	about the default nullary one calling its base class nullary ctor, and there wasn't one.
*	Boogie: Simplify: Added a contracts class that I forgot in the initial porting.	tabarbe	2010-08-27
\|
*	Boogie: Commented out all occurences of repeated inherited contracts - makes ↵	tabarbe	2010-08-27
\| \| \| \|	fewer error messages when compiling with runtime checking on.
*	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).
*	fixed bug with function name look up	qadeer	2010-08-27
\|
*	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: Basetypes port 3/3: Committing changed references	tabarbe	2010-08-27
\| \| \| \|	Z3api.csproj shouldn't get in the way this time 'round.
*	Bug fixes and logging for z3api	akashlal	2010-08-27
\|
*	added some more apis to Z3api	qadeer	2010-08-27
\| \| \| \|	also added a reference from BoogieDriver to z3api
*	Added a (temporary) CCE file so that Z3Api can build.	mikebarnett	2010-08-27
\|
*	simplified the push-pop business	qadeer	2010-08-27
\|
*	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.
*	Minor additions to z3api	akashlal	2010-08-26
\|
*	bug fixes in z3api	qadeer	2010-08-26
\|
*	fixed z3api so that it works on small examples now.	qadeer	2010-08-24
\|
*	Report a bug in Z3 instead of evil input "?"	kyessenov	2010-08-23
\|
*	further fixes to Z3api project trying to make it work; still a long way off.	qadeer	2010-08-23
\|
*	Boogie: Changed reference of Z3api.csproj to the differently-GUIDded ↵	tabarbe	2010-08-20
\| \| \| \|	Core.csproj, rather than Core.sscproj's old GUID.
*	Boogie: Committing changed references	tabarbe	2010-08-20
\|
*	Added the port of Z3api. It is simply a port to the latest version of ↵	qadeer	2010-08-20
\| \| \| \|	Microsoft.Z3.dll and to C#. It does not work yet.
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Removed a completed task comment, added a forgotten ↵	tabarbe	2010-08-19
\| \| \| \|	Contract.EnsuresOnThrow<>()
*	Boogie: Removed a completed task comment	tabarbe	2010-08-19
\|
*	Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m ↵	MichalMoskal	2010-08-18
\| \| \| \|	use separate Z3 type per Boogie type
*	Make /typeEncoding:m work with arrays	MichalMoskal	2010-08-18
\|
*	Boogie: Committing changed references	tabarbe	2010-08-13
\|
*	Boogie: Added boolean code expressions (sans well-formedness checks on the ↵	rustanleino	2010-08-10
\| \| \| \|	input).
*	Remove -z3DebugTraces and -z3Mam options (no longer working). Rename the ↵	MichalMoskal	2010-08-06
\| \| \| \|	-z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).
*	Fixup line-endings.	MichalMoskal	2010-08-06
\|
*	Boogie: added /z3bv option that overrides the current setting of Z3 options ↵	stobies	2010-08-06
\| \| \| \|	for better performance on VCs that are heavy on bitvector arithmetic
*	Remove support for Z3 V1 and clean up parameter processing code for Z3	stobies	2010-08-06
\| \| \| \|	svn-ignoring some build artifacts
*	Boogie: cleanup option handling code for Z3	stobies	2010-08-05
\|
*	Boogie: Removed trailing spaces in code	tabarbe	2010-08-04
\|
*	Boogie: The deletion of those files did not hold, lemme try again.	tabarbe	2010-07-30
\|
*	Boogie: Removed cce.cs's from the provers, because they all reference ↵	tabarbe	2010-07-30
\| \| \| \|	projects which have a (more up-to-date) copy of cce.cs.
*	Made consistent the way all of the C# projects sign themselves and include ↵	mikebarnett	2010-07-30
\| \| \| \|	the version information.
*	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.
*	Fixed reference to VCGeneration project. Mistakenly checked in project files ↵	mikebarnett	2010-07-28
\| \| \| \|	were pointing to the yet-to-exist C# version.
*	Boogie Provers: Changed the references from binary to project references.	tabarbe	2010-07-27
\|