Add parsing support for 'asm goto'

[emiljapelt]

I am working on a project which utilizes goblint-cil, however I have notice a few short comings, which this attempts to fix:

• The 'asm goto' support should to my understanding be following the gcc spec. (https://gcc.gnu.org/onlinedocs/gcc/Extended-Asm.html#GotoLabels)
• The error-state reset, allows resetting when having to parse multiple source files, such that error-states do not propagate.

Parts of this were merged as #15.

[michael-schwarz]

Hi there,

Thank you for the PR!
The new GCC builtins, support for asm inline, and the function to reset the error-state are non-controversial, we'd be happy to merge that.

When it comes to asm goto support, you might want to compare with #92 and #81 to see if there are any differences.

I am personally reluctant about merging this in as is, as it would violate CIL's invariants: instrs are not supposed to have any intraprocedural control flow (https://goblint.github.io/cil/api/goblint-cil/GoblintCil/index.html#type-instr), so asm gotos would have to be promoted to the level of stmts, and prepareCFG and computeCFGInfo would need to be adapted to handle this. Our student estimated this would require changes to ~100 locations in CIL. (#81 (comment)).

If you're up to do this, we happily welcome the contribution.
If you only want such programs to parse but do not need the capabilities to actually analyze them, I would need to discuss with the co-maintainers if a solution where support for parsing is added but all the functions that rely on this throw an exception if the list of gotos is not empty is something we'd be up for merging.

[michael-schwarz]

Also, it would be good to have some regressions tests that cover the new support you added.

[emiljapelt]

Alright, I will move the non-controversial contributions to a different branch and create a seperate PR for those (#151).

I will discuss the case of asm goto with my advisors/colleagues, but would currently assume that just parsing without analysis capabilites are fine for our purposes.

As for regressions tests, this is not a term that I am familiar with, so if I could be provides some more context/explaination, I would be happy to give it a go.

[michael-schwarz]

As for regressions tests, this is not a term that I am familiar with, so if I could be provides some more context/explaination, I would be happy to give it a go.

Yes, I guess we use the terminology in a somewhat non-standard way. What I meant is that it would be nice to add some tests to https://github.com/goblint/cil/tree/develop/test/small1 that could not be parsed before, but can be parsed now.

[michael-schwarz]

This seems like it is now subsumed by #161 which we aim to merge soon.