Support for C11 #24
Support for C11 #24
Conversation
Gcc-10 defaults to -fno-common, which gives an error if there are multiple declarations of the same global variable without the extern storage class specifier.
It does and one would ideally like to compile it away in CIL such that Goblint does not need to handle it. |
There was a problem hiding this comment.
Is there some reason this PR hasn't been merged yet?
According to @vesalvojdani newer Linux kernels use _Generic so it would be good to support it, especially since those are fully type-based, so shouldn't be a problem to do in CIL.
| let typ = | ||
| let rec get_typ lst = match lst with | ||
| | (TDefault, e) :: rest -> default_typ := typeOf e; get_typ rest | ||
| | (t, e) :: rest -> if t = exp_typ then typeOf e else get_typ rest |
There was a problem hiding this comment.
This structural polymorphic type comparison is probably incorrect. The standard calls for lvalue conversions on expr and then the comparison is by compatible types.
| make_cil_list lst [] | ||
| in | ||
| let exp_typ = typeOf exp in | ||
| let default_typ = ref voidType in |
There was a problem hiding this comment.
This should probably be ref None instead, unless somewhere the standard says default should be equivalent to void.
| in | ||
| get_typ cil_list | ||
| in | ||
| finishExp empty (Generic(exp, (cil_list))) typ |
There was a problem hiding this comment.
Since the type switch case is already resolved there just to return the correct type, there's no need to keep the Generic expression, but we could also just return the expression for that particular case. Then Generic doesn't have to exist in CIL AST at all (it's resolved by type during the conversion here). Moreover, Goblint doesn't have to do anything extra to handle Generic everywhere as the logic would always be the same.
There was a problem hiding this comment.
yes, generic should be compiled away!
Because no-one has added C11 support to Goblint yet (C11 threading, AST changes if required, handling of thread-local variables, ...). We wanted to bundle these into a BSc thesis at some point, but I guess we can do a minimal support first. |
|
I added a TODO list into the original PR description with a list of things we have already cherry-picked out of here. That should help us know when at one point we have cherry-picked everything from here. |
|
Is this useful in it's current (out-of-sync) state? Or should it be closed for now? |
Adds support for C11 to Goblint (see #13).
This is work done by @coslu for his Bachelor's thesis.
Cherry-picked
_Noreturn#58char16_t, andchar32_t(part of C99/C11) #80