The C Bounded Model Checker: Criminally Underused

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

Interesting, but how do you define a function that returns an array? Maybe:

  T f(args)[..] { body }

This would be hard to parse. Then what about:

  T[..] f(args) { body }

But if adding [] after T is allowed in function declaration, then why not for arrays as well:

  T[..] a;

[ Parent | on HN ]

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

Very nice comment. This was a blocking point I fell onto too. There is another option, to not allow spans on the return channel, but I don't know how people who handle resources with lifetimes that exceed the function scope will take this. Just like you, I'm curious to see what how this will be solved.

[ Parent | on HN ]