2 ms·

Thank you! I assume 'Access types are not memory-safe, right? Is there a SPARK equivalent which still does not copy (i.e. it only references) that is memory saf

Thank you! I assume 'Access types are not memory-safe, right? Is there a SPARK equivalent which still does not copy (i.e. it only references) that is memory safe? To be more specific, how would one implement something like a "Get_First_Word" or "Trim_Whitespace" without copying?

LegionMammal978 1y ago
I think it's supposed to be safe in Ada by default? As far as I can tell, basic allocated objects cannot be deallocated without an "unchecked" operation, and access objects created from "aliased" declarations are subject to scoping rules [0]. (If you want to know the full details, go figure out however "accessibility levels" are supposed to work [1].) It should preclude functions from returning access objects without a "prefix'Unchecked_Access" operation. I'm not sure how SPARK's borrowing system is tied into all of this. [0] https://www.adaic.org/resources/add_content/docs/craft/html/ch11.htm https://www.adaic.org/resources/add_content/docs/craft/html/... [1] http://www.ada-auth.org/standards/22rm/html/RM-3-10-2.html http://www.ada-auth.org/standards/22rm/html/RM-3-10-2.html