crash in goto-harness (nested struct with padding)

Hi, with this C fragment I see a crash in goto-harness:

typedef struct
{
  char a;
  int b;
} wibble;

typedef struct
{
  wibble c;
} outer;

outer g;

int main(void)
{
  return g.c.a;
}

When run like so:

goto-cc foo.c && goto-harness a.out wibble.c --harness-type call-function --function main --harness-function-name potato

We get:

--- begin invariant violation report ---
Invariant check failed
File: dump_c.cpp:630 function: convert_compound
Condition: false
Reason: Unreachable
Backtrace:
<...>

Version: CBMC 6.10.0 (compiled from source)

I cannot tell if this is legit, but the following change prevents the crash in goto-harness.

diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 89e785ca3f..5e03995309 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -1625,7 +1625,7 @@ static expr2c_configurationt expr2c_configuration()
   // future TODO: with C++20 we can actually use designated initializers as
   // commented out below
   static expr2c_configurationt configuration{
-    /* .include_struct_padding_components = */ true,
+    /* .include_struct_padding_components = */ false,
     /* .print_struct_body_in_type = */ true,
     /* .include_array_size = */ true,
     /* .true_string = */ "1",

Navigation Menu

Repository navigation

crash in goto-harness (nested struct with padding) #9153

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

crash in goto-harness (nested struct with padding) #9153

Description

Activity

lemmy commented on Aug 5, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions