Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dafny crashes when you comment out lots of code #4261

Closed
seanmcl opened this issue Jul 6, 2023 · 0 comments · Fixed by #4424
Closed

Dafny crashes when you comment out lots of code #4261

seanmcl opened this issue Jul 6, 2023 · 0 comments · Fixed by #4424
Assignees
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: parser First phase of Dafny's pipeline

Comments

@seanmcl
Copy link
Collaborator

seanmcl commented Jul 6, 2023

Dafny version

4.1.0

Code to produce this issue

When I'm working on proofs I sometimes comment out code to focus on a particular method.

module M {
  // 0
  // 1
  // 2
  // 3
  // 4
  // 5
  // 6
  // 7
  // 8
  // 9
  // 10
  // 11
  // 12
  // 13
  // 14
  // 15
  // 16
  // 17
  // 18
  // 19
  // 20
  // 21
  // 22
  // 23
  // 24
  // 25
  // 26
  // 27
  // 28
  // 29
  // 30
  // 31
  // 32
  // 33
  // 34
  // 35
  // 36
  // 37
  // 38
  // 39
  // 40
  // 41
  // 42
  // 43
  // 44
  // 45
  // 46
  // 47
  // 48
  // 49
  // 50
  // 51
  // 52
  // 53
  // 54
  // 55
  // 56
  // 57
  // 58
  // 59
  // 60
  // 61
  // 62
  // 63
  // 64
  // 65
  // 66
  // 67
  // 68
  // 69
  // 70
  // 71
  // 72
  // 73
  // 74
  // 75
  // 76
  // 77
  // 78
  // 79
  // 80
  // 81
  // 82
  // 83
  // 84
  // 85
  // 86
  // 87
  // 88
  // 89
  // 90
  // 91
  // 92
  // 93
  // 94
  // 95
  // 96
  // 97
  // 98
  // 99
  // 100
  // 101
  // 102
  // 103
  // 104
  // 105
  // 106
  // 107
  // 108
  // 109
  // 110
  // 111
  // 112
  // 113
  // 114
  // 115
  // 116
  // 117
  // 118
  // 119
  // 120
  // 121
  // 122
  // 123
  // 124
  // 125
  // 126
  // 127
  // 128
  // 129
  // 130
  // 131
  // 132
  // 133
  // 134
  // 135
  // 136
  // 137
  // 138
  // 139
  // 140
  // 141
  // 142
  // 143
  // 144
  // 145
  // 146
  // 147
  // 148
  // 149
  // 150
  // 151
  // 152
  // 153
  // 154
  // 155
  // 156
  // 157
  // 158
  // 159
  // 160
  // 161
  // 162
  // 163
  // 164
  // 165
  // 166
  // 167
  // 168
  // 169
  // 170
  // 171
  // 172
  // 173
  // 174
  // 175
  // 176
  // 177
  // 178
  // 179
  // 180
  // 181
  // 182
  // 183
  // 184
  // 185
  // 186
  // 187
  // 188
  // 189
  // 190
  // 191
  // 192
  // 193
  // 194
  // 195
  // 196
  // 197
  // 198
  // 199
  // 200
  // 201
  // 202
  // 203
  // 204
  // 205
  // 206
  // 207
  // 208
  // 209
  // 210
  // 211
  // 212
  // 213
  // 214
  // 215
  // 216
  // 217
  // 218
  // 219
  // 220
  // 221
  // 222
  // 223
  // 224
  // 225
  // 226
  // 227
  // 228
  // 229
  // 230
  // 231
  // 232
  // 233
  // 234
  // 235
  // 236
  // 237
  // 238
  // 239
  // 240
  // 241
  // 242
  // 243
  // 244
  // 245
  // 246
  // 247
  // 248
  // 249
  // 250
  // 251
  // 252
  // 253
  // 254
  // 255
  // 256
  // 257
  // 258
  // 259
  // 260
  // 261
  // 262
  // 263
  // 264
  // 265
  // 266
  // 267
  // 268
  // 269
  // 270
  // 271
  // 272
  // 273
  // 274
  // 275
  // 276
  // 277
  // 278
  // 279
  // 280
  // 281
  // 282
  // 283
  // 284
  // 285
  // 286
  // 287
  // 288
  // 289
  // 290
  // 291
  // 292
  // 293
  // 294
}


