CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/loop_contract_config.h Source File

CBMC
Loading...
Searching...
No Matches
loop_contract_config.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Config for loop contract
4
5Author: Qinheping Hu
6
7Date: June 2024
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_LOOP_CONTRACT_CONFIG_H
15#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_LOOP_CONTRACT_CONFIG_H
16
19{
20public:
21 // Apply loop contracts.
23
24 // Unwind transformed loops after applying loop contracts or not.
26
27 // Check if loop contracts are all side-effect free.
28 bool check_side_effect = true;
29
30 std::string to_string() const
31{
32 std::string result;
33 result += "Apply loop contracts: ";
34 result += (apply_loop_contracts ? "yes\n" : "no\n");
35 result += "Unwind transformed loops: ";
36 result += (unwind_transformed_loops ? "yes\n" : "no\n");
37 result += "Check side effect of loop contracts: ";
38 result += (check_side_effect ? "yes\n" : "no\n");
39 return result;
40 }
41
48
49 bool operator!=(const loop_contract_configt &rhs) const
50{
51 return !(this == &rhs);
52 }
53};
54
55#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_LOOP_CONTRACT_CONFIG_H
Loop contract configurations.
bool unwind_transformed_loops
bool apply_loop_contracts
std::string to_string() const
bool operator==(const loop_contract_configt &rhs) const
bool operator!=(const loop_contract_configt &rhs) const
bool check_side_effect

AltStyle によって変換されたページ (->オリジナル) /