[K-Bug] AssertionError for incomplete rule

[virgil-serbanuta]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v7.1.121-0-g894298664c

Operating System

Linux

K Definitions (If Possible)

a.k:

module A
  imports INT

  rule [my-rule]:
  rule 1 => 2
endmodule

Steps to Reproduce

kompile a.k

This produces the following error:

[Error] Internal: Uncaught exception thrown of type AssertionError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/runtimeverification/k/issues
(AssertionError: did not expect IOException)

If I run kompile with --debug:

java.lang.AssertionError: did not expect IOException
        at org.kframework.parser.outer.Outer.offsetLine(Outer.java:270)
        at org.kframework.parser.outer.Outer.makeStringSentence(Outer.java:223)
        at org.kframework.parser.outer.Outer.Bubble(Outer.java:442)
        at org.kframework.parser.outer.Outer.Sentence(Outer.java:749)
        at org.kframework.parser.outer.Outer.Module(Outer.java:661)
        at org.kframework.parser.outer.Outer.Start(Outer.java:607)
        at org.kframework.parser.outer.Outer.parse(Outer.java:79)
        at org.kframework.parser.ParserUtils.slurp(ParserUtils.java:117)
        at org.kframework.parser.ParserUtils.loadModules(ParserUtils.java:220)
        at org.kframework.parser.ParserUtils.loadDefinition(ParserUtils.java:393)
        at org.kframework.parser.ParserUtils.loadDefinition(ParserUtils.java:355)
        at org.kframework.kompile.DefinitionParsing.parseDefinition(DefinitionParsing.java:308)
        at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:231)
        at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:389)
        at org.kframework.kompile.Kompile.run(Kompile.java:212)
        at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:91)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:60)
        at org.kframework.main.Main.runApplication(Main.java:127)
        at org.kframework.main.Main.runApplication(Main.java:117)
        at org.kframework.main.Main.main(Main.java:58)
Caused by: java.io.IOException: PGCC end of stream
        at org.kframework.parser.outer.AbstractCharStream.fillBuff(AbstractCharStream.java:278)
        at org.kframework.parser.outer.AbstractCharStream.readChar(AbstractCharStream.java:367)
        at org.kframework.parser.outer.Outer.offsetLine(Outer.java:269)
        ... 19 more
[Error] Internal: Uncaught exception thrown of type AssertionError
(AssertionError: did not expect IOException)

Expected Results

A reasonable error containing the line and column where the error occurred.