Backtranslate Boogie to ACSL, fix backtranslation issues

[schuessf]

Currently our backtranslation from Boogie to C (CACSL2BoogieBacktranslator) returns an IASTExpression. However, we return our own implementation FakeExpression in most cases, which is bascially a string. Therefore we do not create an actual AST, but do some string concatenation instead.

Therefore this PR aims to translate Boogie to an actual AST in ACSL. To output these ACSL-expressions in witnesses or on the console the already existing class ACSLPrettyPrinter is used, which might be extended/improved (e.g. avoid unnecessary parentheses based on the operator precedence). Additionally I extracted a class Boogie2ACSL for this to extract functionality from CACSL2BoogieBacktranslator and translate the Boogie expressions mostly independent from the underlying C-Location.

Also I fixed some issues of the backtranslation:

• Introduce casts in backtranslation (d75e13eb592b736a4271bfad05f393467e82d689) to capture the translation of Boogie's unbounded integers to C properly and avoid unwanted overflows and wraparounds (e.g. for addition/multiplication/...). To avoid too many unnecessary casts, we try to track the possible value of every backtranslated (integer) expression and only introduce casts if necessary (i.e. the backtranslated expression does not fit in the underlying type)
• Fix the backtranslation of large integer literals (a0e59a304ebf9e6f4ffcde9116f142b0d2e30ab6): For some literals we need to add an unsigned suffix, 128bit literals even need to be split using bitwise operations (see https://stackoverflow.com/questions/16088282/is-there-a-128-bit-integer-in-gcc)

Before I rebased this branched, I checked if the new backtranslation via ACSL still produced the same String as the current backtranslation, see the results on Jenkins

[schuessf]

Is the wrapper BacktranslatedExpression useful outside of Boogie2ACSL?

Currently not, it is mainly used for two different reasons:

• BacktranslatedExpression has a CType that might be used
• If ACSL-Expression would be used as a return, we need to prefix the full package name in CACSL2BoogieBacktranslator, since it already uses Boogie-Expression

I see you removed containsProcedureCall, but I didn't quite grasp how the functionality works now. Could you explain?

We do not create any function-calls in our ACSL-backtranslation (I am not entirely sure, if our ACSL currently allows this). So this is no more needed.

Previously we used the CLocation of the Boogie-expression in the backtranslation. We only translated IdentifierExpression, if it contained an IASTDeclaration or IASTExpression. This way we wanted to translate variable, if they did not represent a C-variable, but another expression (e.g. f(x), x++). I already removed this backtranslation of non-identifiers in 5f661d159df0abe32d0264e1ae9f08a3380d6099, because it was not handled correctly anyway and we should not have C-expressions with side-effects in invariants (x++ == f(x) is a bad invariant 😄). Now we backtranslate variables only to C-variables if possible and independant of the location.