@@ -24,15 +24,12 @@ KleeConstraintsPrinter::genConstraints(const std::string &name, const types::Typ
24
24
state = { name, name, paramType, state.endString };
25
25
genConstraintsForPointerOrArray (state);
26
26
break ;
27
- case TypeKind::STRUCT :
27
+ case TypeKind::STRUCT_LIKE :
28
28
genConstraintsForStruct (state);
29
29
break ;
30
30
case TypeKind::ENUM:
31
31
genConstraintsForEnum (state);
32
32
break ;
33
- case TypeKind::UNION:
34
- genConstraintsForUnion (state);
35
- break ;
36
33
default :
37
34
genConstraintsForPrimitive (state);
38
35
}
@@ -50,7 +47,7 @@ void KleeConstraintsPrinter::genConstraintsForPrimitive(const ConstraintsState &
50
47
if (!cons.empty ()) {
51
48
strFunctionCall (PrinterUtils::KLEE_PREFER_CEX, { state.paramName , cons });
52
49
} else {
53
- ss << TAB_N () << " // No constraints for " << state.curElement << NL;
50
+ ss << LINE_INDENT () << " // No constraints for " << state.curElement << NL;
54
51
}
55
52
}
56
53
@@ -67,38 +64,6 @@ void KleeConstraintsPrinter::genConstraintsForEnum(const ConstraintsState &state
67
64
strFunctionCall (PrinterUtils::KLEE_ASSUME, { _ss.str () });
68
65
}
69
66
70
- void KleeConstraintsPrinter::genConstraintsForUnion (const ConstraintsState &state) {
71
- UnionInfo curUnion = typesHandler->getUnionInfo (state.curType );
72
-
73
- for (const auto &field : curUnion.fields ) {
74
- std::string errorMessage = " Unrecognized field of type '" + field.type .typeName () +
75
- " ' in union '" + curUnion.name + " '." ;
76
- auto access = PrinterUtils::getFieldAccess (state.curElement , field);
77
- ConstraintsState newState = { state.paramName , access, field.type , false , state.depth + 1 };
78
- switch (typesHandler->getTypeKind (field.type )) {
79
- case TypeKind::PRIMITIVE:
80
- return genConstraintsForPrimitive (newState);
81
- case TypeKind::STRUCT:
82
- return genConstraintsForStruct (newState);
83
- case TypeKind::ARRAY:
84
- return genConstraintsForPointerOrArray (newState);
85
- case TypeKind::ENUM:
86
- return genConstraintsForEnum (newState);
87
- case TypeKind::UNION:
88
- return genConstraintsForUnion (newState);
89
- case TypeKind::OBJECT_POINTER:
90
- return genConstraintsForPointerInUnion (newState);
91
- case TypeKind::UNKNOWN:
92
- LOG_S (ERROR) << errorMessage;
93
- throw UnImplementedException (errorMessage);
94
- default :
95
- std::string message = " Missing case for this TypeKind in switch" ;
96
- LOG_S (ERROR) << message;
97
- throw NoSuchTypeException (message);
98
- }
99
- }
100
- }
101
-
102
67
void KleeConstraintsPrinter::genConstraintsForPointerOrArray (const ConstraintsState &state) {
103
68
auto sizes = state.curType .arraysSizes (types::PointerUsage::PARAMETER);
104
69
genConstraintsForMultiPointerOrArray (state, sizes);
@@ -119,21 +84,19 @@ void KleeConstraintsPrinter::genConstraintsForMultiPointerOrArray(const Constrai
119
84
TypesHandler::isCStringType (state.curType )) {
120
85
std::vector<std::string> charSizes (indexes.begin (), indexes.end () - 1 );
121
86
const auto charElement = constrMultiIndex (state.curElement , charSizes);
122
- ss << TAB_N () << " if (" << indexes.back () << PrinterUtils::EQ_OPERATOR << sizes.back () - 1 << " )" << LB ();
123
- ss << TAB_N () << PrinterUtils::KLEE_ASSUME << " (" << charElement << " [" << sizes.back () - 1 << " ]" << PrinterUtils::EQ_OPERATOR << " '\\ 0'" << " )" << SCNL;
124
- ss << TAB_N () << " break" << SCNL;
87
+ ss << LINE_INDENT () << " if (" << indexes.back () << PrinterUtils::EQ_OPERATOR << sizes.back () - 1 << " )" << LB ();
88
+ ss << LINE_INDENT () << PrinterUtils::KLEE_ASSUME << " (" << charElement << " [" << sizes.back () - 1 << " ]" << PrinterUtils::EQ_OPERATOR << " '\\ 0'" << " )" << SCNL;
89
+ ss << LINE_INDENT () << " break" << SCNL;
125
90
ss << RB ();
126
91
}
127
92
128
93
ConstraintsState newState = { state.paramName , element, baseType };
129
94
if (assignPointersToNull) {
130
95
genConstraintsForPointerInStruct (newState);
131
- } else if (typesHandler->isStruct (baseType)) {
96
+ } else if (typesHandler->isStructLike (baseType)) {
132
97
genConstraintsForStruct (newState);
133
98
} else if (typesHandler->isEnum (baseType)) {
134
99
genConstraintsForEnum (newState);
135
- } else if (typesHandler->isUnion (baseType)) {
136
- genConstraintsForUnion (newState);
137
100
} else {
138
101
newState = { state.paramName , element, baseType };
139
102
genConstraintsForPrimitive (newState);
@@ -148,37 +111,42 @@ void KleeConstraintsPrinter::genConstraintsForPointerInStruct(const ConstraintsS
148
111
149
112
void KleeConstraintsPrinter::genConstraintsForStruct (const ConstraintsState &state) {
150
113
StructInfo curStruct = typesHandler->getStructInfo (state.curType );
151
-
114
+ bool isStruct = curStruct. subType == SubType::Struct;
152
115
for (const auto &field : curStruct.fields ) {
153
116
std::string errorMessage = " Unrecognized field of type '" + field.type .typeName () +
154
117
" ' in struct '" + curStruct.name + " '." ;
155
118
auto access = PrinterUtils::getFieldAccess (state.curElement , field);
156
- ConstraintsState newState = { state.paramName , access, field.type , state.endString , state.depth + 1 };
119
+ ConstraintsState newState = { state.paramName ,
120
+ access,
121
+ field.type ,
122
+ isStruct ? state.endString : false ,
123
+ state.depth + 1 };
157
124
TypeKind kind = typesHandler->getTypeKind (field.type );
158
125
std::string stubFunctionName = PrinterUtils::getFunctionPointerAsStructFieldStubName (curStruct.name , field.name );
159
126
switch (kind) {
160
- case TypeKind::PRIMITIVE:
161
- genConstraintsForPrimitive (newState);
162
- break ;
163
- case TypeKind::STRUCT:
127
+ case TypeKind::STRUCT_LIKE:
164
128
genConstraintsForStruct (newState);
165
129
break ;
166
- case TypeKind::ARRAY:
167
- genConstraintsForPointerOrArray (newState);
168
- break ;
169
130
case TypeKind::ENUM:
170
131
genConstraintsForEnum (newState);
171
132
break ;
172
- case TypeKind::UNION:
173
- genConstraintsForUnion (newState);
133
+
134
+ case TypeKind::PRIMITIVE:
135
+ genConstraintsForPrimitive (newState);
136
+ break ;
137
+ case TypeKind::ARRAY:
138
+ genConstraintsForPointerOrArray (newState);
174
139
break ;
175
140
case TypeKind::OBJECT_POINTER:
176
141
if (types::TypesHandler::isArrayOfPointersToFunction (field.type )) {
177
- genStubForStructFunctionPointerArray (state.curElement , field.name , stubFunctionName);
142
+ genStubForStructFunctionPointerArray (state.curElement , field,
143
+ stubFunctionName);
178
144
}
179
145
break ;
180
146
case TypeKind::FUNCTION_POINTER:
181
- genStubForStructFunctionPointer (state.curElement , field.name , stubFunctionName);
147
+ genStubForStructFunctionPointer (state.curElement ,
148
+ field,
149
+ stubFunctionName);
182
150
break ;
183
151
case TypeKind::UNKNOWN:
184
152
throw UnImplementedException (errorMessage);
@@ -189,7 +157,6 @@ void KleeConstraintsPrinter::genConstraintsForStruct(const ConstraintsState &sta
189
157
}
190
158
}
191
159
}
192
-
193
160
std::string KleeConstraintsPrinter::cexConstraints (const std::string &name, const types::Type &type) {
194
161
std::stringstream ssCex;
195
162
if (!CollectionUtils::containsKey (TypesHandler::preferredConstraints (), type.baseType ())) {
@@ -205,11 +172,6 @@ std::string KleeConstraintsPrinter::cexConstraints(const std::string &name, cons
205
172
return ssCex.str ();
206
173
}
207
174
208
- void printer::KleeConstraintsPrinter::genConstraintsForPointerInUnion (
209
- const ConstraintsState &state) {
210
- strFunctionCall (PrinterUtils::KLEE_ASSUME, { state.curElement + PrinterUtils::EQ_OPERATOR + PrinterUtils::C_NULL });
211
- }
212
-
213
175
utbot::Language printer::KleeConstraintsPrinter::getLanguage () const {
214
176
return srcLanguage;
215
177
}
0 commit comments