cannot unpack struct with non-byte aligned component

[pmo]

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]

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]

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]

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.