output inconsistent axioms for constants

[agle]

./mill run -i ../basil-tv-artifact/basilbench/cntlm-noduk/cntlm-noduk.gtirb --lifter  --trim-early --simplify-tv cntlm-tv/ --main-procedure-name http_parse_basic  --trim-depth 1 -o cntlm.bpl
boogie cntlm.bpl /proc 'p$http_parse_basic_4232224'   /warnVacuousProofs

Proves everythign vacuously because it outputs inconsistent axioms, e.g.

const {:extern} $__PRETTY_FUNCTION__.0_addr: bv64;
axiom ($__PRETTY_FUNCTION__.0_addr == 4282392bv64);
const {:extern} $__PRETTY_FUNCTION__.0_addr: bv64;
axiom ($__PRETTY_FUNCTION__.0_addr == 4282256bv64);
const {:extern} $__PRETTY_FUNCTION__.0_addr: bv64;

Possibly specific to gtirb readelf frontend, my guess is these are variables with static linkage.

Using this gtirb file: https://github.com/agle/basilbench/blob/fabcf5df5d2f955734882c4227b5a5d1f80b5220/cntlm-noduk/cntlm-noduk.gtirb

[l-kent]

__PRETTY_FUNCTION__ is a gcc-created magic constant that provides the name of the current function. I think clang has adopted it too? https://gcc.gnu.org/onlinedocs/gcc-11.5.0/gcc/Function-Names.html

https://github.com/agle/basilbench/blob/fabcf5df5d2f955734882c4227b5a5d1f80b5220/cntlm-noduk/cntlm-noduk.relf

You can see there's duplicate names in the symbol table. It should be simple to enforce unique names for the symbol table data though.