tree cdd109a78fc3c615556d668a9841bac248c546d8
parent ddffa06501085d3800962b86a2b7eddb18f4e3b4
author Gilles Peskine <Gilles.Peskine@arm.com> 1538670749 +0200
committer Gilles Peskine <Gilles.Peskine@arm.com> 1538681794 +0200

Evolve choose_int_from_mask to if_int

Make the function more robust by taking an arbitrary zero/nonzero
argument instead of insisting on zero/all-bits-one. Update and fix its
documentation.