Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Bring SourceView to front when double-clicking source line | stobies | 2011-12-08 |
| | |||
* | VCC: Fixes for recent prelude changes | Michal Moskal | 2011-12-02 |
| | |||
* | BVD: Fix display bug | Michal Moskal | 2011-11-15 |
| | |||
* | VCC: Further data type improvements | Michal Moskal | 2011-11-15 |
| | |||
* | VCC: Better display of data type values | Michal Moskal | 2011-11-15 |
| | |||
* | VCC: Recognize $result | Michal Moskal | 2011-11-15 |
| | |||
* | VCC: remove _vcc_math_type_ from type names | Michal Moskal | 2011-11-09 |
| | |||
* | VCC: hide #limited# functions | Michal Moskal | 2011-11-09 |
| | |||
* | BVD: don't do the "Duplicate entry exception"; uncomment for debugging | Michal Moskal | 2011-11-08 |
| | |||
* | VCC: show output parameters as roots | Michal Moskal | 2011-11-08 |
| | |||
* | Merge | Rustan Leino | 2011-10-26 |
|\ | |||
* | | BVD: fixed two basic but damning problems with the Dafny provider, and ↵ | Rustan Leino | 2011-10-26 |
| | | | | | | | | elided some temporary variables | ||
| * | VCC: Detect wrong model files | Michal Moskal | 2011-10-26 |
| | | |||
| * | VCC: improvements in showing arrays, addresses, and embeddings | Michal Moskal | 2011-10-24 |
|/ | |||
* | VCC: support some more _(blob ...) buisness | Michal Moskal | 2011-10-19 |
| | |||
* | BVD: Default to expert view; Only VCC uses that stuff now, and all VCC users ↵ | Michal Moskal | 2011-10-19 |
| | | | | are clearly experts | ||
* | Performance improvements in BVD | Michal Moskal | 2011-10-19 |
| | |||
* | VCC: Fix problem with booleans being displayed as maps | Michal Moskal | 2011-10-19 |
| | |||
* | Link Model.cs in ModelViewer, so that BVD can be updated independtly of the ↵ | Michal Moskal | 2011-10-03 |
| | | | | rest of Boogie | ||
* | VCC: Support _(blob ..) types; fix crash | Michal Moskal | 2011-09-28 |
| | |||
* | BVD/VCC: Handle reading records/data types from memory | Michal Moskal | 2011-09-23 |
| | |||
* | Better support for map types | Michal Moskal | 2011-09-23 |
| | |||
* | Handle datatypes and records | Michal Moskal | 2011-09-23 |
| | |||
* | Add handling of union active options | Michal Moskal | 2011-09-23 |
| | |||
* | Make sure items are visible when navigating the model with arrow keys | Michal Moskal | 2011-09-23 |
| | |||
* | Tree navigation with left/right arrow | Michal Moskal | 2011-09-20 |
| | |||
* | Formatting. | Michal Moskal | 2011-09-20 |
| | |||
* | Merge | Michal Moskal | 2011-08-16 |
|\ | |||
| * | various changes to boogie for bitvector analysis and bctprovider | qadeer | 2011-08-08 |
| | | |||
* | | Fix null-ref | Michal Moskal | 2011-08-07 |
| | | |||
| * | further updates to bctprovider | qadeer | 2011-08-05 |
| | | |||
| * | first add | qadeer | 2011-08-05 |
| | | |||
| * | fixed the key signing problem with houdini | qadeer | 2011-08-05 |
|/ | | | | started adding bct provider | ||
* | Add source file (Expression Design) for the BVD icon in case anyone ever ↵ | Michal Moskal | 2011-05-12 |
| | | | | needs it | ||
* | BVD: Smaller initial window (to better fit on a laptop screen) | Rustan Leino | 2011-04-22 |
| | |||
* | Add "Large font" menu item (for demos) | Michal Moskal | 2011-04-15 |
| | |||
* | Introduce states more aggressively. Show is_null() for pointers. | Michal Moskal | 2011-04-06 |
| | |||
* | Removing unused field (and testing mecurial checkins) | Stephan Tobies | 2011-04-05 |
| | |||
* | Improvements in map and skolem functions display. | MichalMoskal | 2011-04-02 |
| | |||
* | model viewer: | stobies | 2011-04-01 |
| | | | | Hide and disable file menu when run in hosted mode | ||
* | model viewer: | stobies | 2011-04-01 |
| | | | | | | Allow opening model file via dialog Added shortcut keys for the menu items Made ReloadModel public so that we can use is as an entry point for a VS tool window | ||
* | Model viewer: | stobies | 2011-04-01 |
| | | | | | Display message box for exception during execution Allow to pass options to Main window constructor | ||
* | Dafny: compile quantifiers | rustanleino | 2011-03-26 |
| | | | | | | Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges | ||
* | Re-enabled quantifier checking in the Checked configuration. | mikebarnett | 2011-03-16 |
| | |||
* | Turn off quantifier checking in the runtime checking. | mikebarnett | 2011-03-14 |
| | |||
* | Added a new solution configuration, Checked, that builds the Checked ↵ | mikebarnett | 2011-03-07 |
| | | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration. | ||
* | Add some ExpertLevel functions | MichalMoskal | 2011-02-21 |
| | |||
* | Dafny: removed CEV instrumentation | rustanleino | 2011-02-03 |
| | |||
* | BVD Dafny: support Skolem constants | rustanleino | 2011-02-02 |
| | |||
* | Improve display of sets; add \now "variable"; | MichalMoskal | 2011-01-29 |
| |