Traces on windows report integers as longs

[polgreen]

I realise long and int are the same size on windows, but I still think CBMC should report the types as they are declared in the code unless a cast occurs. If nothing else, it adds an extra layer of obfuscation when reading the traces.

Test case:

int main()
{
	unsigned long a;
	unsigned int b;
	a = 0;
        b = 0;
	__CPROVER_assert(0,"");
}

The trace on linux will report:

a=0ul
b=0u

On windows it will report

a=0ul
b=0ul

[tautschnig]

This isn't really a bug in building the trace, but actually a side effect of merge_ireps: we maintain the C types as comments. As unsigned int and unsigned long are fundamentally the same type (and just distinguishable by irep comments), merge_ireps discards one of them. Which of them gets discarded really depends on whatever is seen first.

Possible fixes are a way to disable merge_ireps, or using merge_full_irept for some parts. It's not clear to me that either of these are worth the cost, so I'll leave this issue open for documentation purposes, but will tag it "wontfix."