Add cover checks to CBMC

[feliperodri]

Feature

A cover check specified as __CPROVER_cover(expr, msg) is considered a SUCCESS if a model can be found where both control flow constraints and expr are satisfied, and a FAILURE otherwise.

The main motivation is to use cover checks in tandem with assertions, to detect vacuity.

#include <stdbool.h>
int main() {
  int x;
  if(x>0){
    __CPROVER_assert(x > -12, "not vacuous");
    __CPROVER_cover(x > -12, "not vacuous");
  } else if(x <= 0) {
    __CPROVER_assert(x < 12, "not vacuous");
    __CPROVER_cover(x < 12, "not vacuous");
  } else {
    __CPROVER_assert(x > 12, "vacuous");
    __CPROVER_cover(x > 12, "vacuous");
  }

  bool a, b;

  if(!a) {
    __CPROVER_cover(a, "fails");
    __CPROVER_assert(a ==> b, "vacuous");
  }

  return 0;
}

** Results:
vacuity.c function main
[main.assertion.1] line 5 not vacuous: SUCCESS
[main.cover.1] line 6 not vacuous: SUCCESS
[main.assertion.2] line 8 not vacuous: SUCCESS
[main.cover.2] line 9 not vacuous: SUCCESS
[main.assertion.3] line 11 vacuous: SUCCESS
[main.cover.3] line 12 vacuous: FAILURE
[main.cover.4] line 18 fails: FAILURE
[main.assertion.4] line 19 vacuous: SUCCESS

GOTO ASSERTION and symex_target_equationt are extended with an attribute specifying the expected
status, VALID or SATISFIABLE, and the generated VCC for SATISFIABLE is !(guard & cond).

goto_symex_property_decider results are interpreted knowing the expected status for a property, and the PASS/FAIL status is flipped accordingly.

The trace output does not try to show a trace for a failed cover check.

Remaining problems

• some tests are failing, need to investigate (seems like some assertion specific methods get called on instructions that are not assertions)
• goto binary serialization/deserialisation is not updated yet so the expected validity status may well get lost on save/reload (help appreciated)
• traces for successful cover checks are not saved

See #6698 for more details.