David Monniaux on Nostr: nprofile1q…6gyrf I spent quite some energy writing suitable predicates for creduce ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqf3nlrmpjja65pzmvlegyl27l0y2m007nncxttdwqndrejajvdzask6gyrf (nprofile…gyrf) I spent quite some energy writing suitable predicates for creduce when testing CompCert so that it did not introduced undefined behavior.

(I wrote a bit about it in section 4 here https://hal.science/hal-04096390v1/file/tests_CompCert_TAP23_preprint.pdf )