From 9cadc8ddfd0b4597daab0bceb6a80cdac4cfffb4 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Mon, 1 Oct 2012 21:48:34 -0700 Subject: [PATCH] Two change: (1) Bug fix... Check that rf is non-null before calling r_modification (2) Add a hook into assert mechanism for the debugger --- common.cc | 5 +++++ common.h | 4 +++- model.cc | 3 ++- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/common.cc b/common.cc index ac5cb596..e05e094e 100644 --- a/common.cc +++ b/common.cc @@ -29,3 +29,8 @@ void model_print_summary(void) { model->print_summary(); } + +void assert_hook(void) +{ + printf("Add breakpoint to line %u in file %s.\n",__LINE__,__FILE__); +} diff --git a/common.h b/common.h index 2dc8b7d9..003dc805 100644 --- a/common.h +++ b/common.h @@ -18,12 +18,15 @@ #define DBG_ENABLED() (0) #endif +void assert_hook(void); + #define ASSERT(expr) \ do { \ if (!(expr)) { \ fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \ print_trace(); \ model_print_summary(); \ + assert_hook(); \ exit(EXIT_FAILURE); \ } \ } while (0); @@ -32,5 +35,4 @@ do { \ void print_trace(void); void model_print_summary(void); - #endif /* __COMMON_H__ */ diff --git a/model.cc b/model.cc index 9dc1d37c..a22e0214 100644 --- a/model.cc +++ b/model.cc @@ -658,7 +658,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) bool updated = false; if (act->is_read()) { - if (r_modification_order(act, act->get_reads_from())) + const ModelAction *rf = act->get_reads_from(); + if (rf != NULL && r_modification_order(act, rf)) updated = true; } if (act->is_write()) { -- 2.34.1