Default verbosity of output when using contracts

[rod-chapman]

CBMC: 6.3.1 on macOS.

When using contracts and proving using the default level of verbosity, I still get some irrelevant noise in the on-screen output. This appears at the end of the output, so prevents me from seeing the results for the function that I actually asked to be verified.

For example, verifification of the "poly_compress()" function from the pqcp/mlkem-c-aarch46 repo, using the starter-kit, and

make result

yields output that ends with:

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_car_set_insert
[__CPROVER_contracts_car_set_insert.assertion.1] line 161 ptr NULL or writable up to size: SUCCESS
[__CPROVER_contracts_car_set_insert.assertion.4] line 161 ptr NULL or writable up to size: SUCCESS
[__CPROVER_contracts_car_set_insert.assertion.2] line 164 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_car_set_insert.assertion.5] line 164 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_car_set_insert.assertion.3] line 168 no offset bits overflow on CAR upper bound computation: SUCCESS
[__CPROVER_contracts_car_set_insert.assertion.6] line 168 no offset bits overflow on CAR upper bound computation: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_is_fresh
[__CPROVER_contracts_is_fresh.assertion.1] line 1161 __CPROVER_is_fresh is used only in requires or ensures clauses: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.2] line 1198 __CPROVER_is_fresh max allocation size exceeded: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.3] line 1252 __CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_is_fresh.assertion.4] line 1325 __CPROVER_is_fresh is only called in requires or ensures clauses: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_obj_set_create_indexed_by_object_id
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1] line 251 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2] line 251 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3] line 251 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.4] line 251 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_write_set_check_assignment
[__CPROVER_contracts_write_set_check_assignment.assertion.1] line 775 ptr NULL or writable up to size: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.assertion.2] line 792 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.assertion.3] line 798 no offset bits overflow on CAR upper bound computation: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.unwind.1] line 807 unwinding assertion loop 0: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_write_set_havoc_object_whole
[__CPROVER_contracts_write_set_havoc_object_whole.assertion.1] line 1403 no OOB access: SUCCESS

<builtin-library-__builtin___memcpy_chk> function __builtin___memcpy_chk
[__builtin___memcpy_chk.overflow.1] line 39 arithmetic overflow on unsigned to signed type conversion in (signed long int)n: SUCCESS
[__builtin___memcpy_chk.overflow.2] line 39 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)(signed long int)n: SUCCESS

Can these results be suppressed at the default verbosity level please?

[tautschnig]

I agree that we should (contracts or not) just refrain from printing properties in CBMC's built-in library when the result is SUCCESS.

[rod-chapman]

Agreed

[rod-chapman]

Any progress to report on this one please?