Zvonimir Rakamaric

@mutilin Do you maybe have any clues on this one? It seems that these are based on real bugs, and so maybe you know where this bug is hiding. That...

@tautschnig What does CBMC report on this one this year? It timed out last year, but maybe not this year. Basically, I can't really figure out where the bug is...

Coming back to this. As far as I know, trigonometric functions are not specified in the IEEE floating-point standard, and libraries choose to implement them differently, meaing that different implementations...

The implementation in GNU C is system-dependent. I presume it uses inlined assembly and such, which varies depending on for which processor the code is compiled. So could someone point...

I don't think that's true of any implementation, since maybe you could have weird implementations of sin and cos that do not obey any of the rules we might expect...

Oh, and now the discussion is split between the mailing list and github. We should probably pick one and stick with it.

Hi all. Are there any plans for this to be fixed? We are experiencing these issues in the memory safety category. We could create a patch that will fix just...

@tautschnig : It seems that you contributed these tasks, and so maybe you could pitch in here. Thanks!

We find bugs in all of these ``` ntdrivers/diskperf_false-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ntdrivers/diskperf_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ntdrivers/floppy2_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ntdrivers/floppy_false-unreach-call_true-valid-memsafety.i.cil.c false(valid-memtrack) ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-memtrack) ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ntdrivers/parport_false-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ntdrivers/parport_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ``` I am having trouble keeping...

Wait, why shouldn't we just change the labels? It is not like we have to fix them so that they don't contain bugs. We just have to update their labels....