Repository navigation
print out a message when krun times out #53
Description
Activity
@yilongli Yes, you are right. I didn't think of that. Timeout is a rather clear issue, we can have better output message.
harshita@harshita-VPCEH25EN:~/java-semantics/src$ kjkompile.sh
Preprocessing semantics:
/home/harshita/java-semantics/tools/kjkompile.sh: line 99: kompile: command not foundExecution semantics:
/home/harshita/java-semantics/tools/kjkompile.sh: line 98: kompile: command not foundDone
//How to overcome from such type of errorThis says the kompile command cannot be found, Have you add k's bin to path? Kjkompile is a wrapper that wraps a couple k command together, and the error reported is k command not found.
kjkompile.sh
Preprocessing semantics:
[Error] Compiler: Could not find sorts: [SwitchLabel]
Source(/home/harshita/java-semantics/src/./prep/../common/list-syntax.k)
Location(36,38,36,95)Execution semantics:
[Error] Critical: Could not find file: builtins/model-checker.k
Lookup directories:[./exec,
/home/harshita/new/k/lib/java/../../include/builtin]
Source(/home/harshita/java-semantics/src/./exec/ltl-support.k)
Location(1,1,1,34)
still producing error
It's really confusing to just get an empty
*.pkastfile and an inner parser error at the start of exec semantics when the prep semantics times out.