Reinstate the usage of the SilFrontend API and support for the refute statement

[jcp19]

This PR reinstates the changes by Lea 🍔 (@bruggerl) introduced in PR #776. To make sure that there are no feature regressions in Gobra, we should only merge this when

• the pretty printer for termination measures in Viper is fixed (Fix pretty printer for termination measures silver#831)
• the chopper can deal with termination measures (Add support for chopping programs before the Termination plugin runs silver#832 - might not be the best solution, we shall see)

In addition to all the fixes listed in PR #776, this PR now also fixes a bug where the option --respectFunctionPrePermAmounts (introduced in PRs and ) is not properly communicated to the backend, as prior to this PR, we called the TerminationPlugin directly, and passed a wrong SilFrontendConfig object

Depends on #819.

Note to the reviewer: The only non-reviewed changes introduced by this PR are in the PluginAwareChopper and its tests, and in the ChopperUtil file

[ArquintL]

As suggested, I've looked at the 3 not yet reviewed files and have a minor wish if it does not take too long to implement besides 3 suggestions for a bit more documentation or typo fixes. Otherwise, looks good! Thanks for this PR! =)