debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
\| *	Chalice: New command line parameter /time:<n> that allows to output timing ↵	stefanheule	2012-09-11
\| \| \| \| \| \| \| \|	information (with varying verbosity). By default, the overall verification time is output.
* \|	Dafny: did a little to extend the support of labeled statements in ↵	Unknown	2012-09-10
\| \| \| \| \| \| \| \|	refinements (things like multiple labels are still not thought through very well)
* \|	Dafny: improved checking of inherited postconditions (in refinements)	Unknown	2012-09-10
\| \|
* \|	Boogie: added /tracePOs option for printing out number of proof obligations ↵	Unknown	2012-09-10
\| \| \| \| \| \| \| \|	without also printing out the verification times
\| *	Chalice: implemented automatic trigger-finding for quantifiers in ↵	Unknown	2012-09-11
\| \| \| \| \| \| \| \|	user-supplied specifications (searching for sets of matching function terms, and taking their "limited" forms).
* \|	Merge	Rustan Leino	2012-09-10
\|\ \
* \| \|	ignore Chalice/bin	Rustan Leino	2012-09-10
\| \| \|
* \| \|	Merge	Rustan Leino	2012-09-10
\|\ \ \
\| * \| \|	Find implementations of interface methods for dynamic dispatch, not just	Unknown	2012-09-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	overrides of virtual methods.
* \| \| \|	DafnyExtension: addressed a class initialization order problem	Rustan Leino	2012-09-09
\| \| \| \|
* \| \| \|	Dafny: allow 'decreases *' (that is, non-terminating recursion) on ↵	Rustan Leino	2012-09-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	tail-recursive methods
\| * \| \|	Avoid creating a dynamic dispatch table for GetHashCode and ToString: it ends	Unknown	2012-09-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	up creating code that the Boogie parser gets a stack overflow while trying to parse!
\| * \| \|	Moved the statement traverser's operand stack (used for explicit push/pop/dup	Unknown	2012-09-09
\|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	in the code model) into the sink so that the different statement traversers used for things like if-then-else statements share the same stack. Fixed a problem in the dispatch table for whole program virtual dispatch so it works for generic methods. Found input that either crashed the translator or caused it to produce bad Boogie: "fixed" it by having the translator thrown an exception so the method containing the bad code is skipped.
\| \| *	Chalice: added findFunctionAppsContaining(..) to Expression, which finds all ↵	Unknown	2012-09-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the function applications with at least one variable in common with a given list. This is a pre-cursor to writing a trigger-generating routine for quantifiers. Also corrected some copy-paste comments in Translator.scala
\| \| *	Chalice: implemented the final cases of the "inside" feature for predicates. ↵	Unknown	2012-09-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	At the same time, exhaling an unfolding expression now generates corresponding secondary permission information (this can in principle be useful; with fractional permissions it need not be the case that just because we exhale (part of) a predicate, we don't have any left. Also added a test case to test the new non-aliasing knowledge the "inside" encoding provides in various situations.
* \| \|	Merge	Unknown	2012-09-07
\|\ \ \
* \| \| \|	Dafny: Added detection and support for tail recursive calls (and an ↵	Unknown	2012-09-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	optional "tailrecursion" attribute). Also, let the cloner also clone attributes.
* \| \| \|	DafnyExtension: new color (violet) for buffer snapshot sent to the verifier	Unknown	2012-09-07
\| \| \| \|
\| * \| \|	Implement support for alternative SMT solvers -- CVC3 and CVC4	Peter Collingbourne	2012-09-06
\| \| \| \|
\| * \| \|	Dafny: Fixed a test that would fail with Z3 4.1.	wuestholz	2012-09-07
\| \| \| \|
\| \| \| *	Chalice: implemented "inside" information for all cases which translate to ↵	Unknown	2012-09-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	statements. So far this does not include exhaling an unfolding expression, or translation of an unfolding expression in e.g., program code (which looks more challenging). Note that secondary permissions do not appear to be generated in these cases either, which may be problematic for certain pathological examples.
\| \| \| *	Chalice: added "inside" knowledge of predicate instance nesting to unfold ↵	Unknown	2012-09-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	statements (previously only fold was implemented), and to the translation of unfolding expressions in some cases.
\| \| \| *	Chalice: first part of implementation of tracking which predicate instances ↵	Unknown	2012-09-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	occur inside which (for extra non-aliasing information)
* \| \| \|	Merge	Unknown	2012-09-05
\|\\| \| \|
* \| \| \|	Dafny: fixed typo in latex mode	Unknown	2012-09-05
\| \| \| \|
\| \| \| *	Chalice: Merge	Unknown	2012-09-05
\| \| \| \|\
\| \| \| * \|	Chalice: support for static functions. Functions declared "static" are ↵	Unknown	2012-09-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	axiomatised without a receiver. However, calls of such functions still syntactically require a receiver for now (which is ignored).
\| \| \| \| *	Chalice: Remove accidental changes to chalice.bat.	stefanheule	2012-09-05
\| \| \| \|/
\| \| \| *	Chalice: adopted triggering/axioms used for "recursive" functions for all ↵	Unknown	2012-09-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	functions (so that the various tricks get applied uniformly, even when Chalice thinks a function is not recursive).
\| \| \| *	Chalice: reapplied changes from changeset	Unknown	2012-09-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	2648 (ff8bdaa099cd) Chalice: Allow unfolding expressions in predicates (this fixes workitem 10223).
\| \| \| *	reapplied changes from changeset:	Unknown	2012-09-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	2891 (c73229bf100d) Experimental version with weaker triggering for function definition axiom (should trigger whenever both the function application has occurred somewhere in the code, and a corresponding predicate has been either folded or unfolded).
\| \| \| *	Chalice: added list segment example	Unknown	2012-09-03
\| \| \| \|
\| \| \| *	Chalice: reremoved implementation of (unuses) UpdateSecMask, as was ↵	Unknown	2012-09-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	previously done in changeset 2678 (ca2a67918aa7)
\| \| \| *	Chalice: reapplied changes from changeset	Unknown	2012-09-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	2669 (bc94e6c85481) Chalice: Remove IsGoodState as it is not needed and causes problems in certain cases.
\| \| \| *	Reapplied changes from previous update	Unknown	2012-09-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	2568 (f1a12d812207) : Chalice: refactor ExhaleHelper to use a local lambda expression for easier parameter management.
\| \| \| *	Reverted Prelude.scala and Translator.scala to those from version 96adb1c351bd	Unknown	2012-09-03
\| \| \| \|
\| * \| \|	Moved point at which preprocessed output is shown.	Unknown	2012-08-31
\| \| \| \|
\| * \| \|	Shared state is now properly abstracted in requires clauses.	Unknown	2012-08-31
\| \| \| \|
* \| \| \|	DafnyExtension: don't duplicate names of inherited identifiers	Unknown	2012-08-30
\| \| \| \|
* \| \| \|	Dafny: for refinements, don't consider a newly provided predicate body to be ↵	Unknown	2012-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be
* \| \| \|	DafnyExtension: changed how "_" is displayed (now display as a keyword, not ↵	Unknown	2012-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	as an identifier definition)
* \| \| \|	Dafny: allow "_" as don't-care variable name	Unknown	2012-08-30
\| \| \| \|
\| \| * \|	Dafny: allow more corecursive calls for copredicates	Rustan Leino	2012-08-30
\| \|/ / \|/\| \|
\| * \|	Merge	Unknown	2012-08-30
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	Barriers now handled uniformly via bugle_barrier.	Unknown	2012-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Improved loop invariant inference so that procedure formal parameters are treated as constants. (This involved fixing a bug where a Formal was being dualised to a LocalVariable.) Fixed problem in GPUVerifyBoogieDriver where source location information was being looked for via a file name, rather than a full path. Cleaned up some code in GPUVerifyBoogieDriver.
* \| \|	Dafny: fixed bug in checking postconditions of functions that mention the ↵	Unknown	2012-08-29
\| \| \| \| \| \| \| \| \| \| \| \|	result the function itself
* \| \|	DafnyExtension: fixed bug (omitted case: VarDeclStmt has no Update component)	Unknown	2012-08-29
\| \| \|
* \| \|	Dafny: fixed contract violation in parser (for non-parsing Lhs production)	Unknown	2012-08-29
\|/ /
* \|	A small fix in variable definition analysis.	Unknown	2012-08-29
\| \|
* \|	Added generation of invariants to restrict source location to sensible values.	Egor Kyshtymov	2012-08-28
\| \| \| \| \| \| \| \| \| \|	Refactored Make...Variable() and FindOrCreate...Variable() functions to take a variable name as a parameter rather than the variable itself.