CONTRACTS: class that applies loop contract transformations

diffblue · Apr 20, 2023 · 6143154 · 6143154
1 parent 75b519a
commit 6143154
Show file tree

Hide file tree

Showing 3 changed files with 1,087 additions and 0 deletions.
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
@@ -26,6 +26,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_root_object.cpp \
       contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp \
       contracts/dynamic-frames/dfcc_cfg_info.cpp \
+      contracts/dynamic-frames/dfcc_instrument_loop.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \