5 ms·

> there are products that offer memory-safety proofs for C what does the c checked by this tool look like? for an example like https://play.rust-lang.org/?vers

> there are products that offer memory-safety proofs for C what does the c checked by this tool look like? for an example like https://play.rust-lang.org/?version=stable&mode=debug&edition=2024&gist=18cd3ce3a459de7c41563eef542521b7 https://play.rust-lang.org/?version=stable&mode=debug&editio... , does the tool accept the assignment with f and reject the assignment with g?

pron 1y ago
That particular code is shaped by Rust's specific scoping an lifetime rules, but generally - yes (provided you offer annotations for things the tool can't infer). Some changes to the code may be needed to make things easier, but it's still a lot cheaper than a rewrite in a different language.
- kobebrookskC3 1y ago
  in this example, aren't the scoping rules for c pretty much the same? what do the annotations for the tool look like? is the analysis local, in that it doesn't look into the bodies of other functions? if it is, surely you would have to have lifetimes and be generic over them. how much c code satisfies the tool? if there's hardly any c satisfying the tool, there might actually be a larger ecosystem of rust code to use.
  - pron 1y ago
    So the annotations for such tools are pre/post conditions for certain properties (say, pointer validity, ownership). Like types, function annotations can sometimes be inferred, or they may need to be explicit. Once that information is known about a function, there's no need for the tool to look inside it again when analysing callers. If you want to get a sense of what that may look like, see https://www.frama-c.com https://www.frama-c.com (which is a community project, so maybe not as smooth and polished like more professional tools).
    - KsassPeuk 1y ago
      Well, Frama-C is maintained thanks to public funding (Europe/France) and industrial users who use it for actual certification of systems. For example, Thales (Common Criteria EAL7), Airbus (DO-178C), EDF (ISO 60880). I don't know what you mean by professional tool if this is not professional ;)

pron 1y ago

That particular code is shaped by Rust's specific scoping an lifetime rules, but generally - yes (provided you offer annotations for things the tool can't infer). Some changes to the code may be needed to make things easier, but it's still a lot cheaper than a rewrite in a different language.

kobebrookskC3 1y ago
in this example, aren't the scoping rules for c pretty much the same? what do the annotations for the tool look like? is the analysis local, in that it doesn't look into the bodies of other functions? if it is, surely you would have to have lifetimes and be generic over them. how much c code satisfies the tool? if there's hardly any c satisfying the tool, there might actually be a larger ecosystem of rust code to use.
- pron 1y ago
  So the annotations for such tools are pre/post conditions for certain properties (say, pointer validity, ownership). Like types, function annotations can sometimes be inferred, or they may need to be explicit. Once that information is known about a function, there's no need for the tool to look inside it again when analysing callers. If you want to get a sense of what that may look like, see https://www.frama-c.com https://www.frama-c.com (which is a community project, so maybe not as smooth and polished like more professional tools).
  - KsassPeuk 1y ago
    Well, Frama-C is maintained thanks to public funding (Europe/France) and industrial users who use it for actual certification of systems. For example, Thales (Common Criteria EAL7), Airbus (DO-178C), EDF (ISO 60880). I don't know what you mean by professional tool if this is not professional ;)