diff --git a/trunk/examples/programs/regression/c/struct-anonymous-01.c b/trunk/examples/programs/regression/c/struct-anonymous-01.c new file mode 100644 index 00000000000..6b414736274 --- /dev/null +++ b/trunk/examples/programs/regression/c/struct-anonymous-01.c @@ -0,0 +1,22 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with an anonymous struct in a named (outer) struct + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +struct foo { + struct { + int a; + }; +}; + +int main() +{ + struct foo f; + f.a = 10; + int a = f.a; + //@ assert (a == 10); + return f.a; +} diff --git a/trunk/examples/programs/regression/c/struct-anonymous-02.c b/trunk/examples/programs/regression/c/struct-anonymous-02.c new file mode 100644 index 00000000000..07ee41bb655 --- /dev/null +++ b/trunk/examples/programs/regression/c/struct-anonymous-02.c @@ -0,0 +1,28 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with an anonymous struct and variables in a named (outer) struct + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +struct foo { + int a; + struct { + int b; + }; + int c; +}; + +int main() +{ + struct foo f; + f.a = 10; + f.b = 20; + f.c = 30; + int a = f.a; + int b = f.b; + int c = f.c; + //@ assert (a == 10 && b == 20 && c == 30); + return f.a + f.b + f.c; +} diff --git a/trunk/examples/programs/regression/c/struct-anonymous-03.c b/trunk/examples/programs/regression/c/struct-anonymous-03.c new file mode 100644 index 00000000000..767cc90647d --- /dev/null +++ b/trunk/examples/programs/regression/c/struct-anonymous-03.c @@ -0,0 +1,27 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with nested anonymous structs in a named (outer) struct + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +struct foo { + struct { + int a; + struct { + int b; + }; + }; +}; + +int main() +{ + struct foo f; + f.a = 10; + f.b = 20; + int a = f.a; + int b = f.b; + //@ assert (a == 10 && b == 20); + return f.a + f.b; +} diff --git a/trunk/examples/programs/regression/c/struct-anonymous-04.c b/trunk/examples/programs/regression/c/struct-anonymous-04.c new file mode 100644 index 00000000000..371add9edb9 --- /dev/null +++ b/trunk/examples/programs/regression/c/struct-anonymous-04.c @@ -0,0 +1,28 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with an anonymous struct in an outer struct as part of a typedef + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +typedef struct { + int a; + struct { + int b; + }; + int c; +} foo_t; + +int main() +{ + foo_t f; + f.a = 10; + f.b = 20; + f.c = 30; + int a = f.a; + int b = f.b; + int c = f.c; + //@ assert (a == 10 && b == 20 && c == 30); + return f.a + f.b + f.c; +} diff --git a/trunk/examples/programs/regression/c/struct-anonymous-05.c b/trunk/examples/programs/regression/c/struct-anonymous-05.c new file mode 100644 index 00000000000..fb01a4fbd37 --- /dev/null +++ b/trunk/examples/programs/regression/c/struct-anonymous-05.c @@ -0,0 +1,33 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with anonymous structs in an outer struct as part of a typedef + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 14.11.2025 + *---------------------------------------------------------------------------*/ + +typedef struct { + int a; + struct { + int b; + }; + int c; + struct { + int d; + }; +} foo_t; + +int main() +{ + foo_t f; + f.a = 10; + f.b = 20; + f.c = 30; + f.d = 40; + int a = f.a; + int b = f.b; + int c = f.c; + int d = f.d; + //@ assert (a == 10 && b == 20 && c == 30 && d == 40); + return f.a + f.b + f.c + f.d; +} diff --git a/trunk/examples/programs/regression/c/struct-anonymous-06.c b/trunk/examples/programs/regression/c/struct-anonymous-06.c new file mode 100644 index 00000000000..6738bdbcc4d --- /dev/null +++ b/trunk/examples/programs/regression/c/struct-anonymous-06.c @@ -0,0 +1,35 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with (nested) anonymous structs in an outer struct as part of a typedef + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 14.11.2025 + *---------------------------------------------------------------------------*/ + +typedef struct { + int a; + struct { + int b; + }; + struct { + struct { + int c; + }; + int d; + }; +} foo_t; + +int main() +{ + foo_t f; + f.a = 10; + f.b = 20; + f.c = 30; + f.d = 40; + int a = f.a; + int b = f.b; + int c = f.c; + int d = f.d; + //@ assert (a == 10 && b == 20 && c == 30 && d == 40); + return f.a + f.b + f.c + f.d; +} diff --git a/trunk/examples/programs/regression/c/union-anonymous-01.c b/trunk/examples/programs/regression/c/union-anonymous-01.c new file mode 100644 index 00000000000..16c9fa717b1 --- /dev/null +++ b/trunk/examples/programs/regression/c/union-anonymous-01.c @@ -0,0 +1,25 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with an anonymous union in a named (outer) struct + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +struct foo { + union { + int a; + int b; + }; +}; + +int main() +{ + struct foo f; + f.a = 10; + f.b = 20; + int a = f.a; + int b = f.b; + //@ assert (a == 20 && b == 20); + return f.a + f.b; +} diff --git a/trunk/examples/programs/regression/c/union-anonymous-02.c b/trunk/examples/programs/regression/c/union-anonymous-02.c new file mode 100644 index 00000000000..56fdda65f1d --- /dev/null +++ b/trunk/examples/programs/regression/c/union-anonymous-02.c @@ -0,0 +1,31 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with an anonymous union and variables in a named (outer) struct + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +struct foo { + int a; + union { + int b; + int c; + }; + int d; +}; + +int main() +{ + struct foo f; + f.a = 10; + f.b = 20; + f.c = 30; + f.d = 40; + int a = f.a; + int b = f.b; + int c = f.c; + int d = f.d; + //@ assert (a == 10 && b == 30 && c == 30 && d == 40); + return f.a + f.b + f.c + f.d; +} diff --git a/trunk/examples/programs/regression/c/union-anonymous-03.c b/trunk/examples/programs/regression/c/union-anonymous-03.c new file mode 100644 index 00000000000..2a953ec605b --- /dev/null +++ b/trunk/examples/programs/regression/c/union-anonymous-03.c @@ -0,0 +1,30 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with nested anonymous unions in a named (outer) struct + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +struct foo { + union { + int a; + union { + int b; + int c; + }; + }; +}; + +int main() +{ + struct foo f; + f.a = 10; + f.b = 20; + f.c = 30; + int a = f.a; + int b = f.b; + int c = f.c; + //@ assert (a == 30 && b == 30 && c == 30); + return f.a + f.b + f.c; +} diff --git a/trunk/examples/programs/regression/c/union-anonymous-04.c b/trunk/examples/programs/regression/c/union-anonymous-04.c new file mode 100644 index 00000000000..6de92a3e53d --- /dev/null +++ b/trunk/examples/programs/regression/c/union-anonymous-04.c @@ -0,0 +1,28 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with an anonymous union in an outer union as part of a typedef + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +typedef union { + int a; + union { + int b; + int c; + }; +} foo_t; + +int main() +{ + foo_t f; + f.a = 10; + f.b = 20; + f.c = 30; + int a = f.a; + int b = f.b; + int c = f.c; + //@ assert (a == 30 && b == 30 && c == 30); + return f.a + f.b + f.c; +} diff --git a/trunk/examples/programs/regression/c/union-anonymous-05.c b/trunk/examples/programs/regression/c/union-anonymous-05.c new file mode 100644 index 00000000000..a1f5afb6985 --- /dev/null +++ b/trunk/examples/programs/regression/c/union-anonymous-05.c @@ -0,0 +1,33 @@ +/* #Safe + *----------------------------------------------------------------------------- + * Example with an anonymous struct in an outer union as part of a typedef + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 13.11.2025 + *---------------------------------------------------------------------------*/ + +typedef union { + struct { + unsigned int a : 8; + unsigned int b : 8; + unsigned int c : 8; + unsigned int d : 8; + }; + unsigned int all; +} foo_t; + +int main() +{ + foo_t f; + f.a = 10; + f.b = 20; + f.c = 30; + f.d = 40; + int a = f.a; + int b = f.b; + int c = f.c; + int d = f.d; + int all = f.all; + assert (a == 10 && b == 20 && c == 30 && d == 40 && all == 673059850); + return f.all; +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java index 4d6790e85cf..299c5277637 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java @@ -2389,7 +2389,7 @@ public Result visit(final IDispatcher main, final IASTSimpleDeclaration node) { final List noSkipIntermediateResult = intermediateResults.stream().filter(a -> !(a instanceof SkipResult)).collect(Collectors.toList()); if (noSkipIntermediateResult.isEmpty()) { - return new SkipResult(); + return typeResult; } final Result first = noSkipIntermediateResult.get(0); if (noSkipIntermediateResult.size() == 1) { @@ -3630,7 +3630,7 @@ private void processTUchild(final IDispatcher main, final ArrayList mStaticObjectsHandler.addGlobalVariableDeclaration((VariableDeclaration) boogieDecl, cd, null); } } else { - if (childRes instanceof SkipResult || childRes.getNode() == null) { + if (childRes instanceof SkipResult || childRes instanceof TypesResult || childRes.getNode() == null) { return; } assert childRes.getClass() == Result.class; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java index cc1cc1907f2..4562c3d7b74 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java @@ -35,6 +35,7 @@ import java.math.BigInteger; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.HashMap; import java.util.LinkedHashSet; @@ -430,6 +431,16 @@ public Result visit(final IDispatcher main, final IASTCompositeTypeSpecifier nod bitFieldWidths.add(declaration.getBitfieldSize()); } } else if (r instanceof SkipResult) { // skip ;) + } else if (r instanceof final TypesResult tr && tr.getCType() instanceof final CStructOrUnion su) { + if (su.isAnonymous()) { + // Flat unnamed (anonymous) struct or union by adding the field(s) to to the parent struct or union. + fNames.addAll(su.getFieldNames()); + fTypes.addAll(Arrays.asList(su.getFieldTypes())); + bitFieldWidths.addAll(su.getBitFieldWidths()); + } else { + final String msg = "Non-anoymous struct or union declaration cannot be flatten!"; + throw new UnsupportedSyntaxException(loc, msg); + } } else { final String msg = "Unexpected syntax in struct declaration!"; throw new UnsupportedSyntaxException(loc, msg); @@ -438,16 +449,10 @@ public Result visit(final IDispatcher main, final IASTCompositeTypeSpecifier nod final String cId = node.getName().toString(); final String rslvName = mSymboltable.applyMultiparseRenaming(node.getContainingFilename(), cId); - final StructOrUnion isStructOrUnion; - if (node.getKey() == IASTCompositeTypeSpecifier.k_struct) { - isStructOrUnion = StructOrUnion.STRUCT; - } else if (node.getKey() == IASTCompositeTypeSpecifier.k_union) { - isStructOrUnion = StructOrUnion.UNION; - } else { - throw new UnsupportedOperationException(); - } + final StructOrUnion isStructOrUnion = CStructOrUnion.getStructOrUnionFromAstNode(node); + final boolean isAnonymous = CStructOrUnion.isAnonymousFromAstNode(node); - final String identifier = CStructOrUnion.getPrefix(isStructOrUnion) + rslvName; + final String identifier = CStructOrUnion.getPrefix(isStructOrUnion, isAnonymous) + rslvName; if (mIncompleteCStructOrUnionObjects.containsKey(rslvName)) { final CStructOrUnion structOrUnion = mIncompleteCStructOrUnionObjects.get(rslvName); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CStructOrUnion.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CStructOrUnion.java index d6aa04d8850..9dd93349d93 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CStructOrUnion.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CStructOrUnion.java @@ -34,6 +34,8 @@ import java.util.List; import java.util.Objects; +import org.eclipse.cdt.core.dom.ast.IASTCompositeTypeSpecifier; + /** * Struct / Union type (see C11 6.2.5.20.2/3) * @@ -47,6 +49,9 @@ public enum StructOrUnion { } private final StructOrUnion mIsStructOrUnion; + + private final boolean mIsAnonymous; + /** * Field names. */ @@ -83,20 +88,32 @@ public CStructOrUnion(final StructOrUnion isStructOrUnion, final String name, fi assert name != null; assert fNames.length == bitFieldWidths.size(); mIsStructOrUnion = isStructOrUnion; + mIsAnonymous = name.isEmpty() ? true : false; mFieldNames = fNames; mFieldTypes = fTypes; mBitFieldWidths = Collections.unmodifiableList(bitFieldWidths); - mStructName = Objects.requireNonNull(name); + mStructName = isAnonymous() ? Objects.requireNonNull(name) : new String(); mIsComplete = true; } public CStructOrUnion(final StructOrUnion isStructOrUnion, final String name) { - assert name != null && !name.isEmpty(); + assert name != null; + mIsStructOrUnion = isStructOrUnion; + mIsAnonymous = name.isEmpty() ? true : false; + mFieldNames = new String[0]; + mFieldTypes = new ICType[0]; + mBitFieldWidths = Collections.emptyList(); + mStructName = isAnonymous() ? Objects.requireNonNull(name) : new String(); + mIsComplete = false; + } + + public CStructOrUnion(final StructOrUnion isStructOrUnion) { mIsStructOrUnion = isStructOrUnion; + mIsAnonymous = true; mFieldNames = new String[0]; mFieldTypes = new ICType[0]; mBitFieldWidths = Collections.emptyList(); - mStructName = Objects.requireNonNull(name); + mStructName = null; mIsComplete = false; } @@ -157,17 +174,23 @@ public StructOrUnion isStructOrUnion() { return mIsStructOrUnion; } + public boolean isAnonymous() { + return mIsAnonymous; + } + @Override public String toString() { - final String structOrUnionPrefix = getPrefix(mIsStructOrUnion); + final String structOrUnionPrefix = getPrefix(isStructOrUnion(), isAnonymous()); if (isIncomplete()) { return structOrUnionPrefix + "~incomplete~" + getName(); } final StringBuilder sb = new StringBuilder(); sb.append(structOrUnionPrefix); - sb.append('~'); - sb.append(getName()); + if (!isAnonymous()) { + sb.append('~'); + sb.append(getName()); + } for (int i = 0; i < getFieldCount(); i++) { sb.append("?"); sb.append(mFieldNames[i]); @@ -207,6 +230,10 @@ public void complete(final List memberNames, final List memberTy mIsComplete = true; } + public List getFieldNames() { + return Arrays.asList(mFieldNames); + } + public List getBitFieldWidths() { return mBitFieldWidths; } @@ -217,7 +244,7 @@ public List getBitFieldWidths() { */ public int getBitfieldWidth(final String id) { assert !isIncomplete() : "Cannot get a field type in an incomplete struct type."; - final int idx = Arrays.asList(mFieldNames).indexOf(id); + final int idx = getFieldNames().indexOf(id); if (idx < 0) { throw new IllegalArgumentException("Field not in struct: " + id); } @@ -246,13 +273,28 @@ public boolean equals(final Object o) { return this == o; } - public static String getPrefix(final StructOrUnion structOrUnion) { + public static String getPrefix(final StructOrUnion structOrUnion, final boolean anonymous) { + final String unnamed = anonymous ? "ANONYMOUS~" : new String(); return switch (structOrUnion) { - case STRUCT -> "STRUCT~"; - case UNION -> "UNION~"; + case STRUCT -> "STRUCT~" + unnamed; + case UNION -> "UNION~" + unnamed; }; } + public static StructOrUnion getStructOrUnionFromAstNode(final IASTCompositeTypeSpecifier node) { + return switch (node.getKey()) { + case IASTCompositeTypeSpecifier.k_struct -> StructOrUnion.STRUCT; + case IASTCompositeTypeSpecifier.k_union -> StructOrUnion.UNION; + default -> throw new UnsupportedOperationException(); + }; + } + + public static boolean isAnonymousFromAstNode(final IASTCompositeTypeSpecifier node) { + assert node.getKey() == IASTCompositeTypeSpecifier.k_struct + || node.getKey() == IASTCompositeTypeSpecifier.k_union; + return node.getName().toString().isEmpty(); + } + @Override public boolean isAtomic() { return false;