如何在 K 框架中将字符串参数传递给“krun”？答案

【问题标题】：How to pass a string argument to `krun` in K framework?如何在 K 框架中将字符串参数传递给“krun”？
【发布时间】：2020-06-12 13:26:46
【问题描述】：

在K框架中，可以使用krun的-c开关将其他变量传递给初始配置，然后默认$PGM。例如，可能有这样的代码：

configuration <T color="yellow">
                <k color="green"> $PGM:Pgm </k>
                <something> $SOMEARG:Int </something>
              </T>

并运行kompile imp.k; krun tests/sum.imp -cSOMEARG=3，$SOMEARG 变量得到值3。但是，当我尝试传递字符串时遇到了问题：

configuration <T color="yellow">
                <k color="green"> $PGM:Pgm </k>
                <something> $SOMEARG:String </something>
              </T>

kompile 之后的命令

krun tests/sum.imp -cSOMEARG=\"hello\" --debug

输出：

org.kframework.utils.errorsystem.KEMException: [Error] Critical: Parser returned a non-zero exit code: 113
Stdout:

Stderr:
[Error] Inner Parser: Parse error: unexpected token 'hello'.
    Source(<command line: -e>)
    Location(1,1,1,6)

    at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:130)
    at org.kframework.utils.errorsystem.KEMException.criticalError(KEMException.java:39)
    at org.kframework.krun.KRun.externalParse(KRun.java:237)
    at org.kframework.krun.KRun.parseConfigVars(KRun.java:161)
    at org.kframework.krun.KRun.run(KRun.java:77)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:95)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
    at org.kframework.main.Main.runApplication(Main.java:118)
    at org.kframework.main.Main.runApplication(Main.java:108)
    at org.kframework.main.Main.main(Main.java:56)

如何传递字符串参数？

【问题讨论】：

标签： kframework

【解决方案1】：

这是我们使用的选项解析库版本中的一个错误，导致它尝试取消引号，即使这实际上是 shell 的角色。它已在最新版本的选项库中修复。您可以在此处跟踪错误修复的进度：https://github.com/kframework/k/pull/1335

我希望它会在不久的将来得到修复。

【讨论】：