If you use Hoare triples for total correctness, you can't reason about non-terminating programs. I recommend to use a Hoare logic for "generalised" correctness that enables you to reason about both, terminating and nonterminating programs.
I would be interested in your ideas about aliasing. I don't think you can avoid the complications of separation logic or content quantification.
For non-terminating programs I use processes as described by Tony Hoare in "Communicating Sequential Processes". Procedures must always terminate in Albatross.
If I have more documentation on aliasing, I can give you hint. Could you provide me some email address?
I would be interested in your ideas about aliasing. I don't think you can avoid the complications of separation logic or content quantification.