[bug, CN] Unsupported union types

[podhrmic]

CN verification fails with:

/root/.opam/default/lib/cerberus/runtime/libc/include/stdio.h:10:15: error: unsupported union types
typedef union _G_fpos64_t {
              ^~~~~~~~~~~ 

See this CI job for details, the source file is actuator.c, but we see similar error happening with mutiple different input files.

[podhrmic]

This is a blocker for us now - see the PR linked above.

[septract]

[Deleted as I totally misunderstood the issue]

[podhrmic]

I know @peterohanley had some workaround for this, but looks like the new magic syntax has introduced some regression. This CI job was passing before I switched the magic syntax,

[septract]

Can you isolate the regression? Looking at the diff, the new syntax should not have changed any CN behaviour.

[podhrmic]

Good idea. This commit introduced the new special syntax. Can you have a look and see if those changes are sensible?

The previous commit had the CN proof for actuator.c passing.

This commit runs the proofs in the CI again

[septract]

Huh yes, that is weird. The minimal failing case is just a file that includes stdio.h:

#include <stdio.h>

Gives the following result:

% cn test.c 
/Users/miked/.opam/default/lib/cerberus/runtime/libc/include/stdio.h:10:15: error: unsupported union types
typedef union _G_fpos64_t {
              ^~~~~~~~~~~ 

@cp526 Can you look at this? As Michal says, this is a blocker for us.

(A hypothesis: perhaps there's something important up the dependency tree which is now being skipped because it's wrapped in standard CN comments)

[dc-mak]

I'm not sure I follow what's going on. Union types are not supported (yet, in progress) and #include <stdio.h> would not have been either, before or after the --magic-comment-char-dollar change.

[dc-mak]

To double check, I just ran the MWE #include <stdio.h> before (c6075bb6886b679dd4578b77617ae15ca42ddbde) and after (60d013553e414522e55994b8f6cf55fa746f47bf) the change, and got the same error both times.

Is this the correct repro procedure? I wasn't able to repro behaviour.

10:25 ➜  src git:(310e48a) cn -I include --include=include/wars.h components/actuator.c
[1/5]: actuate_devices
[2/5]: c_NDEV
[3/5]: c_NVOTE_LOGIC
[4/5]: c_NTRIP
[5/5]: c_NINSTR
10:26 ➜  src git:(310e48a) tig main
10:26 ➜  src git:(310e48a) gco 952fd147e3ee5c52af1b4a020b63d854964abb15
Previous HEAD position was 310e48a CI: run CN from a makefile
HEAD is now at 952fd14 Add Frama-C specs, and switch the CN syntax to /*$
10:26 ➜  src git:(952fd14) cn --magic-comment-char-dollar -I include --include=include/wars.h components/actuator.c
[1/5]: actuate_devices
[2/5]: c_NDEV
[3/5]: c_NVOTE_LOGIC
[4/5]: c_NTRIP
[5/5]: c_NINSTR
10:27 ➜  src git:(952fd14) pwd
/home/dhruv/VERSE-OpenSUT/components/mission_protection_system/src

[septract]

Okay, I think I'm finally less confused. I think the cause is this commit which sets the PLATFORM_HOST macro. This has the effect of including <stdio.h> here. This isn't supported in CN, and has never been. So this change breaks the CN build for the OpenSUT

Conclusion: this is not a CN bug and nothing to do with the new syntax. If we want <stdio.h> in the OpenSUT we will need CN to support unions.

@dc-mak I think you can close this.

[bcpierce00]

If we want in the OpenSUT we will need CN to support unions.

I'd love to hear some technical discussion (maybe in a call next week?) of what's involved in doing this...

[podhrmic]

@septract thanks for pointing this out!

I have a workaround in #59, but being able to use <stdio.h> seems pretty important in general.

Where can I find a list of supported includes, such that I can properly gate the OpenSUT includes?

[kmemarian]

I noticed that the union type wasn't actually needed for the use we have of fpos_t in the current state of our libc, so I removed it in 4befd44. And there are no use of unions in headers I believe.