Add char literals.

Disallow backslash from being part of identifier names.

2 files changed, 15 insertions, 1 deletions

diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy
index 54764662..f56f36e1 100644
--- a/Test/dafny0/Strings.dfy
+++ b/Test/dafny0/Strings.dfy
@@ -35,6 +35,8 @@ method Main()
   print "Escape X: ", x, "\n";

   print "Escape Y: ", y, "\n";

   print "Escape Z: ", z, "\n";

+  var c, d := CharEscapes();

+  print "Here is the end" + [c, d] + [' ', ' ', ' '] + [[d]][0] + "   ", d, "\n";

 }

 

 method GimmieAChar(s: string) returns (ch: char)

@@ -55,3 +57,13 @@ method Escapes() returns (x: string, y: string, z: string)
   assert x == y;

   z := "There needs to be \u0052\u0026\u0044\n\tYes, sir";

 }

+

+method CharEscapes() returns (c: char, d: char)

+{

+  // cool variable names, huh?

+  var 'x := 'R';

+  var x' := '\u0052';

+  assert 'x==x' ;

+  c := '\n';

+  d := '*';

+}

diff --git a/Test/dafny0/Strings.dfy.expect b/Test/dafny0/Strings.dfy.expect
index 56bffd98..e05312b7 100644
--- a/Test/dafny0/Strings.dfy.expect
+++ b/Test/dafny0/Strings.dfy.expect
@@ -1,5 +1,5 @@
 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 14 verified, 0 errors

 Program compiled successfully

 Running...

 

@@ -9,3 +9,5 @@ Escape X: I say "hello" \ you say 'good bye'
 Escape Y: I say "hello" \ you say 'good bye'
 Escape Z: There needs to be R&D
 	Yes, sir
+Here is the end
+*   *   *