diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-10-26 11:14:25 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-10-26 11:14:25 -0700 |
| commit | cfbfbb0229db8f71c4fb21c0f4c7cfb60debd507 (patch) | |
| tree | 931d29317eacd6eafc20ca006ddd38f9595a9435 /Source/ModelViewer | |
| parent | 321ceeee73433b2a772cd3435cb2ffaa346fb113 (diff) | |
VCC: Detect wrong model files
Diffstat (limited to 'Source/ModelViewer')
| -rw-r--r-- | Source/ModelViewer/VccProvider.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index b5ba6c22..ede520cb 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -135,7 +135,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc sn.SetupVars();
states.Add(sn);
}
+
var allStates = states.ToArray();
+ if (allStates.Length == 1 && allStates[0].vars.Count == 0) {
+ throw new Exception("This VCC model doesn't contain any variables. Was it saved with the -bvd option?");
+ }
states.Clear();
var i = 0;
while (i < allStates.Length) {
|