The C Bounded Model Checker: Criminally Underused

Re:The C Bounded Model Checker: Criminally Underused by teo_zero on Thursday February 01, 2024 @02:12AM (#39213476)

If you "just" want bounds checking, then you don't need a pointer to array. GCC is able to detect the out-of-bound even in this case:

  int get(int n, char buf[n])
  {
    return buf[10];
  }

It's if you want to use sizeof that you need a pointer to array. But if you have n, why would you need to query the size of your array?

[ Parent | on HN ]

Re:The C Bounded Model Checker: Criminally Underused by sigsev_251 on Thursday February 01, 2024 @04:53AM (#39214296)

A possible answer is that one could modify n inside the function body, which means that the length is lost. But honestly, one could just use const to avoid this. Though, pointers to VLAs are really useful and convenient when allocating dynamic arrays, especially multidimensional.

[ Parent | on HN ]

Re:The C Bounded Model Checker: Criminally Underused by uecker on Friday February 02, 2024 @01:04AM (#39225610)

GCC only works in the first case anyway: https://godbolt.org/z/jo57r1MW4 One could add in the other too, but language semantics currently do not allow this.

Changing the n later has no impact on the size of the arrays later and the compiler is perfectly able to remember the original size.

[ Parent | on HN ]