Exporting kore_symbol in hook_events and exposing symbol entry point in kore_parser

[Robertorosmaninho]

This PR introduces the new version of the LLVM Backend Proof Hints: Version 10.

The major update is in the llvm_hook_event, which will have a new field: kore_symbol.
The new format of hook accepted and produced is:

symbol_name       ::= string
hook              ::= WORD(0xAA) name symbol_name location arg* WORD(0xBB) kore_term

It also exposes the symbol entry point in the kore_parser.

This modification will help the Math Proof Team from Pi2 to parse the llvm_hook_event->kore_symbol and llvm_function_event using the same method.

[Baltoli]

There's a big switch-case statement where we parse sentences; is it possible to refactor the code in that part to use this new method?

[Baltoli]

You will need to bump the hint trace format version here as you're adding new data to the trace.

[Robertorosmaninho]

There's a big switch-case statement where we parse sentences; is it possible to refactor the code in that part to use this new method?

I can do it in application_pattern but not in sentence. The difference is that in the last, we're setting it as hooked or not, and we're using sort_variables(symbol.get()) instead of init_pattern_arguments().

I've modified the code to use symbol in application_pattern .

[Baltoli]

Makes sense!