Repository navigation
print out a message when krun times out #53
Description
It's really confusing to just get an empty *.pkast file and an inner parser error at the start of exec semantics when the prep semantics times out.
Metadata
Metadata
Assignees
Labels
No labels
Activity
laurayuwen commentedon Nov 3, 2015
@yilongli Yes, you are right. I didn't think of that. Timeout is a rather clear issue, we can have better output message.
20harshita commentedon Jan 15, 2016
harshita@harshita-VPCEH25EN:~/java-semantics/src$ kjkompile.sh
Preprocessing semantics:
/home/harshita/java-semantics/tools/kjkompile.sh: line 99: kompile: command not found
Execution semantics:
/home/harshita/java-semantics/tools/kjkompile.sh: line 98: kompile: command not found
Done
//How to overcome from such type of error
laurayuwen commentedon Jan 15, 2016
This 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.
20harshita commentedon Jan 15, 2016
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