| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
Dafny: Don't display "alloc" field in BVD
Chalice: Fixed error-message parsing error in VS mode
|
| |
|
|
| |
Distinguish warnings/errors in Chalice.
|
| |
|
|
|
|
| |
constructs.
Dafny VS2010 extension: link with Dafny and use it to parse and type check
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
* Also copy CodeContractExtender in PrepareBoogieZip.bat
* Added some comments and a new program in Test/textbook
* Included refinement keywords in Chalice emacs mode
* Used assignment instead of spec statement in DuplicatesVideo.chalice
|
| |
|
|
|
| |
* extended the cheap type inference to also consider "in" expressions and quantifiers
* added some refinement keywords to the Emacs mode for Chalice
|
| | |
|
| |
|
|
|
|
| |
* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields
|
| | |
|
| | |
|
| |
|
|
| |
with string literals
|
| |
|
|
| |
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.
|
rustanleino