This PR enables automatic memory initialization proofs for raw pointers in Kani. This is done without any extra instrumentation from the user.
Currently, due to high memory consumption and only partial support of pointee types for which memory initialization proofs work, this feature is gated behind -Z uninit-checks flag. Note that because it uses shadow memory under the hood, programs using this feature need to pass -Z ghost-state flag as well.
This PR is a part of working towards #3300.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This PR enables automatic memory initialization proofs for raw pointers in Kani. This is done without any extra instrumentation from the user.
Currently, due to high memory consumption and only partial support of pointee types for which memory initialization proofs work, this feature is gated behind
-Z uninit-checksflag. Note that because it uses shadow memory under the hood, programs using this feature need to pass-Z ghost-stateflag as well.This PR is a part of working towards #3300.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.