Support atomic types

[schuessf]

This PR adds support for atomic types (_Atomic). To do so, I performed the following steps:

• First the keyword is replaced by some artificial GCC attribute (__attribute__((atomic))) for our parser not to crash.
• Whether we have an atomic type is then stored in the CType. This flag is only set explicitly in CPrimitive (based on the GCC attribute) and a CNamed is atomic iff the underlying type is atomic. All other types are currently not atomic. There can be actually an atomic pointer (see here), but we cannot parse the attribute properly at this location and thus don't support atomic pointers.
• We don't check for data-races on atomic types (see DataRaceChecker).
• We have to ensure that all operations on atomic variables are actually performed atomically. Therefore the translation of reads (see MemoryHandler::getReadCall), writes (see MemoryHandler::getWriteCall and CHandler::makeAssignment) and combined read-writes (e.g. ++, --, *=, ...) (see CHandler::makeAtomicAssignmentIfNecessary) was adapted.

[maul-esel]

We have to ensure that all operations on atomic variables are actually performed atomically. Our translation seems to ensure this for read and write operations (I am not 100% sure though).

I think we should ensure this by adding atomic statements in Boogie.

This would also solve the current unsoundness on this branch when using the setting --rcfgbuilder.only.consider.context.switches.at.boundaries.of.atomic.blocks true aka the "assume no data race"-LBE.

[schuessf]

I think we should ensure this by adding atomic statements in Boogie.

This would also solve the current unsoundness on this branch when using the setting --rcfgbuilder.only.consider.context.switches.at.boundaries.of.atomic.blocks true aka the "assume no data race"-LBE.

Thanks, that's a good point. With this settings, it actually makes a difference, whether we translate to a single Boogie statement st or atomic { st }.
So I guess, the only C expressions where the translation neeeds to be adapted for atomic types, are assignments (also sth. like +=) and reads (probably only for variables on the heap).

[maul-esel]

👍 Thanks for tackling this!

I've left some questions, and we should in particular also support other atomic operations such as += etc.

[maul-esel]

Three small questions/requests left, otherwise it looks good. Thanks again for taking care of this feature!