diff options
Diffstat (limited to 'include/rv/ltl_monitor.h')
| -rw-r--r-- | include/rv/ltl_monitor.h | 18 |
1 files changed, 5 insertions, 13 deletions
diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h index 5368cf5fd623..00c42b36f961 100644 --- a/include/rv/ltl_monitor.h +++ b/include/rv/ltl_monitor.h @@ -16,21 +16,12 @@ #error "Please include $(MODEL_NAME).h generated by rvgen" #endif -#ifdef CONFIG_RV_REACTORS #define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME) -static struct rv_monitor RV_MONITOR_NAME; -static void rv_cond_react(struct task_struct *task) -{ - if (!rv_reacting_on() || !RV_MONITOR_NAME.react) - return; - RV_MONITOR_NAME.react("rv: "__stringify(MONITOR_NAME)": %s[%d]: violation detected\n", - task->comm, task->pid); -} +#ifdef CONFIG_RV_REACTORS +static struct rv_monitor RV_MONITOR_NAME; #else -static void rv_cond_react(struct task_struct *task) -{ -} +extern struct rv_monitor RV_MONITOR_NAME; #endif static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT; @@ -98,7 +89,8 @@ static void ltl_monitor_destroy(void) static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon) { CONCATENATE(trace_error_, MONITOR_NAME)(task); - rv_cond_react(task); + rv_react(&RV_MONITOR_NAME, "rv: "__stringify(MONITOR_NAME)": %s[%d]: violation detected\n", + task->comm, task->pid); } static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon) |