diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md index cd81a5d4635..a074078b70a 100644 --- a/doc/cprover-manual/properties.md +++ b/doc/cprover-manual/properties.md @@ -130,6 +130,7 @@ The goto-instrument program supports these checks: | `--undefined-shift-check` | add range checks for shift distances | | `--nan-check` | add floating-point NaN checks | | `--uninitialized-check` | add checks for uninitialized locals (experimental) | +| `--race-check` | add data race checks for concurrent programs | | `--error-label label` | check that given label is unreachable | As all of these checks apply across the entire input program, we may wish to diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 5d971063565..afd4d967b70 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -249,7 +249,7 @@ add checks for uninitialized locals (experimental) add check that call stack size of non\-inlined functions never exceeds n .TP \fB\-\-race\-check\fR -add floating\-point data race checks +add data race checks for concurrent programs .SS "Semantic transformations:" .TP \fB\-\-nondet\-volatile\fR diff --git a/regression/goto-instrument/race-check/conditional.c b/regression/goto-instrument/race-check/conditional.c new file mode 100644 index 00000000000..f71d6451340 --- /dev/null +++ b/regression/goto-instrument/race-check/conditional.c @@ -0,0 +1,17 @@ +int shared; +_Bool flag; + +void thread(void) +{ + if(flag) + shared = 1; +} + +int main(void) +{ + flag = 1; +__CPROVER_ASYNC_0: + thread(); + shared = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/conditional.desc b/regression/goto-instrument/race-check/conditional.desc new file mode 100644 index 00000000000..9b62fe820b7 --- /dev/null +++ b/regression/goto-instrument/race-check/conditional.desc @@ -0,0 +1,9 @@ +CORE +conditional.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +W/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/dirty-local-verification.desc b/regression/goto-instrument/race-check/dirty-local-verification.desc new file mode 100644 index 00000000000..b0134e4c089 --- /dev/null +++ b/regression/goto-instrument/race-check/dirty-local-verification.desc @@ -0,0 +1,14 @@ +// This test verifies that --race-check detects a W/W data race on a +// dirty local variable (a local whose address is passed to another thread). +// It is marked KNOWNBUG because CBMC's symex aborts with "pointer handling +// for concurrency is unsound" when a pointer to a local variable is shared +// between threads, preventing verification from completing. +KNOWNBUG +dirty-local.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +W/W data race on main::1::local +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/dirty-local.c b/regression/goto-instrument/race-check/dirty-local.c new file mode 100644 index 00000000000..7b03fe1a6be --- /dev/null +++ b/regression/goto-instrument/race-check/dirty-local.c @@ -0,0 +1,13 @@ +void writer(int *p) +{ + *p = 42; +} + +int main(void) +{ + int local = 0; +__CPROVER_ASYNC_0: + writer(&local); + local = 1; + return 0; +} diff --git a/regression/goto-instrument/race-check/dirty-local.desc b/regression/goto-instrument/race-check/dirty-local.desc new file mode 100644 index 00000000000..8bae3904b2f --- /dev/null +++ b/regression/goto-instrument/race-check/dirty-local.desc @@ -0,0 +1,9 @@ +CORE +dirty-local.c +--race-check +ASSIGN main::1::local\$w_guard := true +W/W data race on main::1::local +^EXIT=6$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/function-call-arg.c b/regression/goto-instrument/race-check/function-call-arg.c new file mode 100644 index 00000000000..a8f14c220e3 --- /dev/null +++ b/regression/goto-instrument/race-check/function-call-arg.c @@ -0,0 +1,19 @@ +int shared; + +void sink(int val) +{ + (void)val; +} + +void writer(void) +{ + shared = 42; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + writer(); + sink(shared); + return 0; +} diff --git a/regression/goto-instrument/race-check/function-call-arg.desc b/regression/goto-instrument/race-check/function-call-arg.desc new file mode 100644 index 00000000000..e52301f58b1 --- /dev/null +++ b/regression/goto-instrument/race-check/function-call-arg.desc @@ -0,0 +1,9 @@ +CORE +function-call-arg.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +R/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/function-call-lhs.c b/regression/goto-instrument/race-check/function-call-lhs.c new file mode 100644 index 00000000000..8bfa90d196c --- /dev/null +++ b/regression/goto-instrument/race-check/function-call-lhs.c @@ -0,0 +1,19 @@ +int shared; + +int source(void) +{ + return 42; +} + +void writer(void) +{ + shared = 1; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + writer(); + shared = source(); + return 0; +} diff --git a/regression/goto-instrument/race-check/function-call-lhs.desc b/regression/goto-instrument/race-check/function-call-lhs.desc new file mode 100644 index 00000000000..437083552d1 --- /dev/null +++ b/regression/goto-instrument/race-check/function-call-lhs.desc @@ -0,0 +1,9 @@ +CORE +function-call-lhs.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +W/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/goto-guard.c b/regression/goto-instrument/race-check/goto-guard.c new file mode 100644 index 00000000000..2a5f2540f29 --- /dev/null +++ b/regression/goto-instrument/race-check/goto-guard.c @@ -0,0 +1,16 @@ +int shared; + +void writer(void) +{ + shared = 42; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + writer(); + if(shared) + { + } + return 0; +} diff --git a/regression/goto-instrument/race-check/goto-guard.desc b/regression/goto-instrument/race-check/goto-guard.desc new file mode 100644 index 00000000000..fb18c2debfd --- /dev/null +++ b/regression/goto-instrument/race-check/goto-guard.desc @@ -0,0 +1,9 @@ +CORE +goto-guard.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +R/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/no-race-sequential.c b/regression/goto-instrument/race-check/no-race-sequential.c new file mode 100644 index 00000000000..1a68d84bd04 --- /dev/null +++ b/regression/goto-instrument/race-check/no-race-sequential.c @@ -0,0 +1,8 @@ +int shared; + +int main(void) +{ + shared = 1; + shared = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/no-race-sequential.desc b/regression/goto-instrument/race-check/no-race-sequential.desc new file mode 100644 index 00000000000..ba3c49dbc2b --- /dev/null +++ b/regression/goto-instrument/race-check/no-race-sequential.desc @@ -0,0 +1,8 @@ +CORE +no-race-sequential.c +--race-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/no-race.c b/regression/goto-instrument/race-check/no-race.c new file mode 100644 index 00000000000..2d8b8943ddb --- /dev/null +++ b/regression/goto-instrument/race-check/no-race.c @@ -0,0 +1,14 @@ +__CPROVER_thread_local int thread_local_var; + +void thread(void) +{ + thread_local_var = 1; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + thread(); + thread_local_var = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/no-race.desc b/regression/goto-instrument/race-check/no-race.desc new file mode 100644 index 00000000000..b2793c39b74 --- /dev/null +++ b/regression/goto-instrument/race-check/no-race.desc @@ -0,0 +1,8 @@ +CORE +no-race.c +--race-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/pointer.c b/regression/goto-instrument/race-check/pointer.c new file mode 100644 index 00000000000..d1bea54ae85 --- /dev/null +++ b/regression/goto-instrument/race-check/pointer.c @@ -0,0 +1,14 @@ +int x; + +void thread(int *p) +{ + *p = 1; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + thread(&x); + x = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/pointer.desc b/regression/goto-instrument/race-check/pointer.desc new file mode 100644 index 00000000000..bee1f5a1196 --- /dev/null +++ b/regression/goto-instrument/race-check/pointer.desc @@ -0,0 +1,9 @@ +CORE +pointer.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +data race on x +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/read-write.c b/regression/goto-instrument/race-check/read-write.c new file mode 100644 index 00000000000..46edb50a447 --- /dev/null +++ b/regression/goto-instrument/race-check/read-write.c @@ -0,0 +1,15 @@ +int shared; + +void thread(void) +{ + shared = 1; +} + +int main(void) +{ + int local; +__CPROVER_ASYNC_0: + thread(); + local = shared; + return 0; +} diff --git a/regression/goto-instrument/race-check/read-write.desc b/regression/goto-instrument/race-check/read-write.desc new file mode 100644 index 00000000000..57beaded5c4 --- /dev/null +++ b/regression/goto-instrument/race-check/read-write.desc @@ -0,0 +1,9 @@ +CORE +read-write.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +R/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/return-value.c b/regression/goto-instrument/race-check/return-value.c new file mode 100644 index 00000000000..06bc6d74fdc --- /dev/null +++ b/regression/goto-instrument/race-check/return-value.c @@ -0,0 +1,20 @@ +int shared; + +int get_shared(void) +{ + return shared; +} + +void writer(void) +{ + shared = 42; +} + +int main(void) +{ + int local; +__CPROVER_ASYNC_0: + writer(); + local = get_shared(); + return 0; +} diff --git a/regression/goto-instrument/race-check/return-value.desc b/regression/goto-instrument/race-check/return-value.desc new file mode 100644 index 00000000000..f297e2f06db --- /dev/null +++ b/regression/goto-instrument/race-check/return-value.desc @@ -0,0 +1,9 @@ +CORE +return-value.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +R/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/write-write.c b/regression/goto-instrument/race-check/write-write.c new file mode 100644 index 00000000000..3bb0020910e --- /dev/null +++ b/regression/goto-instrument/race-check/write-write.c @@ -0,0 +1,14 @@ +int shared; + +void thread(void) +{ + shared = 1; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + thread(); + shared = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/write-write.desc b/regression/goto-instrument/race-check/write-write.desc new file mode 100644 index 00000000000..75f5ff59dc8 --- /dev/null +++ b/regression/goto-instrument/race-check/write-write.desc @@ -0,0 +1,9 @@ +CORE +write-write.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +W/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 570554155b4..86c51e70538 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1940,7 +1940,7 @@ void goto_instrument_parse_optionst::help() HELP_UNINITIALIZED_CHECK " {y--stack-depth} {un} \t add check that call stack size of non-inlined" " functions never exceeds {un}\n" - " {y--race-check} \t add floating-point data race checks\n" + " {y--race-check} \t add data race checks for concurrent programs\n" "\n" "Semantic transformations:\n" HELP_NONDET_VOLATILE diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index fce1b27d0ed..f0151941f2b 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -10,6 +10,8 @@ Date: February 2006 /// \file /// Race Detection for Threaded Goto Programs +/// +/// \see race_check.h for an overview of the instrumentation scheme. #include "race_check.h" @@ -17,6 +19,7 @@ Date: February 2006 #include +#include #include #include "rw_set.h" @@ -30,6 +33,10 @@ Date: February 2006 #define L_M_LAST_ARG(x) #endif +/// Manages boolean "write guard" variables used to detect concurrent writes. +/// For each shared variable `x`, a boolean symbol `x$w_guard` is created. +/// These guards are set to true around write accesses and checked by +/// assertions in other threads. class w_guardst { public: @@ -63,6 +70,9 @@ class w_guardst symbol_table_baset &symbol_table; }; +/// Get or create the boolean guard symbol for a shared variable. +/// \param object: the identifier of the shared variable +/// \return the guard symbol `$w_guard` const symbolt &w_guardst::get_guard_symbol(const irep_idt &object) { const irep_idt identifier=id2string(object)+"$w_guard"; @@ -86,6 +96,8 @@ const symbolt &w_guardst::get_guard_symbol(const irep_idt &object) return *symbol_ptr; } +/// Insert assignments to initialize all write guard variables to false +/// at the beginning of the given program. void w_guardst::add_initialization(goto_programt &goto_program) const { goto_programt::targett t=goto_program.instructions.begin(); @@ -105,6 +117,10 @@ void w_guardst::add_initialization(goto_programt &goto_program) const } } +/// Build a human-readable comment for a race-check assertion. +/// \param entry: the read/write set entry describing the access +/// \param write: true if this is a W/W race check, false for R/W +/// \return a string like "R/W data race on x" or "W/W data race on x" static std::string comment(const rw_set_baset::entryt &entry, bool write) { std::string result; @@ -118,7 +134,15 @@ static std::string comment(const rw_set_baset::entryt &entry, bool write) return result; } -static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) +/// Check whether a symbol refers to a shared (non-thread-local) variable, +/// excluding internal CPROVER symbols that should not be race-checked. +/// A variable is considered shared if it is globally shared or if it is a +/// "dirty" local (its address has been taken, so it may be accessible from +/// other threads). +static bool is_shared( + const namespacet &ns, + const symbol_exprt &symbol_expr, + const dirtyt &dirty) { const irep_idt &identifier=symbol_expr.get_identifier(); @@ -132,23 +156,27 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) return false; // no race check const symbolt &symbol=ns.lookup(identifier); - return symbol.is_shared(); + return !symbol.is_function() && (symbol.is_shared() || dirty(identifier)); } -static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set) +/// Check whether any entry in the read/write set refers to a shared variable. +static bool has_shared_entries( + const namespacet &ns, + const rw_set_baset &rw_set, + const dirtyt &dirty) { for(rw_set_baset::entriest::const_iterator it=rw_set.r_entries.begin(); it!=rw_set.r_entries.end(); it++) - if(is_shared(ns, it->second.symbol_expr)) + if(is_shared(ns, it->second.symbol_expr, dirty)) return true; for(rw_set_baset::entriest::const_iterator it=rw_set.w_entries.begin(); it!=rw_set.w_entries.end(); it++) - if(is_shared(ns, it->second.symbol_expr)) + if(is_shared(ns, it->second.symbol_expr, dirty)) return true; return false; @@ -164,6 +192,7 @@ static void race_check( L_M_ARG(const goto_functionst::goto_functiont &goto_function) goto_programt &goto_program, w_guardst &w_guards, + const dirtyt &dirty, message_handlert &message_handler) // clang-format on { @@ -177,7 +206,7 @@ static void race_check( { goto_programt::instructiont &instruction=*i_it; - if(instruction.is_assign()) + if(instruction.is_assign() || instruction.is_function_call()) { rw_set_loct rw_set( ns, @@ -186,7 +215,7 @@ static void race_check( i_it L_M_LAST_ARG(local_may), message_handler); - if(!has_shared_entries(ns, rw_set)) + if(!has_shared_entries(ns, rw_set, dirty)) continue; goto_programt::instructiont original_instruction; @@ -199,7 +228,7 @@ static void race_check( // now add assignments for what is written -- set for(const auto &w_entry : rw_set.w_entries) { - if(!is_shared(ns, w_entry.second.symbol_expr)) + if(!is_shared(ns, w_entry.second.symbol_expr, dirty)) continue; goto_program.insert_before( @@ -219,7 +248,7 @@ static void race_check( // now add assignments for what is written -- reset for(const auto &w_entry : rw_set.w_entries) { - if(!is_shared(ns, w_entry.second.symbol_expr)) + if(!is_shared(ns, w_entry.second.symbol_expr, dirty)) continue; goto_program.insert_before( @@ -233,12 +262,13 @@ static void race_check( // now add assertions for what is read and written for(const auto &r_entry : rw_set.r_entries) { - if(!is_shared(ns, r_entry.second.symbol_expr)) + if(!is_shared(ns, r_entry.second.symbol_expr, dirty)) continue; source_locationt annotated_location = original_instruction.source_location(); annotated_location.set_comment(comment(r_entry.second, false)); + annotated_location.set_property_class("race-check"); goto_program.insert_before( i_it, goto_programt::make_assertion( @@ -247,12 +277,13 @@ static void race_check( for(const auto &w_entry : rw_set.w_entries) { - if(!is_shared(ns, w_entry.second.symbol_expr)) + if(!is_shared(ns, w_entry.second.symbol_expr, dirty)) continue; source_locationt annotated_location = original_instruction.source_location(); annotated_location.set_comment(comment(w_entry.second, true)); + annotated_location.set_property_class("race-check"); goto_program.insert_before( i_it, goto_programt::make_assertion( @@ -261,6 +292,35 @@ static void race_check( i_it--; // the for loop already counts us up } + else if( + instruction.is_goto() || instruction.is_assume() || + instruction.is_assert() || instruction.is_set_return_value()) + { + rw_set_loct rw_set( + ns, + value_sets, + function_id, + i_it L_M_LAST_ARG(local_may), + message_handler); + + if(!has_shared_entries(ns, rw_set, dirty)) + continue; + + // add R/W assertions for shared reads before the instruction + for(const auto &r_entry : rw_set.r_entries) + { + if(!is_shared(ns, r_entry.second.symbol_expr, dirty)) + continue; + + source_locationt annotated_location = instruction.source_location(); + annotated_location.set_comment(comment(r_entry.second, false)); + annotated_location.set_property_class("race-check"); + goto_program.insert_before( + i_it, + goto_programt::make_assertion( + w_guards.get_assertion(r_entry.second), annotated_location)); + } + } } remove_skip(goto_program); @@ -277,6 +337,11 @@ void race_check( message_handlert &message_handler) { w_guardst w_guards(symbol_table); + // When called for a single function we don't have the full goto_functions + // to build a complete dirtyt, so we use an empty one. The goto_modelt + // overload below computes a proper whole-program dirty analysis. + dirtyt dirty; + dirty.build(goto_functionst()); race_check( value_sets, @@ -284,6 +349,7 @@ void race_check( function_id, L_M_ARG(goto_function) goto_program, w_guards, + dirty, message_handler); w_guards.add_initialization(goto_program); @@ -296,6 +362,7 @@ void race_check( message_handlert &message_handler) { w_guardst w_guards(goto_model.symbol_table); + dirtyt dirty(goto_model.goto_functions); for(auto &gf_entry : goto_model.goto_functions.function_map) { @@ -309,6 +376,7 @@ void race_check( gf_entry.first, L_M_ARG(gf_entry.second) gf_entry.second.body, w_guards, + dirty, message_handler); } } diff --git a/src/goto-instrument/race_check.h b/src/goto-instrument/race_check.h index e4d6daa3443..542e8bd3570 100644 --- a/src/goto-instrument/race_check.h +++ b/src/goto-instrument/race_check.h @@ -10,6 +10,46 @@ Date: February 2006 /// \file /// Race Detection for Threaded Goto Programs +/// +/// This implements a data-race detector for concurrent programs, inspired by +/// the Eraser algorithm (Savage et al., "Eraser: A Dynamic Data Race Detector +/// for Multithreaded Programs", ACM TOCS 1997). While Eraser uses lockset +/// tracking at runtime, this implementation adapts the core idea for static +/// verification via bounded model checking: it instruments the program with +/// boolean "write guard" flags and assertions so that CBMC's exploration of +/// thread interleavings can reveal conflicting concurrent accesses. +/// +/// A data race occurs when two threads access the same shared memory location +/// concurrently and at least one access is a write. This instrumentation +/// detects two kinds of races: +/// - R/W races: one thread reads a variable while another writes it. +/// - W/W races: two threads write the same variable concurrently. +/// +/// For each assignment or function call that accesses shared variables, the +/// instrumentation replaces the original instruction with the following +/// sequence: +/// +/// 1. For each shared variable `x` written: set `x$w_guard` to the guard +/// condition under which the write occurs. +/// 2. Execute the original instruction. +/// 3. For each shared variable `x` written: reset `x$w_guard` to false. +/// 4. For each shared variable `y` read: assert `!y$w_guard` (R/W check). +/// 5. For each shared variable `x` written: assert `!x$w_guard` (W/W check). +/// +/// For instructions that only read shared variables (GOTO/ASSUME/ASSERT +/// guards, SET_RETURN_VALUE), only R/W assertions (step 4) are added before +/// the instruction. +/// +/// During symbolic execution of concurrent programs, CBMC explores thread +/// interleavings. If another thread's write guard is set (step 1) when the +/// current thread checks it (steps 4/5), the assertion fails, indicating a +/// data race. +/// +/// Pointer dereferences are resolved using value-set analysis (or, when +/// LOCAL_MAY is defined, local may-alias analysis) so that races through +/// aliased pointer accesses are detected. For example, if thread A writes +/// `*p` and thread B writes `x`, and `p` points to `x`, the instrumentation +/// will detect the W/W race on `x`. #ifndef CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H #define CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H @@ -25,6 +65,12 @@ class goto_programt; class message_handlert; class value_setst; +/// Instrument a single function with data-race detection assertions. +/// \param value_sets: value-set analysis results for pointer resolution +/// \param symbol_table: the symbol table (modified to add guard symbols) +/// \param function_id: identifier of the function being instrumented +/// \param goto_program: the function body to instrument +/// \param message_handler: handler for status and diagnostic messages void race_check( value_setst &, class symbol_table_baset &, @@ -35,6 +81,11 @@ void race_check( goto_programt &goto_program, message_handlert &); +/// Instrument all functions in a goto model with data-race detection +/// assertions. Skips the entry point and the initialization function. +/// \param value_sets: value-set analysis results for pointer resolution +/// \param goto_model: the goto model to instrument +/// \param message_handler: handler for status and diagnostic messages void race_check(value_setst &, goto_modelt &, message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index b1c03a6c273..a5f81f287f2 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -68,6 +68,10 @@ void _rw_set_loct::compute() if(target->call_lhs().is_not_nil()) write(target->call_lhs()); } + else if(target->is_set_return_value()) + { + read(target->return_value()); + } } void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)