We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 677f579 commit 56bf6c1Copy full SHA for 56bf6c1
src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h
@@ -8,6 +8,8 @@ Date: February 2023
8
\*******************************************************************/
9
10
/// \file
11
+/// Translates assigns and frees clauses of a function contract or
12
+/// loop contract into goto programs that build write sets or havoc write sets.
13
14
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
15
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
0 commit comments