summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
* Boogie build failedGravatar codeplexbot2010-07-29
|
* Changed reference to AbsInt from a dll reference to a project reference.Gravatar mikebarnett2010-07-28
|
* Dafny: DafnyDriver port part 3/3: Updating sources to reference new project.Gravatar tabarbe2010-07-28
|
* Dafny: DafnyDriver port part 2/3: Adding new dependent file, removing ↵Gravatar tabarbe2010-07-28
| | | | unnecessary one.
* Dafny: DafnyDriver port part 1/3: Replacing old source files with ported versionGravatar tabarbe2010-07-28
|
* Dafny/DafnyDriver: Renaming source files in preparation for port commitGravatar tabarbe2010-07-28
|
* Boogie: VCGeneration port part 3/3: Updating sources to reference new ↵Gravatar tabarbe2010-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 ↵Gravatar tabarbe2010-07-28
| | | | unnecessary one.
* Boogie: VCGeneration port part 1/3: Replacing old source files with ported ↵Gravatar tabarbe2010-07-28
| | | | version
* Boogie\VCGeneration: Renaming sources in preparation for my addition of the ↵Gravatar tabarbe2010-07-28
| | | | ported C# version
* Fixed reference to VCGeneration project. Mistakenly checked in project files ↵Gravatar mikebarnett2010-07-28
| | | | were pointing to the yet-to-exist C# version.
* Boogie build failedGravatar codeplexbot2010-07-28
|
* Boogie: Changed references from binary to project references.Gravatar tabarbe2010-07-27
|
* Boogie Provers: Changed the references from binary to project references.Gravatar tabarbe2010-07-27
|
* Chalice: pretty printer now prints element type for sequences; fixed a bug ↵Gravatar kyessenov2010-07-27
| | | | in copying resolved member in sequence accesses; added graph closure (DSW) verification example
* Boogie build failedGravatar codeplexbot2010-07-24
|
* Also traverse bodies of function definitions when performing lambda expansion.Gravatar sboehme2010-07-23
|
* Boogie: AssemblyInfo.cs is no longer required for the build; cce.cs is.Gravatar tabarbe2010-07-23
|
* Boogie: Committing my port of simplify, along with the slightly changed ↵Gravatar tabarbe2010-07-23
| | | | references of simplify's dependents.
* Boogie: Renaming Simplify.sscproj and source files in preparation for ↵Gravatar tabarbe2010-07-23
| | | | committing my port of Simplify.csproj.
* Boogie build succeededGravatar codeplexbot2010-07-23
|
* Boogie: One last file to add for the port commit. Also, AssemblyInfo.ssc is ↵Gravatar tabarbe2010-07-22
| | | | no longer necessarry.
* Boogie: Committing my port of the SMTLib projectGravatar tabarbe2010-07-22
|
* Boogie: Renaming the source files for the SMTLib project in preparation for ↵Gravatar tabarbe2010-07-22
| | | | commiting my port of the project.
* Boogie: This file is no longer necessary, with how the csproj file is ↵Gravatar tabarbe2010-07-22
| | | | structured.
* Boogie: Repaired a reentrancy error in Z3/Simplify.Gravatar tabarbe2010-07-22
|
* Boogie build succeeded, 25 test(s) failedGravatar codeplexbot2010-07-22
|
* Boogie: Looks like the default namespace should be Microsoft.Boogie.Z3, ↵Gravatar tabarbe2010-07-22
| | | | rather than Provers.Z3. I updated that.
* Boogie: Changed the assembly name for the Z3 project to Provers.Z3.dll, so ↵Gravatar tabarbe2010-07-22
| | | | that it matches the namespace.
* Boogie build succeeded, 25 test(s) failedGravatar codeplexbot2010-07-22
|
* Chalice: bug -- permissions were implicity converted to Booge expressions ↵Gravatar kyessenov2010-07-22
| | | | (due to "implicit def")
* Chalice: bug -- expression substitution should preserve typingGravatar kyessenov2010-07-22
|
* Chalice: sequence access wildcards a[*].* and a[*].f have been implemented ↵Gravatar kyessenov2010-07-22
| | | | (sans checking for epsilon going beyond infinity and rd(...,*) permissions)
* Chalice: introduced proper AST nodes for permission expressions and ↵Gravatar kyessenov2010-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 ↵Gravatar tabarbe2010-07-21
| | | | Contracts dll) in AbsInt, Isabelle, and Z3
* Boogie: Forgot this file when I checked in the port of Z3. (cce = Code ↵Gravatar tabarbe2010-07-21
| | | | Contracts Extensions - utility methods for the port that are not present in Code Contracts.)
* Boogie build failedGravatar codeplexbot2010-07-21
|
* Chalice: fixed typos in strings; trying out committing with TFSGravatar kyessenov2010-07-21
|
* Boogie: The reference to Z3 was dropped during the commit. Here it is back.Gravatar tabarbe2010-07-20
|
* Boogie: Committing ported version of Z3.Gravatar tabarbe2010-07-20
|
* Chalice: added surface syntax for acc(s[*].*) and acc(s[*].f); extended AST, ↵Gravatar kyessenov2010-07-20
| | | | resolver, printer; translation is not yet done
* Boogie: Typo with the renaming. FixedGravatar tabarbe2010-07-20
|
* Boogie: Let's try that rename again, shall we?Gravatar tabarbe2010-07-20
|
* Boogie: Rename didn't work. Resetting to try againGravatar tabarbe2010-07-20
|
* Boogie/Z3: Renaming the sources for Z3 in preparation for commit of my port ↵Gravatar tabarbe2010-07-20
| | | | of the project.
* Chalice: fixed a bug with permission operations treating AccessAll not as a ↵Gravatar kyessenov2010-07-20
| | | | permission expression; refactored Translator my moving prelude/implicits into TranslatorHelper for consistency
* Boogie build succeededGravatar codeplexbot2010-07-20
|
* Chalice: added type information for sequences ("where" clauses in local ↵Gravatar kyessenov2010-07-20
| | | | variable declarations and method/function formals); the clause says that every element in a sequence is either null or its dtype is the element type
* Chalice: adding support for sequence local variables; removed ClassType from ↵Gravatar kyessenov2010-07-20
| | | | Boogie since it was maskng bad job done by Translator; fixing warnings in case we ever decide to switch to newer Scala compiler
* Boogie/Isabelle: implemented missing translation of if-then-else expressionsGravatar sboehme2010-07-20
|
generated by cgit v1.2.3 (git 2.39.1) at 2025-03-08 14:29:19 +0000