Debugging

Function evaluation

K function rules correspond to Kore equations. There are three options available in kore-exec to debug equations:

• --debug-apply-equation EQUATION-IDENTIFIER
  Record when an equation matching EQUATION-IDENTIFIER is successfully applied.
• --debug-attempt-equation EQUATION-IDENTIFIER
  Record when an equation matching EQUATION-IDENTIFIER is attempted. The stages of equation evaluation are logged (argument matching, instantiation, and requirement checking), but the final result (whether the equation is applied or not) is not logged; this may be important if multiple equations could apply.
• --debug-equation EQUATION-IDENTIFIER
  Enables both --debug-apply-equation and --debug-attempt-equation, so that every equation attempt and every applied equation is logged. This is the option we will use most often.

An EQUATION-IDENTIFIER is one of the following:

• A Kore symbol name, matching all equations (rules) with the named symbol at the top of the left-hand side.
• A K label name, matching all equations (rules) with the named label at the top of the left-hand side.
• An equation name of the form MODULE-NAME.rule-name, matching the named equation only.