Options --no-arch and --no-library do not appear to affect generated symbol table

[florianschanda]

Hi,

I have this tiny program:

int main()
{
  int x = 5;
  if (x > 7) {
    x = 9;
  }
  assert (x <= 4);
}

I am observing that the following invocations generate bit-for-bit equal output:

• cbmc --json-ui --show-symbol-table foo.c
• cbmc --json-ui --show-symbol-table --no-arch --no-library foo.c

Specifically the generated symbol table is full of:

   __CPROVER__start
   __CPROVER_alloca_object
   __CPROVER_architecture_NULL_is_zero
   __CPROVER_architecture_alignment
   __CPROVER_architecture_arch
   __CPROVER_architecture_bool_width
   __CPROVER_architecture_char_is_unsigned
   __CPROVER_architecture_char_width
   __CPROVER_architecture_double_width
   __CPROVER_architecture_endianness
   __CPROVER_architecture_int_width
   __CPROVER_architecture_long_double_width
   __CPROVER_architecture_long_int_width
   __CPROVER_architecture_long_long_int_width
   __CPROVER_architecture_memory_operand_size
   __CPROVER_architecture_os
   __CPROVER_architecture_pointer_width
   __CPROVER_architecture_short_int_width
   __CPROVER_architecture_single_width
   __CPROVER_architecture_wchar_t_is_unsigned
   __CPROVER_architecture_wchar_t_width
   __CPROVER_architecture_word_size
   __CPROVER_constant_infinity_uint
   __CPROVER_dead_object
   __CPROVER_deallocated
   __CPROVER_initialize
   __CPROVER_malloc_failure_mode
   __CPROVER_malloc_failure_mode_assert_then_assume
   __CPROVER_malloc_failure_mode_return_null
   __CPROVER_malloc_is_new_array
   __CPROVER_malloc_may_fail
   __CPROVER_malloc_object
   __CPROVER_malloc_size
   __CPROVER_max_malloc_size
   __CPROVER_memory
   __CPROVER_memory_leak
   __CPROVER_next_thread_id
   __CPROVER_next_thread_key
   __CPROVER_pipe_count
   __CPROVER_rounding_mode
   __CPROVER_size_t
   __CPROVER_thread_id
   __CPROVER_thread_key_dtors
   __CPROVER_thread_keys
   __CPROVER_threads_exited

Some of which I would have expected to disappear if the --no-arch and --no-library options are given.

Did I mis-understand what these options are doing?

[martin-cs]

• There are no regression tests for either.
• --no-arch was added on or before 2013, maybe in the CVS era (pre-subversion, pre-git)? As far as I can tell it is not actually used. --arch none should do something (although it may break because ... we do need some architectural information) along those lines so I am thinking we should just remove it.
• --no-library looks like it could work but it is used in link_to_library which is just after the handling of --show-symbol-table so you won't see any difference in that.