@@ -44,6 +44,9 @@ struct ModelCheckerContracts
44
44
return has (_source) && contracts.at (_source).count (_contract);
45
45
}
46
46
47
+ bool operator !=(ModelCheckerContracts const & _other) const noexcept { return !(*this == _other); }
48
+ bool operator ==(ModelCheckerContracts const & _other) const noexcept { return contracts == _other.contracts ; }
49
+
47
50
// / Represents which contracts should be analyzed by the SMTChecker
48
51
// / as the most derived.
49
52
// / The key is the source file. If the map is empty, all sources must be analyzed.
@@ -79,6 +82,9 @@ struct ModelCheckerEngine
79
82
return engineMap.at (_engine);
80
83
return {};
81
84
}
85
+
86
+ bool operator !=(ModelCheckerEngine const & _other) const noexcept { return !(*this == _other); }
87
+ bool operator ==(ModelCheckerEngine const & _other) const noexcept { return bmc == _other.bmc && chc == _other.chc ; }
82
88
};
83
89
84
90
enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds };
@@ -97,6 +103,9 @@ struct ModelCheckerTargets
97
103
98
104
static std::map<std::string, VerificationTargetType> const targetStrings;
99
105
106
+ bool operator !=(ModelCheckerTargets const & _other) const noexcept { return !(*this == _other); }
107
+ bool operator ==(ModelCheckerTargets const & _other) const noexcept { return targets == _other.targets ; }
108
+
100
109
std::set<VerificationTargetType> targets;
101
110
};
102
111
@@ -106,6 +115,16 @@ struct ModelCheckerSettings
106
115
ModelCheckerEngine engine = ModelCheckerEngine::None();
107
116
ModelCheckerTargets targets = ModelCheckerTargets::Default();
108
117
std::optional<unsigned > timeout;
118
+
119
+ bool operator !=(ModelCheckerSettings const & _other) const noexcept { return !(*this == _other); }
120
+ bool operator ==(ModelCheckerSettings const & _other) const noexcept
121
+ {
122
+ return
123
+ contracts == _other.contracts &&
124
+ engine == _other.engine &&
125
+ targets == _other.targets &&
126
+ timeout == _other.timeout ;
127
+ }
109
128
};
110
129
111
130
}
0 commit comments