Summary

The Checked C docs (“Programmer-inserted dynamic checks”) and other articles mention that using _Dynamic_check as a loop precondition so the compiler can eliminate dynamic bounds checks inside the loop. In the example below, even with_Dynamic_check(src_count <= dst_count) placed before the loop, the dynamic bound checks for src[i]/dst[i] remain at -O1 and -O2.

example

#include <stddef.h>

void append(
    _Array_ptr<char> dst : count(dst_count),
    _Array_ptr<char> src : count(src_count),
    size_t dst_count, size_t src_count)
{
  _Dynamic_check(src_count <= dst_count);

  for (size_t i = 0; i < src_count; i++) {
    if (src[i] == '\0') {
      break;
    }
    dst[i] = src[i];
  }
}

Expected behavior

From _Dynamic_check(src_count <= dst_count) and the loop guard i < src_count, it should follow that i < dst_count. Therefore:

The dynamic bounds checks for dst[i] should be removed .
The checks for src[i] should also be removable based on the loop bound.

Actual behavior

At -O1/-O2, the generated IR/assembly still contains dynamic checks (or equivalent guarded paths) inside the loop for both dst[i] and src[i]. No elimination is observed.

Questions

Does the Checked C toolchain currently support proving loop safety from _Dynamic_check + for-loop bounds and eliminating the bound checks?
If supported, are there specific flags/passes or coding patterns (e.g., additional assumptions/builtins) required to trigger this optimization?
If not supported yet, is this optimization on the roadmap? Any recommended workaround short of manual code cloning?