malloc1.c wrong, not aligned

[andrew-appel]

The usual C specification of malloc() says that the result shall be aligned:

"If allocation succeeds, returns a pointer to the lowest (first) byte in the allocated memory block that is suitably aligned for any object type with fundamental alignment."
cite

Typically for a 32-bit C implementation with 64-bit "long long", the fundamental alignment is 8 bytes.

The implementation of malloc1.c is incorrect on almost any C implementation. That makes it difficult to prove correct.

[andrew-appel]

My workaround is to assert in the precondition that parameter n is a multiple of the natural alignment; this condition is named BOGUS.