silver UnmappableCharacterException on some quote characters

Created by bitbucket user goltzc on 2018-05-09 11:35 Last updated on 2018-05-09 11:50

These quotes trigger an exception when opening a file containing them in vscode:

“ ”

The first character of the file gets highlighted (independent of where the quotes are in the file) and on hovering the highlighted text it shows: java.nio.charset.UnmappableCharacterException: Input length = 1

In the Viper output pannel can be found the following trace:

ERROR: S: The following exception occured in ViperServer: java.nio.charset.UnmappableCharacterException: Input length = 1
 trace:
  java.nio.charset.CoderResult.throwException(Unknown Source)
  sun.nio.cs.StreamDecoder.implRead(Unknown Source)
  sun.nio.cs.StreamDecoder.read(Unknown Source)
  java.io.InputStreamReader.read(Unknown Source)
  java.io.BufferedReader.read1(Unknown Source)
  java.io.BufferedReader.read(Unknown Source)
  java.io.Reader.read(Unknown Source)
  scala.io.BufferedSource.mkString(BufferedSource.scala:96)
  viper.silver.frontend.DefaultFrontend$class.reset(Frontend.scala:167)
  viper.carbon.CarbonFrontend.viper$silver$frontend$SilFrontend$$super$reset(Carbon.scala:29)
  viper.silver.frontend.SilFrontend$class.reset(SilFrontend.scala:133)
  viper.carbon.CarbonFrontend.reset(Carbon.scala:29)
  viper.server.ViperBackend.execute(VerificationWorker.scala:236)
  viper.server.VerificationWorker.run(VerificationWorker.scala:86)
  java.lang.Thread.run(Unknown Source)

The problem is independent of the chosen verification backend.

Attached is a file containing them, just in case copying them here and back somehow messes the characters up.

Attachments:

May 09 '18 11:05 viper-admin

@mschwerhoff commented on 2018-05-09 11:50

Looks like a problem with the Unicode BOM. Running Silicon directly (not via the IDE) on utf8-no-bom.vpr works fine, despite the quotation marks in the file. For utf8-bom.vpr, Silicon reports Parse error: Expected End ([email protected]), but no exception is raised. The latter appears to be raised by the Viper server, i.e. only if then IDE is used.