cannot unpack struct with non-byte aligned component

9 views
Skip to first unread message

pmo

unread,
Oct 7, 2019, 8:54:57 AM10/7/19
to CProver Support
Hello
On my program, just after the SSA conversion I have the message:
cannot unpack struct with non-byte aligned component 
width:1
followed by information of the concerned struct_type.
Can you explain to me why CBMC failed to handle this kind of constructions ?
Thanks

Michael Tautschnig

unread,
Oct 7, 2019, 8:57:29 AM10/7/19
to cprover...@googlegroups.com
Hello,

Would you be able to share the program you are working on? It may be possible to make improvements to CBMC to handle this case. For now CBMC has some limitations when doing byte-level operations on structures.

Best,
Michael

On 7 Oct 2019, at 13:54, pmo <patric...@gmail.com> wrote:


--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/088e9423-a43a-4812-9700-bb1c24d692b5%40googlegroups.com.

pmo

unread,
Oct 7, 2019, 9:47:24 AM10/7/19
to CProver Support
unfortunately I am not able to ...  I know it is hard to help without code :-/ 
I hoped this warning rang you a bell with a well-known problem. I will try to extract a pattern to share with you.
I can precise here is  the structure contains bit-fields of one  and if I add the the option --nondet-static, the message disappears.



Le lundi 7 octobre 2019 14:57:29 UTC+2, Michael Tautschnig a écrit :
Hello,

Would you be able to share the program you are working on? It may be possible to make improvements to CBMC to handle this case. For now CBMC has some limitations when doing byte-level operations on structures.

Best,
Michael

On 7 Oct 2019, at 13:54, pmo <patric...@gmail.com> wrote:


Hello
On my program, just after the SSA conversion I have the message:
cannot unpack struct with non-byte aligned component 
width:1
followed by information of the concerned struct_type.
Can you explain to me why CBMC failed to handle this kind of constructions ?
Thanks

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover...@googlegroups.com.

Michael Tautschnig

unread,
Oct 7, 2019, 9:57:59 AM10/7/19
to cprover...@googlegroups.com
If you could share details about the struct (in some anonymised form) and maybe create an example as small as possible that would be really helpful. I know where that error is raised, but I’m not sure I can easily craft an example that will trigger it.

Thanks,
Michael

On 7 Oct 2019, at 14:47, pmo <patric...@gmail.com> wrote:


To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/bcb879dc-f6f9-40f8-b1c8-4a09ee7cc25e%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages