@@ -80,18 +80,85 @@ predicate violatesCustomizedMoveOrCopyRequirements(AnalyzableClass c, string rea
8080}
8181
8282private predicate undeclaredMoveException ( AnalyzableClass c ) {
83- // A copy-enabled class may have an undeclared move constructor.
8483 isCopyEnabled ( c ) and
85- not c .copyAssignable ( ) and
86- not c .declaresMoveConstructor ( )
87- or
88- // A copy-assignable class may leave both move operations undeclared.
89- c .copyAssignable ( ) and
90- not c .declaresMoveConstructor ( ) and
91- not c .declaresMoveAssignmentOperator ( )
84+ (
85+ if c .copyAssignable ( )
86+ then
87+ // A copy-assignable class may have an undeclared move constructor.
88+ not c .declaresMoveConstructor ( ) and
89+ not c .declaresMoveAssignmentOperator ( )
90+ else
91+ // A copy-enabled class may have an undeclared move constructor.
92+ not c .declaresMoveConstructor ( )
93+ )
9294}
9395
9496predicate violatesCustomizedDestructorRequirements ( AnalyzableClass c , string reason ) {
97+ // This is is simplified from the exact MISRA spec in order to more closely enforce the general
98+ // idea that, if you customize the destructor, you generally need to customize the other special
99+ // member functions (e.g., ISO C++ Core Guidelines C.21 and C.22).
100+ //
101+ // The MISRA specification is subtle and arguably ambiguous. In our interpretation of the rules,
102+ // bullet 2 sentence 2 is deemed to only apply to move-only classes, otherwise it would conflict
103+ // with bullet 3 sentence 2. We do not strictly need to enforce any additional constraints on
104+ // bullet 3 sentence 2; all compliant copy-assignable classes must be copy-enabled.
105+ //
106+ // Here is a logical derivation that shows our logic is equivalent to the MISRA spec for classes
107+ // that fall into one of the compliant categories. For classes outside of those categories, we
108+ // essentially enforce C.21 and C.22 from the ISO C++ Core Guidelines.
109+ //
110+ // ```
111+ // -- For all rules, assume hasCustomizedDestructor(class).
112+ // isMoveOnly(class) -> hasCustomMoveConstructor(class)
113+ // isMoveOnly(class) &&
114+ // isMoveAssignable(class) -> hasCustomMoveConstructor(class) && hasCustomMoveAssignment(class)
115+ // isCopyEnabled(class) -> hasCustomCopyConstructor(class) && (hasCustomMoveConstructor(class)
116+ // || ~isMoveConstructorDeclared(class))
117+ // isCopyAssignable(class) -> hasCustomCopyAssignment(class)
118+ // && ( hasCustomMoveConstructor(class) && hasCustomMoveAssignment(class)
119+ // || ~isMoveConstructorDeclared(class) && ~isMoveAssignmentDeclared(class))
120+ //
121+ // -- Invert
122+ // hasCustomMoveConstructor(c) -> isMoveOnly(c)
123+ // || isMoveAssignable(c)
124+ // || (isCopyEnabled(c) && ~isMoveConstructorDeclared(c))
125+ // || (isCopyAssignable(c) && ~isMoveConstructorDeclared(c)
126+ // && ~isMoveAssignmentDeclared(c))
127+ //
128+ // hasCustomMoveAssignmentOperator(c) -> (isMoveOnly(class) && isMoveAssignable(c))
129+ // || isCopyAssignable(c) && ~isMoveConstructorDeclared(c)
130+ // && ~isMoveAssignmentDeclared(c))
131+ //
132+ // hasCustomCopyConstructor(c) -> isCopyEnabled(c)
133+ // || isCopyAssignable(c)
134+ //
135+ // hasCustomCopyAssignmentOperator(c) -> isCopyAssignable(c);
136+ //
137+ // -- Intermediate statements derived from table
138+ // isCopyAssignable(c) -> isMoveAssignable(c)
139+ // isMoveAssignable(c) -> isMoveConstructible(c)
140+ // isCopyEnabled(c) || isCopyAssignable(c) -> isCopyConstructible(c)
141+ // isMoveOnly(c) || isMoveAssignable(c) || isCopyEnabled(c) || isCopyAssignable(c) -> isMoveConstructible(c)
142+ //
143+ // -- Simplify
144+ // hasCustomMoveConstructor(c) -> isMoveConstructible(c)
145+ // || (isCopyEnabled(c) && ~isMoveConstructorDeclared(c))
146+ // || (isCopyAssignable(c) && ~isMoveConstructorDeclared(c) && ~isMoveAssignmentDeclared(c))
147+ // hasCustomMoveAssignmentOperator(c) -> isMoveAssignable(c)
148+ // || isCopyAssignable(c) && (~isMoveConstructorDeclared(c) && ~isMoveAssignmentDeclared(c))
149+ // hasCustomCopyConstructor(c) -> isCopyConstructible(c)
150+ // hasCustomCopyAssignmentOperator(c) -> isCopyAssignable(c)
151+ //
152+ // -- Extract exceptional cases
153+ // Exception1(class) :- isCopyEnabled(c) && ~isMoveConstructorDeclared(c)
154+ // Exception2(class) :- isCopyAssignable(c) && ~isMoveConstructorDeclared(c) && ~isMoveAssignmentDeclared(c)
155+ //
156+ // -- Simplify
157+ // hasCustomMoveConstructor(class) -> isMoveConstructible(c) || Exception1(c) || Exception2(c)
158+ // hasCustomMoveAssignmentOperator(c) -> isMoveAssignable(c) || Exception2(c)
159+ // hasCustomCopyConstructor(c) -> isCopyConstructible(c)
160+ // hasCustomCopyAssignmentOperator(c) -> isCopyAssignable(c);
161+ // ```
95162 c .isCustomized ( TDestructor ( ) ) and
96163 (
97164 c .moveConstructible ( ) and
0 commit comments