diff options
Diffstat (limited to 'include/rv')
| -rw-r--r-- | include/rv/da_monitor.h | 35 | ||||
| -rw-r--r-- | include/rv/ltl_monitor.h | 17 |
2 files changed, 12 insertions, 40 deletions
diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index 17fa4f6e5ea6..0cef64366538 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -16,34 +16,19 @@ #include <linux/bug.h> #include <linux/sched.h> -#ifdef CONFIG_RV_REACTORS - -#define DECLARE_RV_REACTING_HELPERS(name, type) \ -static void cond_react_##name(type curr_state, type event) \ -{ \ - if (!rv_reacting_on() || !rv_##name.react) \ - return; \ - rv_##name.react("rv: monitor %s does not allow event %s on state %s\n", \ - #name, \ - model_get_event_name_##name(event), \ - model_get_state_name_##name(curr_state)); \ -} - -#else /* CONFIG_RV_REACTOR */ - -#define DECLARE_RV_REACTING_HELPERS(name, type) \ -static void cond_react_##name(type curr_state, type event) \ -{ \ - return; \ -} -#endif - /* * Generic helpers for all types of deterministic automata monitors. */ #define DECLARE_DA_MON_GENERIC_HELPERS(name, type) \ \ -DECLARE_RV_REACTING_HELPERS(name, type) \ +static void react_##name(type curr_state, type event) \ +{ \ + rv_react(&rv_##name, \ + "rv: monitor %s does not allow event %s on state %s\n", \ + #name, \ + model_get_event_name_##name(event), \ + model_get_state_name_##name(curr_state)); \ +} \ \ /* \ * da_monitor_reset_##name - reset a monitor and setting it to init state \ @@ -126,7 +111,7 @@ da_event_##name(struct da_monitor *da_mon, enum events_##name event) \ for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \ next_state = model_get_next_state_##name(curr_state, event); \ if (next_state == INVALID_STATE) { \ - cond_react_##name(curr_state, event); \ + react_##name(curr_state, event); \ trace_error_##name(model_get_state_name_##name(curr_state), \ model_get_event_name_##name(event)); \ return false; \ @@ -165,7 +150,7 @@ static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \ next_state = model_get_next_state_##name(curr_state, event); \ if (next_state == INVALID_STATE) { \ - cond_react_##name(curr_state, event); \ + react_##name(curr_state, event); \ trace_error_##name(tsk->pid, \ model_get_state_name_##name(curr_state), \ model_get_event_name_##name(event)); \ diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h index 5368cf5fd623..eff60cd61106 100644 --- a/include/rv/ltl_monitor.h +++ b/include/rv/ltl_monitor.h @@ -16,23 +16,9 @@ #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); -} -#else -static void rv_cond_react(struct task_struct *task) -{ -} -#endif - static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT; static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon); @@ -98,7 +84,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) |