K-user mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

Hi all: when a strictness annotation is nonsense, like the one below, the version of K I downloaded today from the website raises a JS error.

Input:

module JS

  syntax Expr ::= Int

  syntax Stmt ::= Expr       [strict]

endmodule

output:

$ ./k.11-29/bin/kompile js.k

java.lang.ClassCastException: org.kframework.kil.Variable cannot be cast to org.kframework.kil.TermCons

at org.kframework.compile.transformers.StrictnessToContexts.strictInAll(StrictnessToContexts.java:192)

at org.kframework.compile.transformers.StrictnessToContexts.transform(StrictnessToContexts.java:64)

at org.kframework.kil.Module.accept(Module.java:132)

at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:30)

at org.kframework.kil.Definition.accept(Definition.java:117)

at org.kframework.compile.utils.CompilerTransformerStep.compile(CompilerTransformerStep.java:25)

at org.kframework.main.KompileFrontEnd.compile(KompileFrontEnd.java:532)

at org.kframework.main.KompileFrontEnd.compile(KompileFrontEnd.java:492)

at org.kframework.main.KompileFrontEnd.kompile(KompileFrontEnd.java:183)

at org.kframework.main.Main.main(Main.java:17)

[robby@yanpu] ~/git/robby/395-2012$