> Easier to keep the generator simple and let the compiler do the optimisations > it already understands.
Based on things like the experiences of Tahoe LAFS with compiler optimizations vs. security - let alone plain bugs - I am scared if anybody uses any optimizations at all, especially for serious business. I have not researched the position se4L takes on this. Are the proofs about the before-optimization code, or do they consider the after-optimization assembly output? thanks. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
