How to use the semantics after build

[Stevengre]

I just try krun under .build/defn/verification, and got this error. I want to know how to verify a boogie program using this semantics, and the architecture of this semantics. For example, what is the use of frontend and kore? why don't just use kompile, but kjinja instead?

[Stevengre]

After reading "build" file, I try to use "./frontend/frontend" which gives me a right return.