Open
Description
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: