debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Chalice: abstract Shorr-Waite algorithm verified	kyessenov	2010-08-03
\|
*	Chalice: deriving SchorrWaite algorithm with Chalice	kyessenov	2010-08-03
\|
*	Defunct project.	mikebarnett	2010-08-03
\|
*	Chalice: added Tarjan's SCC algorithm for computing function call graph and ↵	kyessenov	2010-08-03
\| \| \| \|	recursion bits
*	fixed path to the binaries directory; there was an extra .."	qadeer	2010-08-03
\|
*	Chalice:	kyessenov	2010-08-02
\| \| \| \| \| \| \|	* change syntax for range: [a..b] instead of [a:b] * add multi-triggers to Boogie bindings * fix unsoundness in frame axiom for functions -- whenever acc(s[].f,...) is detected in pre-condition, a different encoding to Boogie is applied add limited functions to translator (disabled since Resolver is not ready yet)
*	Boogie: Added a new code snippet for IEnumerable out parameters	tabarbe	2010-08-02
\|
*	Code Snippets: Corrected an annoyance in one of the snippets	tabarbe	2010-08-02
\|
*	Chalice:	kyessenov	2010-08-02
\| \| \| \| \| \|	* added quantifiers over any type (forall i: int :: i + 1 == i + 1) * cleaned up AST transformation code; organized one transform operation that should preserve source positions -- it was very annoying to see assertions with lost source positions * added a desugar method that simplifies Chalice AST by unrolling a few constructs -- maybe useful in the future to quickly add a syntactic sugar
*	Boogie build succeeded	codeplexbot	2010-07-31
\|
*	Boogie: The deletion of those files did not hold, lemme try again.	tabarbe	2010-07-30
\|
*	Boogie: Changed BoogieDriver.cs to use a copy of cce.cs, rather than an ↵	tabarbe	2010-07-30
\| \| \| \|	internal cce.cs class.
*	Boogie: Removed cce.cs's from the provers, because they all reference ↵	tabarbe	2010-07-30
\| \| \| \|	projects which have a (more up-to-date) copy of cce.cs.
*	Chalice:	kyessenov	2010-07-30
\| \| \| \| \| \| \|	* add sequence axiom updates from Dafny * fix a bug in pretty printer for functions and predicates * add a command line option for not checking termination; refactor options code to update syntax help string * relax resolver to allow ghost state in assume statements (we don't know how to compile them in general anyways; assume false is still a special case and is compiled into assert false)
*	Also build Boogie and Dafny projects in 32-bit configurations.	rustanleino	2010-07-30
\| \| \| \|	Don't insist on DafnyDriver picking up the LKG version (1.0.21125.0) of the Spec# runtime (in fact, most builders will probably have 1.0.21126.0).
*	Boogie/Dafny: For those who may have not used custom code snippets before, ↵	tabarbe	2010-07-30
\| \| \| \|	some instructions on getting VS to track them down, along with an Excel sheet detailing the ones available.
*	Sign both of the Dafny projects and have Dafny.exe get a version number as well.	mikebarnett	2010-07-30
\|
*	Boogie/Dafny: Boogie and Dafny's conversion to C# and Code Contracts does ↵	tabarbe	2010-07-30
\| \| \| \|	not need to mean that adding functionality will take longer than it had before, now that the handy Spec# non-null typesystem and verification keywords no longer are used. Here are some handy Code Snippets which can be implemented in Visual Studio in order to make adding to the Boogie codebase rapid.
*	Made consistent the way all of the C# projects sign themselves and include ↵	mikebarnett	2010-07-30
\| \| \| \|	the version information.
*	Boogie: Added a new simple regression test, "sanity", which runs a single ↵	tabarbe	2010-07-29
\| \| \| \|	test for Boogie and a single test for Dafny, just to check for grievous runtime errors in the code. (In my porting, I work with code that, in some cases, is not tested until the 3rd or 4th regression test. These 2 test files should make use of that more obscure code and alert me to my errors quickly, rather than making me wait through a full regression cycle.)
*	Boogie build failed	codeplexbot	2010-07-29
\|
*	Changed reference to AbsInt from a dll reference to a project reference.	mikebarnett	2010-07-28
\|
*	Dafny: DafnyDriver port part 3/3: Updating sources to reference new project.	tabarbe	2010-07-28
\|
*	Dafny: DafnyDriver port part 2/3: Adding new dependent file, removing ↵	tabarbe	2010-07-28
\| \| \| \|	unnecessary one.
*	Dafny: DafnyDriver port part 1/3: Replacing old source files with ported version	tabarbe	2010-07-28
\|
*	Dafny/DafnyDriver: Renaming source files in preparation for port commit	tabarbe	2010-07-28
\|
*	Boogie: VCGeneration port part 3/3: Updating sources to reference new ↵	tabarbe	2010-07-28
\| \| \| \|	project; making Core work with the port by removing the nonnull requirements on one abstract method.
*	Boogie: VCGeneration port part 2/3: Adding new dependent files, removing ↵	tabarbe	2010-07-28
\| \| \| \|	unnecessary one.
*	Boogie: VCGeneration port part 1/3: Replacing old source files with ported ↵	tabarbe	2010-07-28
\| \| \| \|	version
*	Boogie\VCGeneration: Renaming sources in preparation for my addition of the ↵	tabarbe	2010-07-28
\| \| \| \|	ported C# version
*	Fixed reference to VCGeneration project. Mistakenly checked in project files ↵	mikebarnett	2010-07-28
\| \| \| \|	were pointing to the yet-to-exist C# version.
*	Boogie build failed	codeplexbot	2010-07-28
\|
*	Boogie: Changed references from binary to project references.	tabarbe	2010-07-27
\|
*	Boogie Provers: Changed the references from binary to project references.	tabarbe	2010-07-27
\|
*	Chalice: pretty printer now prints element type for sequences; fixed a bug ↵	kyessenov	2010-07-27
\| \| \| \|	in copying resolved member in sequence accesses; added graph closure (DSW) verification example
*	Boogie build failed	codeplexbot	2010-07-24
\|
*	Also traverse bodies of function definitions when performing lambda expansion.	sboehme	2010-07-23
\|
*	Boogie: AssemblyInfo.cs is no longer required for the build; cce.cs is.	tabarbe	2010-07-23
\|
*	Boogie: Committing my port of simplify, along with the slightly changed ↵	tabarbe	2010-07-23
\| \| \| \|	references of simplify's dependents.
*	Boogie: Renaming Simplify.sscproj and source files in preparation for ↵	tabarbe	2010-07-23
\| \| \| \|	committing my port of Simplify.csproj.
*	Boogie build succeeded	codeplexbot	2010-07-23
\|
*	Boogie: One last file to add for the port commit. Also, AssemblyInfo.ssc is ↵	tabarbe	2010-07-22
\| \| \| \|	no longer necessarry.
*	Boogie: Committing my port of the SMTLib project	tabarbe	2010-07-22
\|
*	Boogie: Renaming the source files for the SMTLib project in preparation for ↵	tabarbe	2010-07-22
\| \| \| \|	commiting my port of the project.
*	Boogie: This file is no longer necessary, with how the csproj file is ↵	tabarbe	2010-07-22
\| \| \| \|	structured.
*	Boogie: Repaired a reentrancy error in Z3/Simplify.	tabarbe	2010-07-22
\|
*	Boogie build succeeded, 25 test(s) failed	codeplexbot	2010-07-22
\|
*	Boogie: Looks like the default namespace should be Microsoft.Boogie.Z3, ↵	tabarbe	2010-07-22
\| \| \| \|	rather than Provers.Z3. I updated that.
*	Boogie: Changed the assembly name for the Z3 project to Provers.Z3.dll, so ↵	tabarbe	2010-07-22
\| \| \| \|	that it matches the namespace.
*	Boogie build succeeded, 25 test(s) failed	codeplexbot	2010-07-22
\|