infinite recursion in goto-cc

[nmanthey]

Dear CBMC Team,

I just tried to compile upstream Xen with the current develop branch version (8f6dab8). I get the following trace when I compile the symbols tool of Xen. This single goto-gcc call leads to segmentation faults on machines with large memory.

Best,
Norbert

To reproduce:
git clone git://xenbits.xen.org/xen.git
cd xen
git checkout 11535cd
cd xen/tools
gdb --args goto-gcc -Wall -Werror -Wstrict-prototypes -O2 -fomit-frame-pointer -fno-strict-aliasing -Wdeclaration-after-statement -o symbols symbols.c

Trace:
#6884 0x0000000000584f37 in c_typecheck_baset::typecheck_expr (this=this@entry=0x7fffffffc9a0, expr=...)
at c_typecheck_expr.cpp:50
#6885 0x00000000005832e6 in c_typecheck_baset::typecheck_return (this=0x7fffffffc9a0, code=...)
at c_typecheck_code.cpp:681
#6886 0x0000000000581fa1 in c_typecheck_baset::typecheck_code (this=0x7fffffffc9a0, code=...)
at c_typecheck_code.cpp:69
#6887 0x00000000005803f2 in c_typecheck_baset::typecheck_block (this=0x7fffffffc9a0, code=...)
at c_typecheck_code.cpp:187
#6888 0x0000000000581ce6 in c_typecheck_baset::typecheck_code (this=0x7fffffffc9a0, code=...)
at c_typecheck_code.cpp:46
#6889 0x00000000005992d4 in c_typecheck_baset::typecheck_side_effect_function_call (
this=0x7fffffffc9a0, expr=...) at c_typecheck_expr.cpp:2020
#6890 0x0000000000597afd in c_typecheck_baset::typecheck_expr_side_effect (this=0x7fffffffc9a0,
expr=...) at c_typecheck_expr.cpp:1886
#6891 0x000000000058bf1b in c_typecheck_baset::typecheck_expr_main (this=0x7fffffffc9a0, expr=...)
at c_typecheck_expr.cpp:172
#6892 0x0000000000584f37 in c_typecheck_baset::typecheck_expr (this=this@entry=0x7fffffffc9a0, expr=...)
at c_typecheck_expr.cpp:50
#6893 0x00000000005832e6 in c_typecheck_baset::typecheck_return (this=0x7fffffffc9a0, code=...)
at c_typecheck_code.cpp:681
#6894 0x0000000000581fa1 in c_typecheck_baset::typecheck_code (this=0x7fffffffc9a0, code=...)

[tautschnig]

This has been fixed by #2553.