Michael Tautschnig

I believe CBMC would be quite ok with inserting the necessary type casts (to use the C library functions) if you just consistently go with the Rust/LLVM declarations.

> I changed Kani to insert the casts. I have another blocker with the std sockets library. I haven't had time to figure out what's wrong I wouldn't be surprised...

To what extent is Kani controlling the code being generated here? I note that, as of https://github.com/diffblue/cbmc/pull/6647, CBMC has support for saturating addition and subtraction, and adding support for multiplication...

I believe the problem is that the symbols you create for missing functions do not have a source location. Looking at `_ZN60_$LT$alloc..string..String$u20$as$u20$core..clone..Clone$GT$5clone17hd1d44edec193123bE` as is generated from the following piece of...

I re-enabled the RustRealloc hook that was removed in #1088 and then tried the examples from #702 with this PR. I got: ``` $ kani 702.rs --enable-unstable --zero-init-vars thread 'rustc'...

They might be the same underlying type, but it seems their struct tags (the names of the symbols that have the actual type information in the symbol table) are different.

I'll work on improving the output of those checks, I've myself been caught by this lack of information more than once. That said, however: are you setting `is_parameter` at all?...

> I don't see `is_parameter` set to true anywhere. Which symbols does CBMC expect it to be set for? All symbols that are function parameters. Presumably there is some code...

It seems that there is an inconsistency on the parameter types. Your symbol table includes a declaration of `memcmp` that matches the one that C has, which has `void*` typed...

> Thanks Michael! That message was a bit cryptic for me. What a euphemism :-) I locally hacked it to use the `.pretty()` output to get the full ireps in...