| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Cleans and builds both projects, then executes the regressions if the build succeeded. If the build had failed, it will stop the script.
|
| |
|
|
| |
positions were negative
|
| |
|
|
| |
be easily extensible.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
* 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)
|
| |
|
|
| |
some instructions on getting VS to track them down, along with an Excel sheet detailing the ones available.
|
| |
|
|
| |
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.
|
| |
|
|
|
|
| |
.dfy file; duh!)
Chalice tests: removed machine-specific path from test.bat (replacing the file reference with just 'scala', which in some ways is machine-specific too)
|
| |
|
|
|
|
|
| |
}'. Think of the new brackets as atomicity brackets (see PetersonsAlgorithm.chalice)
Chalice: Added Peterson's algorithm to test suite (safety properties only)
VS 2010 integration: Updated Chalice and Dafny modes, added keyword highlighting for a new Boogie mode
|
| |
|
|
| |
install binaries" link from the boogie.codeplex.com home page.
|
| | |
|
| |
|
|
| |
of the "held" field in the heap
|
| | |
|
| | |
|
| |
|
|
| |
implementations in the refinement VC
|
| |
|
|
|
| |
* changed rule about scoping of out-parameters
* added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
* renamed keyword "maxlock" to "waitlevel"
* added -vs switch, for I/O suitable for VS integration
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
|
| |
|
|
|
|
|
|
|
|
| |
* Added support for polymorphism in lambda expressions
* Little clean-up here and there
* Added 'then' keyword to emacs and latex modes
Dafny:
* Added support for fine-grained framing, using the back-tick syntax from Region Logic
* Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses
|
| |
|
|
|
| |
Previously, a "use" function was one whose definition was applied only in limited ways, namely when the function was uttered in a program (possibly in a "use" statement). Now, recursive functions are always limited, unless declared with the new modifier "unlimited". Non-recursive functions are always unlimited. Also new is that only function calls within the same SCC of the call graph use the limited form of the callee.
The "use" modifier is no longer supported. The "use" statement is still supported, now for both limited and unlimited functions; but it's probably better and easier to just explicitly mention a function in an assertion, if needed.
|
| |
|
|
|
|
|
|
| |
* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies)
* Added "print" statement (to make running compiled programs more interesting)
* Changed name of default class from $default to _default
Boogie:
* Included "lambda" as a keyword in emacs and latex style files
|
| |
|
|
|
| |
* Beginning of module implementation
* Changed "class" modifier (for functions and methods) to "static"
|
| | |
|
| | |
|
| |
|
|
| |
supports syntax-highlighting, auto-indentation and imenu.
|
| |
|
|
|
|
|
|
| |
boolean-only if-then-else expressions)
Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter)
Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::'
Dafny: Check for division-by-zero for both '/' and '%'
|
| |
|
|
|
|
|
| |
* Allow (and currently ignore) "ghost" modifier.
* Fixed bug in boxing.
* Check for div-by-zero error for modulo operator.
* Improved emacs and latex modes.
|
| |
|
|
| |
Included VSI-Benchmarks in standard tests.
|
| |
|
|
|
|
|
| |
"!(x in S)".
Changed Dafny test files to use the new operator.
Included the file b8.dfy into the VSI-Benchmarks test harness.
|
| |
|
|
|
| |
Dafny: Make use of function preconditions in function well-definedness checks.
Chalice: Changed old "install" to current "reorder" keyword in Emacs mode.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- channel declarations
- send and receive statements
- bounds clause for new, to accommodate channels
- Added ProdConsChannel.chalice test case
- Resolve and Translate (but no Compile yet)
- Added Credits to global state in encoding (this caused changes to lots of source lines)
* Simplified meaning of maxlock==E
* Various parser improvements
* Added alternative syntax for eval statements
* Some renamings in error messages (e.g., install -> reorder)
* Added preliminary parsing for condition variables and their wait and signal operations
* Added new keywords to Chalice emacs mode
|
| |
|
tabarbe