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
7575 // / with an assertion that the `requires` clause holds followed by an
7676 // / assumption that the `ensures` clause holds. In order to ensure that `F`
7777 // / 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
7979 // / it using `cbmc --function F`.
8080 void replace_calls (const std::set<std::string> &to_replace);
8181
@@ -159,7 +159,7 @@ class code_contractst
159159 std::unordered_map<goto_programt::const_targett, unsigned , const_target_hash>
160160 original_loop_number_map;
161161
162- // / Loop havoc instructions instrumneted during applying loop contracts.
162+ // / Loop havoc instructions instrumented during applying loop contracts.
163163 std::unordered_set<goto_programt::const_targett, const_target_hash>
164164 loop_havoc_set;
165165
You can’t perform that action at this time.
0 commit comments