debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Boogie: handle absolute paths on *nix correctly	Peter Collingbourne	2012-05-02
\| \| \| \| \| \|	Specifically, if the directory separator character is '/' and an unrecognised command line parameter begins with '/', treat it as a file path rather than an option.
*	Get Boogie and GPUVerify to compile and run with Mono	Peter Collingbourne	2012-05-02
\|
*	added counterexample generation based on labels back to stratified inlining	qadeer	2012-05-01
\|
*	UseLabels=false when stratified inline is on	qadeer	2012-04-29
\|
*	removed proccopybounding code	qadeer	2012-04-28
\| \| \| \|	stratified inliinig is now run always with /doNotUseLabels
*	removed lazy inlining	qadeer	2012-04-28
\|
*	unsat core for houdini	qadeer	2012-04-27
\|
*	Added functionality to "skip" procedures. Some cleanup.	akashlal	2012-04-12
\|
*	Fixed bug with triply nested maps and polymorphism (reported as Item # 10218).	Unknown	2012-04-04
\|
*	added nonUniformUnfolding option	qadeer	2012-04-03
\|
*	deleted the option UseUnsatCoreForInlining	qadeer	2012-04-02
\| \| \| \| \|	Split ApiChecker.CheckAssumptions into two different methods, one which computes the unsatCore and one which does not Further edits to the MaxSat code
*	Emit of invariants now prints out the invariant attributes also	qadeer	2012-03-26
\|
*	added attributes to loop invariants	qadeer	2012-03-23
\|
*	more type checking for datatypes	qadeer	2012-03-18
\|
*	Boogie: Simplified (and liberalized) parsing of string literals as attribute ↵	Unknown	2012-03-12
\| \| \| \|	parameters
*	updated Boogie strings so that they can refer to \" (and more)	qadeer	2012-03-12
\| \| \| \|	fixed BCT :value
*	make the call to ProcessDataTypeConstructors in the right place	qadeer	2012-03-11
\|
*	Boogie: map the given filename stdin.bpl to standard input	Unknown	2012-03-09
\|
*	various refactorings related to houdini	qadeer	2012-03-02
\|
*	verbose mode for stratified inlining.	Unknown	2012-02-29
\|
*	bug fixes related to using ControlFlowFunction instead of labels	qadeer	2012-02-23
\|
*	using model instead of labels	Unknown	2012-02-23
\|
*	verbose mode	akashlal	2012-02-19
\|
*	Use DateTime.UtcNow instead of DateTime.Now	stobies	2012-01-11
\| \| \| \|	see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx
*	Boogie: output number of proof obligations (asserts) along with timing ↵	Rustan Leino	2012-01-09
\| \| \| \|	information when using the /trace option
*	made delegate a datatype	qadeer	2011-12-30
\| \| \| \|	added a DatatypeConstructor class
*	fixed problems with datatypes	qadeer	2011-12-29
\| \| \| \| \|	removed stale contracts in stratified inlining added test to datatypes
*	fixed a completeness problem in houdini with inlining	qadeer	2011-12-18
\|
*	Fixed the Boogie build.	wuestholz	2011-12-16
\|
*	Dafny: Made sure that error locations refer to the Dafny program, even if ↵	wuestholz	2011-12-15
\| \| \| \|	the /print option is used.
*	Boogie: Changed Expr.Not to keep swap arguments rather change direction of ↵	Rustan Leino	2011-12-12
\| \| \| \|	operator when negating <, <=, >=, or >
*	Merge	Rustan Leino	2011-12-07
\|\
\| *	Merge	Michal Moskal	2011-12-07
\| \|\
\| * \|	Fix atg file and add comment about Set/Variable/	Michal Moskal	2011-12-07
\| \| \|
\| * \|	Make set iteration order deterministic	Michal Moskal	2011-12-07
\| \| \| \| \| \| \| \| \| \| \| \|	Make the set class generic
* \| \|	Merge	Rustan Leino	2011-12-05
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	Boogie: Added new abstract interpretation harness, which uses native Boogie ↵	Rustan Leino	2011-12-05
\| \|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \|	Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred}
\| *	Emit attribute on a requires	akashlal	2011-12-04
\|/
*	Added option of turning off model generation in SI. Can be very expensive ↵	akashlal	2011-11-26
\| \| \| \|	sometimes.
*	fixed bug in the inlineDepth option for houdini	qadeer	2011-11-23
\| \| \| \|	small clean up in the inlining implementation
*	Merge	qadeer	2011-11-22
\|\
\| *	Boogie: don't resolve ignored types (that is, "extern" types that have been ↵	Rustan Leino	2011-11-22
\| \| \| \| \| \| \| \|	thrown out)
* \|	added support for handling duplicate axioms	qadeer	2011-11-22
\|/
*	Added lazy summary computation to stratified inlining (not finished yet)	akashlal	2011-11-20
\|
*	commented calls to GC.Collect()	qadeer	2011-11-18
\|
*	changed the semantics of requires and ensures for inlined procedures	qadeer	2011-11-17
\|
*	Boogie: fixed build error (incorrect type in Contract.Result)	Rustan Leino	2011-11-16
\|
*	Merge	akashlal	2011-11-16
\|\
\| *	Debugging output for stratified inlining. Emit attribute on Ensures while	Unknown	2011-11-16
\| \| \| \| \| \| \| \|	printing it.
* \|	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.