summaryrefslogtreecommitdiff
path: root/Source/ModelViewer/DafnyProvider.cs
Commit message (Collapse)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
* Changed BVD to display shortened names if they are unique.Gravatar wuestholz2013-08-05
|
* Make it possible to look up variables in the Dafny error models.Gravatar wuestholz2013-07-30
|
* Fixed issue in the model viewer.Gravatar wuestholz2013-07-29
|
* Dafny/Boogie/BVD: made Dafny plug-in for BVD work againGravatar Rustan Leino2012-06-08
|
* BVD: fixed two basic but damning problems with the Dafny provider, and ↵Gravatar Rustan Leino2011-10-26
| | | | elided some temporary variables
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
|
* BVD Dafny: support Skolem constantsGravatar rustanleino2011-02-02
|
* Allow the provider to skip some states when generating SourceLocationsGravatar MichalMoskal2011-01-26
|
* Introduce new NamedState base class to reduce code duplicationGravatar MichalMoskal2011-01-26
|
* Right-clicking on a state allows to display the source code for itGravatar MichalMoskal2011-01-26
|
* More user-friendly canonical namesGravatar MichalMoskal2011-01-17
|
* Make the filename length limit be 30 (as in VCC)Gravatar MichalMoskal2011-01-14
|
* Rework the namer interface a bitGravatar MichalMoskal2010-12-10
|
* Introduce node categories; sort fields based on that not special charactersGravatar MichalMoskal2010-12-01
|
* Dafny: Improved default decreases clauses for methods and functionsGravatar rustanleino2010-11-25
| | | | | Dafny: Don't display "alloc" field in BVD Chalice: Fixed error-message parsing error in VS mode
* BVD for Dafny: improved string that displays array indicesGravatar rustanleino2010-11-17
|
* BVD Dafny provider: treat sets and datatype valuesGravatar rustanleino2010-11-17
|
* Implement different levels of view (normal, expert, etc).Gravatar MichalMoskal2010-11-09
| | | | Display functions and pointer sets in VCC
* Simplify languague-specific interfaceGravatar MichalMoskal2010-11-06
|
* Refactor the Namer into two classesGravatar MichalMoskal2010-11-04
|
* Rework canonical name computationGravatar MichalMoskal2010-11-03
| | | | Sort fields inteligently (allow for override as well)
* Dafny model viewer: handle (single- and multi-dimensional) arraysGravatar rustanleino2010-11-03
|
* ModelViewer:Gravatar rustanleino2010-11-02
| | | | | | | * map back values introduced by bool_2_U and int_2_U * map back internal names for select/store to [n] and [n:=], where n is the arity of the map * added /break switch to ModelViewer * display more things (including sequences) in Dafny provider
* Dafny: a partial first crack at a Dafny model-viewer provider, including ↵Gravatar rustanleino2010-11-01
captureState mark-ups in the Boogie code generated from Dafny