java-semantics print out a message when krun times out

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.

Nov 03 '15 03:11 yilongli

@yilongli Yes, you are right. I didn't think of that. Timeout is a rather clear issue, we can have better output message.

Nov 03 '15 17:11 laurayuwen

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

Jan 15 '16 06:01 20harshita

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.

Jan 15 '16 06:01 laurayuwen

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

Jan 15 '16 11:01 20harshita