debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Normalise line endings using a .gitattributes file. Unfortunately	Dan Liew	2015-06-28
\| \| \| \| \| \|	this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
*	Fix Boogie so it compiled with mono. Patch by Dan Liew.	Ally Donaldson	2014-01-14
\|
*	Boogie: added type 'real' with overloaded arithmetic operations plus real ↵	boehmes	2012-09-27
\| \| \| \| \| \| \| \| \|	division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
*	Removed AIFramework from Boogie -- use native trivial or native ↵	boehmes	2012-09-27
\| \| \| \| \| \| \|	interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
*	Trying to merge with recent changes, failing.	Ken McMillan	2012-06-05
\|\
\| *	Some changes to support expanded use of z3api.	Ken McMillan	2012-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Should not affect function of other provers. There is an option added in Check.cs to allow creation of a Checker with a user-specified ProverContext. Also, some extension of z3api prover context to support conversion of Z3 formulas back to VCExpr. Finally, some experimental code, not enabled, to allow conversion of loops to recursion with "head recursion" rather than "tail recursion" (i.e., recursive call before loop body rather than after).
* \|	eliminated class ErrorModel	qadeer	2012-04-28
\| \|
* \|	bug fix	qadeer	2012-02-29
\| \|
* \|	small changes to z3api to make it compile after the z3 project was ripped out	qadeer	2012-02-29
\| \| \| \| \| \| \| \|	added CheckOutcomeCore to the class that extends ProverInterface; should be checked
* \|	further fixes related to using uninterpreted function for error traces	qadeer	2012-02-25
\|/ \| \| \|	removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
*	Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵	Rustan Leino	2011-11-15
\| \| \| \|	CommandLineOptions to separate the options that belong to these 3 tools.
*	further refactoring	qadeer	2011-06-24
\|
*	fixes to z3api	qadeer	2011-06-24
\|
*	clean up in z3api	qadeer	2011-06-22
\|
*	various fixes to port to latest version of Microsoft.Z3.dll	qadeer	2011-06-22
\|
*	Fixed a tricky bug in z3api	akashlal	2011-03-18
\|
*	Re-enabled quantifier checking in the Checked configuration.	mikebarnett	2011-03-16
\|
*	Turn off quantifier checking in the runtime checking.	mikebarnett	2011-03-14
\|
*	Added a new solution configuration, Checked, that builds the Checked ↵	mikebarnett	2011-03-07
\| \| \| \|	configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
*	Better support for timeout	akashlal	2011-02-12
\|
*	implemented /UseUnsatCoreForInlining option for use in stratified inlining	qadeer	2011-02-06
\|
*	Use a made-up name when Context.Lookup() cannot find a name	MichalMoskal	2010-12-10
\|
*	Don't crash in Context.Lookup when the namer has never seen the name. This ↵	MichalMoskal	2010-12-10
\| \| \| \|	happens when the name is never used in the VC (e.g. it gets peep-hole optimized).
*	z3api: Bug fix with timeout. Use CheckAssumptions.	akashlal	2010-12-07
\|
*	Added version.cs as link to those projects that were missing it	stobies	2010-12-06
\| \| \| \|	Select 4.0 client profile on all projects
*	Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln	qadeer	2010-12-01
\|
*	z3api: Print log in smtlib2 format. Use CheckAssumptions (currently broken)	akashlal	2010-11-29
\|
*	Added CheckAssumptions api interface	akashlal	2010-11-28
\|
*	added a fix for a bug in the Evaluate function.	qadeer	2010-11-27
\|
*	changed the procedure Check so that the conflict clause is blocked only when ↵	qadeer	2010-11-27
\| \| \| \|	more than one counterexample is needed.
*	Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵	qadeer	2010-11-27
\| \| \| \|	Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
*	Some changes to the prover interface to make way for z3-api.	akashlal	2010-11-24
\|
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	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.
*	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: 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
\|
*	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.