0

在 K 框架中，可以使用-cswitchkrun将其他变量传递给初始配置，然后是 default $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)

如何传递字符串参数？

4

1 回答 1

1

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

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

于 2020-06-12T14:42:12.427 回答