model-checker does not like buster-produced binaries
Contrary Stretch, on Buster, we get this from the model checker:
Multiple read only segments for /home/samy/test, not supported
And indeed:
55fc2d1c3000-55fc2d1c4000 r--p 00000000 fd:02 27001857 /home/samy/test
55fc2d1c4000-55fc2d1c5000 r-xp 00001000 fd:02 27001857 /home/samy/test
55fc2d1c5000-55fc2d1c6000 r--p 00002000 fd:02 27001857 /home/samy/test
55fc2d1c6000-55fc2d1c7000 r--p 00002000 fd:02 27001857 /home/samy/test
55fc2d1c7000-55fc2d1c8000 rw-p 00003000 fd:02 27001857 /home/samy/test
Using -Wl,-z -Wl,norelro
gets rid of one of the spurious RO segment, but not the other, which contains for instance:
0000000000002000 R _IO_stdin_used
0000000000002018 r __GNU_EH_FRAME_HDR
000000000000215c r __FRAME_END__
It seems that the Buster linker script now puts read-only variables after the read-write variables, and thus they can't be put in the same segment as the code, and there are thus basically always two separate read-only segments.