Ted Kaminski

@giltho wrote a test showing this, but we decided not to merge it as a "fixme" since it's more of a feature request, but recording it here for future reference:...

When I wrote `kani-driver` I dropped this feature because there were parts of it that were taking me too longer to figure out how to translate correctly (in part because...

This is probably a concrete example of #1056 needing to be done.

> I need to understand when the NondetTransformer is used and why. Right now, even when the NondetTransformer is used, the final code will contain Nondet expressions because the lowering...

Is this just about `main` in integration tests? Isn't that a strange thing to do? Did we actually run into code somewhere that does that?

Writing down thoughts so they don't get lost. Two potential issues here 1. #661 This could be causing issues because `main` might otherwise be given a fully-qualified name that doesn't...

ALTERNATIVELY! It sounds like MIRI does "normal" compilation (to rlib) every step of the way until the very end, where it also pulls in the standard library rlib and then...

I think the fix for this MIGHT be to refactor the "virtual table drop" code to actually call the normal virtual table invocation code, instead of sort of duplicating it,...

I don't quite get the "reasoning" section. The function returns only true or false (the result of the `==`). The bits of the `u8` don't really matter except that they're...

Three approaches to this: 1. We could move calling `symtab2gb` into `kani-compiler`. This would probably be the most optimal solution given our current architecture. 2. We could just parallelize these...