debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	integrating predication	qadeer	2012-06-19
\|
*	Move block predicator to VCGeneration	Peter Collingbourne	2012-06-18
\|
*	GPUVerify: implement is-a-constant analysis	Peter Collingbourne	2012-06-15
\| \| \| \| \| \| \| \| \| \| \| \| \|	This analysis is used to generate race checking invariants for arbitrary (thread-level) constant offsets, in place of invariant generators for four specific constants (thread-id, global-id, 2D thread-id and 2D global-id) which are subsumed by the new analysis. The main motivation is to be able to recognise offsets used by word level accesses into byte arrays, which are formed from linear combinations of thread IDs and constants. This change allows us to remove the 2D and global size analyses, resulting in a 536-line net reduction in total code size.
*	Merging again	Ken McMillan	2012-06-07
\|\
\| *	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).
* \| \|	Boogie: add /printCFG command line option, which prints each ↵	Peter Collingbourne	2012-06-06
\|/ / \| \| \| \| \| \|	implementation's CFG in Graphviz format
* \|	moved class Macro to Absy	qadeer	2012-06-04
\| \| \| \| \| \| \| \| \| \|	cleanup up DefineMacro Changed SI to use macros for reach info
* \|	Merge	qadeer	2012-06-01
\|\ \
* \| \|	changed behavior of InlinedEnsures so that free ensures is skipped unless an ↵	qadeer	2012-06-01
\| \| \| \| \| \| \| \| \| \| \| \|	attribute called :assume is there
\| * \|	1. Fix for free ensures in inlined procedures. Becomes a skip instead of an ↵	Unknown	2012-06-01
\|/ / \| \| \| \| \| \| \| \| \| \| \| \|	assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change.
* \|	No need for extra attributes in ExtractLoops	akashlal	2012-05-28
\| \|
* \|	Better interface for adding skipped calls, and	akashlal	2012-05-26
\| \| \| \| \| \| \| \|	adding extra recursion bound to some procedures.
* \|	Merge	Unknown	2012-05-25
\|\ \
* \| \|	Adding an option for deterministicExtractLoops, that uses an alternate way ↵	Unknown	2012-05-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	to extract loops into procedures. Unsound for concurrency. Added a test in extractLoops directory.
\| * \|	Merge	qadeer	2012-05-24
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	more refactoring in stratified inlining	qadeer	2012-05-24
\| \| \|
* \| \|	Boogie: document /typeEncoding:m	Peter Collingbourne	2012-05-22
\|/ /
* \|	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
\|\