K-user mailing list

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

I think it should be a syntax error with a nice source location.

Robby

On Thu, Nov 29, 2012 at 6:00 PM, Cansu Erdogan 
<cerdoga2 AT illinois.edu>
 wrote:
> I am not quite sure how this case should be handled. Should I just
> ignore the strict attribute because it is already a Variable? If
> someone can explain me what the behavior should be, I can fix it.
>
> Cansu
>
> On Thu, Nov 29, 2012 at 5:27 PM, Robby Findler
> <robby AT eecs.northwestern.edu>
>  wrote:
>> 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$
>>
>>
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>