We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 39f9c87 commit b6bae90Copy full SHA for b6bae90
src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h
@@ -285,8 +285,6 @@ class dfcc_instrumentt
285
286
/// Instrument the \p lhs of an `ASSIGN lhs := rhs` instruction by
287
/// adding an inclusion check of \p lhs in \p write_set.
288
- /// If \ref is_dead_object_update returns a successful match, the matched
289
- /// pointer expression is removed from \p write_set.
290
/// If \p rhs is a `side_effect_expr(ID_allocate)`, the allocated pointer gets
291
/// added to the \p write_set.
292
/// \pre \p target points to an `ASSIGN` instruction.
0 commit comments