3 ms·

Doing it normally should create a copy of the value, as far as I can tell. Unless you use it to create a renamed variable or by-reference parameter, the same wa

Doing it normally should create a copy of the value, as far as I can tell. Unless you use it to create a renamed variable or by-reference parameter, the same way you can create references in C++. I think the closest thing to a &str in Ada would be an "access String" or "access constant String", which you would get either from an allocated "String" or from a declared "aliased String". You'd create a subslice with "string(x..y)'Access". Though I'm not sure whether that actually works without explicitly declaring an array of "aliased Character", the Manual is dense (as with C++, it's nearly meaningless unless you already know what it's supposed to mean) and the tutorials generally avoid talking about access objects.

whytevuhuni 1y ago
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
shakna 1y ago
That's for String, not the referenced Unbounded String.

whytevuhuni 1y ago

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

shakna 1y ago

That's for String, not the referenced Unbounded String.