Added tests that demonstrate the issue with static inline c functions.

[NlightNFotis]

There is a problem with cbmc with how it handles static inline qualified functions. If we include a main function, and run cbmc without the --function parameter, so that it defaults to main, it converts the program without any issues.

On the other hand, if we pass it a file without a main method in it, and call it with --function fun, then it will result in a CONVERSION ERROR.

This pull request contains tests to demonstrate that.

[thk123]

@NlightNFotis Unless I've misremembered, even if we have a main method, calling a static inline method with the --function flag causes a conversion error.

[thk123]

This one should be CORE right?

[martin-cs]

> @@ -0,0 +1,9 @@ +KNOWNBUG This one should be CORE right?

CORE if we are supposed to be fixing it / it is fixed. KNOWNBUG if we hope to fix it one day and are just documenting.

[NlightNFotis]

The investigation so far has produced the following results:

It seems that the function ansi_c_entry_point, lines 207-225, can't find the function supplied with the command line argument --function fun in the symbol table.

In a investigation of the symbol table values from the command line and from program debugging (inspecting the symbol table data structure), I found that for the version with the main function, the symbol table contains 42 entries, whereas for the version without the main function, the symbol table contains 35 entries, missing the critical entries for fun and fun::a which correspond to the function itself, and its argument.

I plan on investigating further the symbol table construction, to understand why in the case where the static inline function is the only one in the translation unit, it doesn't even get added in the symbol table, and what happens during the symbol table creation function that doesn't add the entries.

[tautschnig]

I'd say this is remove_internal_symbols doing its work well before the argument to --function is being considered.