debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
*	Add a string for an uninterpreted value in errModel	Unknown	2011-06-06
\|
*	LetVC can get null label2absy from lazy inlining. So, I weakened the ↵	qadeer	2011-05-03
\| \| \| \|	precondition otherwise the checked build was failing
*	modified letvc generation so that the use of control flow function and ↵	qadeer	2011-04-15
\| \| \| \|	labels is decoupled. Former is controled by controlFlowVariable and the latter by label2Absy.
*	merge	Unknown	2011-04-14
\|\
* \|	added reachability information to the VC and used that to support arbitrary ↵	Unknown	2011-04-14
\| \| \| \| \| \| \| \|	asserts in lazy inlining
\| *	Stratified Inlining: minor bux fix with recording model values	Unknown	2011-04-14
\|/
*	Minor fixes	schaef	2011-03-27
\|
*	Boogie: fixed contract violation in stratified inlining	rustanleino	2011-03-23
\|
*	Print recorded value of any type	akashlal	2011-03-21
\|
*	Bug fix with model generation.	akashlal	2011-03-21
\|
*	minor fix with loopy counterexample generation	akashlal	2011-03-18
\|
*	Print out requested values in the counterexample trace	akashlal	2011-03-17
\|
*	Re-enabled quantifier checking in the Checked configuration.	mikebarnett	2011-03-16
\|
*	new algorithm for dead code detection (vc:doomed)	schaef	2011-03-15
\|
*	Turn off quantifier checking in the runtime checking.	mikebarnett	2011-03-14
\|
*	Replaced all dictionaries that mapped to bool (i.e., were being used to ↵	mikebarnett	2011-03-10
\| \| \| \|	implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
*	Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵	mikebarnett	2011-03-10
\| \| \| \| \| \|	dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
*	Updated PrepareBoogieZip.bat to include BVD and smt2	rustanleino	2011-03-10
\| \| \| \|	Ignore duplicated else functions in models
*	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.
*	Fix contracts so runtime checking can be turned on.	mikebarnett	2011-03-07
\|
*	Handle as-array[...] model elements	MichalMoskal	2011-02-23
\|
*	Parse else-> clauses in the model	MichalMoskal	2011-02-23
\| \| \| \|	Disable MODEL_PARTIAL in SMTLib
*	Throw exceptions when push/pop interface is used but not implemented	MichalMoskal	2011-02-23
\| \| \| \|	Complete ErrorModel tables with the final bogus else clause
*	Implement Push/Pop interface.	MichalMoskal	2011-02-23
\| \| \| \|	Implement ProverContext.Lookup method.
*	Move model printing to ErrorModel class	MichalMoskal	2011-02-21
\| \| \| \|	Allow construction of ErrorModel instance from Model instance
*	Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3	MichalMoskal	2011-02-18
\|
*	Kill {:prover "..."} attribute support; no one ever used this stuff	MichalMoskal	2011-02-17
\|
*	Stratified inlining: Added concrete values to error traces. Added an extra ↵	akashlal	2011-02-17
\| \| \| \|	flag "inferLeastForUnsat".
*	Fix with timeout	akashlal	2011-02-12
\|
*	Better support for timeout	akashlal	2011-02-12
\|
*	Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP ↵	MichalMoskal	2011-02-11
\| \| \| \|	provers. Add handling of help message about /proverOpt.
*	Minor change to stratified inlining	akashlal	2011-02-11
\|
*	Added a new method StratifiedVC for refinement.	akashlal	2011-02-08
\| \| \| \|	Added a method to copy a FunctionCall.
*	implemented /UseUnsatCoreForInlining option for use in stratified inlining	qadeer	2011-02-06
\|
*	deleted debugging statement	akashlal	2011-02-05
\|
*	Fix to counterexample generation for over-approx query	akashlal	2011-02-05
\|
*	Don't treat "Inconclusive" answer as fatal when splitting.	MichalMoskal	2011-02-02
\|
*	stratified inlining: minor fix to the call tree being saved	akashlal	2010-12-21
\|
*	stratified inlining: record the name of the main procedure.	akashlal	2010-12-18
\|
*	Add new feature: {:selective_checking} on procedures. See testcase for a ↵	MichalMoskal	2010-12-17
\| \| \| \|	description (it was implemented in VCC before and is quite useful).
*	Add functions generated in lambda-expansion of function body to top-level ↵	MichalMoskal	2010-12-17
\| \| \| \|	program declarations.
*	stratified inlining: minor changes to coverage reporter	akashlal	2010-12-13
\|
*	Boogie: Did some minor refactoring.	wuestholz	2010-12-10
\|
*	stratified inlining: added option of turning off CheckAssumptions	akashlal	2010-12-07
\|
*	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
*	Factored out the ParserHelper class into a separate project and updated the ↵	wuestholz	2010-12-02
\| \| \| \| \| \|	files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
*	Construct @MV_state function only once so it doesn't get renamed to ↵	MichalMoskal	2010-12-02
\| \| \| \|	@MV_state@@0 when we have more than one procedure to verify
*	stratified inlining: small fix	akashlal	2010-12-01
\|
*	stratified inlining: reuse call tree across queries	akashlal	2010-12-01
\|