@@ -24,15 +24,12 @@ KleeConstraintsPrinter::genConstraints(const std::string &name, const types::Typ
2424            state = { name, name, paramType, state.endString  };
2525            genConstraintsForPointerOrArray (state);
2626            break ;
27-         case  TypeKind::STRUCT :
27+         case  TypeKind::STRUCT_LIKE :
2828            genConstraintsForStruct (state);
2929            break ;
3030        case  TypeKind::ENUM:
3131            genConstraintsForEnum (state);
3232            break ;
33-         case  TypeKind::UNION:
34-             genConstraintsForUnion (state);
35-             break ;
3633        default :
3734            genConstraintsForPrimitive (state);
3835    }
@@ -50,7 +47,7 @@ void KleeConstraintsPrinter::genConstraintsForPrimitive(const ConstraintsState &
5047    if  (!cons.empty ()) {
5148        strFunctionCall (PrinterUtils::KLEE_PREFER_CEX, { state.paramName , cons });
5249    } else  {
53-         ss << TAB_N () << " // No constraints for " curElement  << NL;
50+         ss << LINE_INDENT () << " // No constraints for " curElement  << NL;
5451    }
5552}
5653
@@ -67,38 +64,6 @@ void KleeConstraintsPrinter::genConstraintsForEnum(const ConstraintsState &state
6764    strFunctionCall (PrinterUtils::KLEE_ASSUME, { _ss.str () });
6865}
6966
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 '" type .typeName () +
75-                                    " ' in union '" 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- 
10267void  KleeConstraintsPrinter::genConstraintsForPointerOrArray (const  ConstraintsState &state) {
10368    auto  sizes = state.curType .arraysSizes (types::PointerUsage::PARAMETER);
10469    genConstraintsForMultiPointerOrArray (state, sizes);
@@ -119,21 +84,19 @@ void KleeConstraintsPrinter::genConstraintsForMultiPointerOrArray(const Constrai
11984        TypesHandler::isCStringType (state.curType )) {
12085        std::vector<std::string> charSizes (indexes.begin (), indexes.end () - 1 );
12186        const  auto  charElement = constrMultiIndex (state.curElement , charSizes);
122-         ss << TAB_N () << " if (" back () << PrinterUtils::EQ_OPERATOR << sizes.back () - 1  << " )" LB ();
123-         ss << TAB_N () << PrinterUtils::KLEE_ASSUME << " (" " [" back () - 1  << " ]" " '\\ 0'" " )" 
124-         ss << TAB_N () << " break" 
87+         ss << LINE_INDENT () << " if (" back () << PrinterUtils::EQ_OPERATOR << sizes.back () - 1  << " )" LB ();
88+         ss << LINE_INDENT () << PrinterUtils::KLEE_ASSUME << " (" " [" back () - 1  << " ]" " '\\ 0'" " )" 
89+         ss << LINE_INDENT () << " break" 
12590        ss << RB ();
12691    }
12792
12893    ConstraintsState newState = { state.paramName , element, baseType };
12994    if  (assignPointersToNull) {
13095        genConstraintsForPointerInStruct (newState);
131-     } else  if  (typesHandler->isStruct (baseType)) {
96+     } else  if  (typesHandler->isStructLike (baseType)) {
13297        genConstraintsForStruct (newState);
13398    } else  if  (typesHandler->isEnum (baseType)) {
13499        genConstraintsForEnum (newState);
135-     } else  if  (typesHandler->isUnion (baseType)) {
136-         genConstraintsForUnion (newState);
137100    } else  {
138101        newState = { state.paramName , element, baseType };
139102        genConstraintsForPrimitive (newState);
@@ -148,37 +111,42 @@ void KleeConstraintsPrinter::genConstraintsForPointerInStruct(const ConstraintsS
148111
149112void  KleeConstraintsPrinter::genConstraintsForStruct (const  ConstraintsState &state) {
150113    StructInfo curStruct = typesHandler->getStructInfo (state.curType );
151- 
114+      bool  isStruct = curStruct. subType  == SubType::Struct; 
152115    for  (const  auto  &field : curStruct.fields ) {
153116        std::string errorMessage = " Unrecognized field of type '" type .typeName () +
154117                                   " ' in struct '" name  + " '." 
155118        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  };
157124        TypeKind kind = typesHandler->getTypeKind (field.type );
158125        std::string stubFunctionName = PrinterUtils::getFunctionPointerAsStructFieldStubName (curStruct.name , field.name );
159126        switch  (kind) {
160-         case  TypeKind::PRIMITIVE:
161-             genConstraintsForPrimitive (newState);
162-             break ;
163-         case  TypeKind::STRUCT:
127+         case  TypeKind::STRUCT_LIKE:
164128            genConstraintsForStruct (newState);
165129            break ;
166-         case  TypeKind::ARRAY:
167-             genConstraintsForPointerOrArray (newState);
168-             break ;
169130        case  TypeKind::ENUM:
170131            genConstraintsForEnum (newState);
171132            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);
174139            break ;
175140        case  TypeKind::OBJECT_POINTER:
176141            if  (types::TypesHandler::isArrayOfPointersToFunction (field.type )) {
177-                 genStubForStructFunctionPointerArray (state.curElement , field.name , stubFunctionName);
142+                 genStubForStructFunctionPointerArray (state.curElement , field,
143+                                                      stubFunctionName);
178144            }
179145            break ;
180146        case  TypeKind::FUNCTION_POINTER:
181-             genStubForStructFunctionPointer (state.curElement , field.name , stubFunctionName);
147+             genStubForStructFunctionPointer (state.curElement ,
148+                                             field,
149+                                             stubFunctionName);
182150            break ;
183151        case  TypeKind::UNKNOWN:
184152            throw  UnImplementedException (errorMessage);
@@ -189,7 +157,6 @@ void KleeConstraintsPrinter::genConstraintsForStruct(const ConstraintsState &sta
189157        }
190158    }
191159}
192- 
193160std::string KleeConstraintsPrinter::cexConstraints (const  std::string &name, const  types::Type &type) {
194161    std::stringstream ssCex;
195162    if  (!CollectionUtils::containsKey (TypesHandler::preferredConstraints (), type.baseType ())) {
@@ -205,11 +172,6 @@ std::string KleeConstraintsPrinter::cexConstraints(const std::string &name, cons
205172    return  ssCex.str ();
206173}
207174
208- void  printer::KleeConstraintsPrinter::genConstraintsForPointerInUnion (
209-     const  ConstraintsState &state) {
210-     strFunctionCall (PrinterUtils::KLEE_ASSUME, { state.curElement  + PrinterUtils::EQ_OPERATOR + PrinterUtils::C_NULL });
211- }
212- 
213175utbot::Language printer::KleeConstraintsPrinter::getLanguage () const  {
214176    return  srcLanguage;
215177}
0 commit comments