| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
caused malformed Boogie and malformed VCs. In particular, the problem arose in the CEV $file_name_is declarations. Such characters are now replaced by a percent sign followed by a four-digit hexadecimal number representing the Unicode value of the character.
This fixes issue #6057.
|
| |
|
|
|
| |
* SscBoogie: changed default setting for /modifiesOnLoop
(we really should move this SscBoogie-specific code to the Spec# codeplex)
|
| |
|
|
|
| |
Dafny: Make use of function preconditions in function well-definedness checks.
Chalice: Changed old "install" to current "reorder" keyword in Emacs mode.
|
| |
|
|
|
|
|
|
| |
* Added DeclType(f)==C axioms, which for each field f says which class declares it.
Boogie:
* Changed behavior of free loop invariants. Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures. The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior.
* NOTE: I did NOT yet make the corresponding change for loop unrolling, but it is needed.
|
| | |
|
| | |
|
| |
|
|
| |
Boogie.
|
| |
|
|
| |
are run.
|
| | |
|
| |
|
RMonahan