CBMC
loop_contract_config.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Config for loop contract
4 
5 Author: Qinheping Hu
6 
7 Date: 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 {
20 public:
21  // Apply loop contracts.
22  bool apply_loop_contracts = false;
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 
42  bool operator==(const loop_contract_configt &rhs) const
43  {
47  }
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.
std::string to_string() const
bool operator==(const loop_contract_configt &rhs) const
bool operator!=(const loop_contract_configt &rhs) const