File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
src/goto-instrument/contracts Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -75,7 +75,7 @@ class code_contractst
75
75
// / with an assertion that the `requires` clause holds followed by an
76
76
// / assumption that the `ensures` clause holds. In order to ensure that `F`
77
77
// / actually abides by its `ensures` and `requires` clauses, you should
78
- // / separately call `code_constractst ::enforce_contracts()` on `F` and verify
78
+ // / separately call `code_contractst ::enforce_contracts()` on `F` and verify
79
79
// / it using `cbmc --function F`.
80
80
void replace_calls (const std::set<std::string> &to_replace);
81
81
@@ -159,7 +159,7 @@ class code_contractst
159
159
std::unordered_map<goto_programt::const_targett, unsigned , const_target_hash>
160
160
original_loop_number_map;
161
161
162
- // / Loop havoc instructions instrumneted during applying loop contracts.
162
+ // / Loop havoc instructions instrumented during applying loop contracts.
163
163
std::unordered_set<goto_programt::const_targett, const_target_hash>
164
164
loop_havoc_set;
165
165
You can’t perform that action at this time.
0 commit comments