Daniel Schemmel

Well, @MartinNowack `KLEE: ERROR: Loading file /tmp/klee_build110stp/runtime/lib/libkleeRuntimeKLEELibc32_Debug+Asserts.bca failed: No such file or directory` sounds like there might be some problem outside of this PR? I also cannot reproduce the other...

@ccadar rebased. Sorry about the nested namespaces, that was my fault.

@ccadar has asked me to shepherd this PR for eventual inclusion in mainline KLEE. Here is what I currently think we have to do: - Cleanly rebase on master (the...

@qrort you may also wish to answer the open review questions.

This test executes external function calls into the C++ standard library to initalize buffers. This is not supported (and has not been supported in 2014). C++ support has since been...

Note that the proc-macro in question spews out a rather large function primarily consisting of a large (>30k lines in this case) initializer. That initalizer has a few levels of...

There are some known problems with the dockerfile (age has not been very kind to it), which I am currently working on. However, you should be aware that your M1...

Generally speaking, any `no_std` Rust code that wants to exit in a similar fashion to `std::process::exit` (rather than returning through `main`), for example when having to write a panic handler....

Turns out that I was not quite thorough enough, and that `rustix::runtime::exit_group` was exactly what I was looking for, I just could not find it without your comments. I still...

The following program shows that STP thinks `0x80 ashr 100 == 0xFF`, i.e., overshifting a negative value also gives minus one here. ``` ret is false COUNTEREXAMPLE BEGIN: ASSERT( b...