Skip to content

Commit b591f66

Browse files
committed
Fix typos in dfcc
1 parent 339d17c commit b591f66

File tree

2 files changed

+7
-7
lines changed

2 files changed

+7
-7
lines changed

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ void dfcc_instrumentt::get_instrumented_functions(
133133
are allowed for deallocation by the write set.
134134
135135
There is also a number of CPROVER global static symbols that are used to
136-
suport memory safety property instrumentation, and assignments to these
136+
support memory safety property instrumentation, and assignments to these
137137
statics should always be allowed (i.e not instrumented):
138138
- __CPROVER_alloca_object,
139139
- __CPROVER_dead_object,
@@ -831,7 +831,7 @@ void dfcc_instrumentt::instrument_assign(
831831
if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_allocate)
832832
{
833833
// ```
834-
// CALL lhs := side_effect(statemet = ID_allocate, args = {size, clear});
834+
// CALL lhs := side_effect(statement = ID_allocate, args = {size, clear});
835835
// ----
836836
// IF !write_set GOTO skip_target;
837837
// CALL add_allocated(write_set, lhs);
@@ -1078,7 +1078,7 @@ void dfcc_instrumentt::instrument_other(
10781078
// DEAD check_array_set;
10791079
// skip_target: SKIP;
10801080
// ----
1081-
// OTHER {statemet = array_set, args = {dest, value}};
1081+
// OTHER {statement = array_set, args = {dest, value}};
10821082
// ```
10831083
const auto &mode = utils.get_function_symbol(function_id).mode;
10841084
goto_programt payload;
@@ -1139,7 +1139,7 @@ void dfcc_instrumentt::instrument_other(
11391139
// DEAD check_array_replace;
11401140
// skip_target: SKIP;
11411141
// ----
1142-
// OTHER {statemet = array_replace, args = {dest, src}};
1142+
// OTHER {statement = array_replace, args = {dest, src}};
11431143
// ```
11441144
const auto &mode = utils.get_function_symbol(function_id).mode;
11451145
goto_programt payload;

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ class dfcc_instrumentt
105105
/// variables in the write set.
106106
///
107107
/// \pre The function must be a function wrapped for contract checking or
108-
/// replacemend. For other functions \ref instrument_function must be used
108+
/// replacement. For other functions \ref instrument_function must be used
109109
/// instead.
110110
///
111111
/// \param wrapped_function_id The name of the function, used to retrieve the
@@ -309,7 +309,7 @@ class dfcc_instrumentt
309309

310310
/// Instrument the \p lhs of an `ASSIGN lhs := rhs` instruction by
311311
/// adding an inclusion check of \p lhs in \p write_set.
312-
/// If \ref is_dead_object_update returns a successfull match, the matched
312+
/// If \ref is_dead_object_update returns a successful match, the matched
313313
/// pointer expression is removed from \p write_set.
314314
/// If \p rhs is a `side_effect_expr(ID_allocate)`, the allocated pointer gets
315315
/// added to the \p write_set.
@@ -332,7 +332,7 @@ class dfcc_instrumentt
332332
/// Before calling a function pointer, performs a dynamic lookup into
333333
/// the map of instrumented function provided by
334334
/// \ref dfcc_libraryt.get_instrumented_functions_map_symbol,
335-
/// and passes the write_set parameter to the funciton pointer only if
335+
/// and passes the write_set parameter to the function pointer only if
336336
/// it points to a function known to be instrumented and hence able to accept
337337
/// this parameter.
338338
/// \pre \p target points to a `CALL` instruction where the function

0 commit comments

Comments
 (0)