| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | 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 |
| | | |||
| * | Chalice: bug -- permissions were implicity converted to Booge expressions ↵ | kyessenov | 2010-07-22 |
| | | | | | (due to "implicit def") | ||
| * | Chalice: bug -- expression substitution should preserve typing | kyessenov | 2010-07-22 |
| | | |||
| * | Chalice: sequence access wildcards a[*].* and a[*].f have been implemented ↵ | kyessenov | 2010-07-22 |
| | | | | | (sans checking for epsilon going beyond infinity and rd(...,*) permissions) | ||
| * | Chalice: introduced proper AST nodes for permission expressions and ↵ | kyessenov | 2010-07-21 |
| | | | | | permissions. This gets of redundancy in treating acc and rd in many places and should hopefully make permissions code more comprehensible | ||
| * | Boogie: Fixing incorrect referencing of Microsoft.Contracts (the Code ↵ | tabarbe | 2010-07-21 |
| | | | | | Contracts dll) in AbsInt, Isabelle, and Z3 | ||
| * | Boogie: Forgot this file when I checked in the port of Z3. (cce = Code ↵ | tabarbe | 2010-07-21 |
| | | | | | Contracts Extensions - utility methods for the port that are not present in Code Contracts.) | ||
| * | Boogie build failed | codeplexbot | 2010-07-21 |
| | | |||
| * | Chalice: fixed typos in strings; trying out committing with TFS | kyessenov | 2010-07-21 |
| | | |||
| * | Boogie: The reference to Z3 was dropped during the commit. Here it is back. | tabarbe | 2010-07-20 |
| | | |||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |