Support witnesses with ghost variables

[schuessf]

This PR adds support for the validation of witnesses that contain ghost variables. Namely the entry-types (that are not official yet) in YAML-witnesses ghost_variable and ghost_update can now be handled in the validation. The validation of those entry-types works in a similar fashion to the existing entry-type invariant: We translate them to ACSL, s.t. the entries instrumented are in our Boogie-Code. This instrumentation uses ghost code in ACSL that is now supported (see #649).

[schuessf]

Needs to be revised (after SV-COMP), because the format for YAML witnesses has changed and we also use a different parser.

[bahnwaerter]

An important note: The current implementation does not follow the intended witness schema for ghost variables. The following things are different and should be changed in my opinion (in order to remain backwards compatible with the original style of the schema):

• ghost_variables and ghost_updates are not put under content (like the invariant_set entry type does).
• Expressions of ghost_variables and ghost_updates are not represented correctly. They are composed of a value and format field instead of directly assigning the value to the expression field.

[schuessf]

This PR has canged the behaiour for location invariants, they are now added inside an atomic-block. Therefore some witness-tests (e.g. this) fail now with an AssertionError: Atomic section must begin with ICFG location.

@maul-esel Since you worked recently on atomic blocks, why is this the case?

[maul-esel]

The problem seems to be an atomic block in dead code, due to a wrong instrumentation of invariants pointing to labels. The instrumented Boogie program contains the following code:

    ...
    #res := 0;
    return;
    atomic {
        assert false;
    }
  ERROR:
    assert { :reach "ERROR_FUNCTION","reach_error" } false;
    ...

The witness specifies the invariant false at the location for the label. I don't know if we have definitively fixed the semantics for location invariants at labels, but I would expect them to hold whenever one jumps to the label. I've committed a fix for these cases, have a look if you agree.

[maul-esel]

Incidentally, to add regression tests for these kinds of bugs (the instrumentation was wrong, even if the atomic wouldn't have caused it to crash) we would need to support tests where we expect a witness to be rejected. We should add that in the future (maybe we can base it on our planned experiments comparing with other validators).