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

Compilation of raw backslash is failing in C# backend #6109

Open
MikaelMayer opened this issue Feb 17, 2025 · 0 comments · May be fixed by #6111
Open

Compilation of raw backslash is failing in C# backend #6109

MikaelMayer opened this issue Feb 17, 2025 · 0 comments · May be fixed by #6111
Labels
difficulty: good-first-issue Good first issues during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@MikaelMayer
Copy link
Member

Dafny version

Since 4.4.0 at least

Code to produce this issue

method Main() {
  print @"\";
}

Command to run and resulting output

dafny build -t:cs file.dfy

What happened?

We get this exception:

Unhandled exception: System.IndexOutOfRangeException: Index was outside the bounds of the array.
   at System.String.get_Chars(Int32 index)
   at Microsoft.Dafny.Util.TokensWithEscapes(String p, Boolean isVerbatimString)+MoveNext() in C:\Users
\mimayere\Documents\dafny\Source\DafnyCore\Generic\Util.cs:line 406
   at System.Linq.Enumerable.SelectEnumerableIterator`2.MoveNext()
   at System.String.Join(String separator, IEnumerable`1 values)
   at Microsoft.Dafny.Util.ReplaceTokensWithEscapes(String s, Regex pattern, MatchEvaluator evaluator)
in dafny\Source\DafnyCore\Generic\Util.cs:line 293
   at Microsoft.Dafny.Util.ExpandUnicodeEscapes(String s, Boolean lowerCaseU) in C:\Users\mimayere\Docu
ments\dafny\Source\DafnyCore\Generic\Util.cs:line 299
   at Microsoft.Dafny.Compilers.CsharpCodeGenerator.EmitStringLiteral(String str, Boolean isVerbatim, C
oncreteSyntaxTree wr) in dafny\Source\DafnyCore\Backends\CSharp\CsharpCodeG
enerator.cs:line 2300
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrStringLiteral(StringLiteralExpr str, Concrete
SyntaxTree wr) in dafny\Source\DafnyCore\Backends\SinglePassCodeGenerator\S
inglePassCodeGenerator.cs:line 5206
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.StringLiteral(StringLiteralExpr str) in C:\User
s\mimayere\Documents\dafny\Source\DafnyCore\Backends\SinglePassCodeGenerator\SinglePassCodeGenerator.cs
:line 5199
   at Microsoft.Dafny.Compilers.CsharpCodeGenerator.EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr
e) in dafny\Source\DafnyCore\Backends\CSharp\CsharpCodeGenerator.cs:line 22
52
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitExpr(Expression expr, Boolean inLetExprBody
, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) in dafny\Source\DafnyCo
re\Backends\SinglePassCodeGenerator\SinglePassCodeGenerator.Expression.cs:line 31
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.Expr(Expression expr, Boolean inLetExprBody, Co
ncreteSyntaxTree wStmts) in dafny\Source\DafnyCore\Backends\SinglePassCodeG
enerator\SinglePassCodeGenerator.cs:line 4829
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitBinaryExpr(Boolean inLetExprBody, ConcreteS
yntaxTree wr, ConcreteSyntaxTree wStmts, BinaryExpr binary) in dafny\Source
\DafnyCore\Backends\SinglePassCodeGenerator\SinglePassCodeGenerator.Expression.cs:line 646
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitExpr(Expression expr, Boolean inLetExprBody
, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) in dafny\Source\DafnyCo
re\Backends\SinglePassCodeGenerator\SinglePassCodeGenerator.Expression.cs:line 317
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrExprOpt(Expression expr, Type resultType, Con
creteSyntaxTree wr, ConcreteSyntaxTree wStmts, Boolean inLetExprBody, IVariable accumulatorVar, Optimiz
edExpressionContinuation continuation) in dafny\Source\DafnyCore\Backends\S
inglePassCodeGenerator\SinglePassCodeGenerator.cs:line 3042
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrExprOpt(Expression expr, Type resultType, Con
creteSyntaxTree wr, ConcreteSyntaxTree wStmts, Boolean inLetExprBody, IVariable accumulatorVar, Optimiz
edExpressionContinuation continuation) in dafny\Source\DafnyCore\Backends\S
inglePassCodeGenerator\SinglePassCodeGenerator.cs:line 3050
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrExprOpt(Expression expr, Type resultType, Con
creteSyntaxTree wr, ConcreteSyntaxTree wStmts, Boolean inLetExprBody, IVariable accumulatorVar, Optimiz
edExpressionContinuation continuation) in dafny\Source\DafnyCore\Backends\S
inglePassCodeGenerator\SinglePassCodeGenerator.cs:line 3050
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.CompileReturnBody(Expression body, Type resultT
ype, ConcreteSyntaxTree wr, IVariable accumulatorVar) in dafny\Source\Dafny
Core\Backends\SinglePassCodeGenerator\SinglePassCodeGenerator.cs:line 3179
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.CompileFunction(Function f, IClassWriter cw, Bo
olean lookasideBody) in dafny\Source\DafnyCore\Backends\SinglePassCodeGener
ator\SinglePassCodeGenerator.cs:line 2814

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

Windows

@MikaelMayer MikaelMayer added during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label difficulty: good-first-issue Good first issues labels Feb 17, 2025
MikaelMayer added a commit that referenced this issue Feb 17, 2025
@MikaelMayer MikaelMayer linked a pull request Feb 17, 2025 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
difficulty: good-first-issue Good first issues during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant