Allow checking cover statements without `--cover cover`

[zhassan-aws]

CBMC version: cbmc-5.49.0
Operating system: All

This is an enhancement request. Currently, the __CPROVER_cover statements are only checked if cbmc is run with --cover cover. Running cbmc without --cover cover results in the following warning:

**** WARNING: no body for function __CPROVER_cover

and the statement is ignored. Given that cover statements are useful for checking reachability and certain conditions, and given that they cannot be used with other commonly-used options (e.g. --unwinding-assertions):

$ cbmc cover.c --cover cover --unwinding-assertions
--cover and --unwinding-assertions must not be given together

it would be useful if CBMC checks cover statements by default.

[tautschnig]

Here's an example of mine that could be "cover.c":

#include <assert.h>

int main(int argc, char * argv[])
{
  if(argc < 5)
    __CPROVER_cover(argc < 4);

  assert(argc < 42);

  for(int i=0; i < argc; ++i)
    ++i;
}

which would be nice to process successfully when using cbmc --cover cover --unwinding-assertions --unwind 5 cover.c.

[feliperodri]

@tautschnig any updates on this issue?