[K-Bug] Broken MInt literal parsing
Opened this issue · 0 comments
virgil-serbanuta commented
What component is the issue in?
None
Which command
- kompile
- kast
- krun
- kprove
- kprovex
- ksearch
What K Version?
v7.1.104-0-g34892bf1cc
Operating System
Linux
K Definitions (If Possible)
module A-SYNTAX
imports INT
imports MINT
syntax MInt{64}
syntax A ::= a(Int, MInt{64})
endmodule
module A
imports A-SYNTAX
syntax A ::= b(MInt{64}, MInt{64}, MInt{64})
rule a(I, M) => b(Int2MInt(I), M, 100p64)
configuration <k> $PGM:A </k>
endmodule
Steps to Reproduce
kompile a.k
krun -cPGM='a(100, 100p64)'Note that the result is
<k>
b ( 100p64 , 6p64 , 100p64 ) ~> .K
</k>
i.e., 100p64 in the input was parsed, for some reason as 6p64. Note that 100p64 is parsed properly in the k file. Also, a simple kast call parses the value properly:
$ kast -e 'a(100,100p64)'
`a(_,_)_A-SYNTAX_A_Int_MInt`(#token("100","Int"),#token("100p64","MInt{64}"))