### Command to run and resulting output

```code
dafny verify

What happened?

Parsing /Users/seanmcl/workplace/yucca-new/src/YuccaModelDafny/tmp.dfy
Stack overflow.
Repeat 290 times:
--------------------------------
   at Microsoft.Dafny.Scanner.NextToken()
--------------------------------
   at Microsoft.Dafny.Scanner.Scan()
   at Microsoft.Dafny.Parser.Get()
   at Microsoft.Dafny.Parser.Expect(Int32)
   at Microsoft.Dafny.Parser.ModuleDefinition(DeclModifierData, Microsoft.Dafny.ModuleDefinition, Microsoft.Dafny.ModuleDecl ByRef)
   at Microsoft.Dafny.Parser.SubModuleDecl(DeclModifierData, Microsoft.Dafny.ModuleDefinition, Microsoft.Dafny.ModuleDecl ByRef, Boolean)
   at Microsoft.Dafny.Parser.TopDecl(Microsoft.Dafny.ModuleDefinition, Boolean, Boolean)
   at Microsoft.Dafny.Parser.Dafny()
   at Microsoft.Dafny.Parser.Parse()
   at Microsoft.Dafny.ProgramParser.ParseFile(Microsoft.Dafny.DafnyOptions, System.String, System.Uri)
   at Microsoft.Dafny.ProgramParser.ParseFile(Microsoft.Dafny.DafnyOptions, System.IO.TextReader, System.Uri)
   at Microsoft.Dafny.ProgramParser.ParseFiles(System.String, System.Collections.Generic.IReadOnlyList`1<Microsoft.Dafny.DafnyFile>, Microsoft.Dafny.ErrorReporter, System.Threading.CancellationToken)
   at Microsoft.Dafny.DafnyMain.Parse(System.Collections.Generic.IReadOnlyList`1<Microsoft.Dafny.DafnyFile>, System.String, Microsoft.Dafny.DafnyOptions, Microsoft.Dafny.Program ByRef)
   at Microsoft.Dafny.DafnyMain.ParseCheck(System.IO.TextReader, System.Collections.Generic.IReadOnlyList`1<Microsoft.Dafny.DafnyFile>, System.String, Microsoft.Dafny.DafnyOptions, Microsoft.Dafny.Program ByRef)
   at Microsoft.Dafny.DafnyDriver+<ProcessFilesAsync>d__16.MoveNext()
   at System.Runtime.CompilerServices.AsyncMethodBuilderCore.Start[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](System.__Canon ByRef)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1[[Microsoft.Dafny.DafnyDriver+ExitValue, DafnyDriver, Version=0.0.0.0, Culture=neutral, PublicKeyToken=null]].Start[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](System$
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(System.Collections.Gene

What type of operating system are you experiencing the problem on?

Mac

@seanmcl seanmcl added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Jul 6, 2023
@fabiomadge fabiomadge added the part: parser First phase of Dafny's pipeline label Jul 7, 2023
MikaelMayer added a commit that referenced this issue Aug 15, 2023
MikaelMayer added a commit that referenced this issue Aug 16, 2023
…comments (#4424)

This PR fixes #4261
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
@MikaelMayer MikaelMayer self-assigned this Aug 17, 2023
keyboardDrummer pushed a commit to keyboardDrummer/dafny that referenced this issue Sep 15, 2023
…comments (dafny-lang#4424)

This PR fixes dafny-lang#4261
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer pushed a commit that referenced this issue Sep 19, 2023
…comments (#4424)

This PR fixes #4261
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: parser First phase of Dafny's pipeline
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants