Can't you just have a NonZeroInt type?

Only if your language supports dependent types.

It's perfectly possible in languages with ordinary ADTs.

  data Nat = Z | S Nat
  data NonZeroNat = OnePlus Nat
  data NonZeroInt = Negative NonZeroNat | Positive NonZeroNat

C isn't one of those languages, though.

The analogous would be the Go-style represent-a-sum-badly-as-a-product,

  struct nonzero_t {
    int is_negative;
    unsigned int one_less_than_the_absolute_value;
  };

which, under interpretation, ranges from -(2^32) to -1 and +1 to +(2^32).

In Ada, you can define integer types that only accept a given range of values.

Not really - internally inputs 0 and 1 use different branches.

That's not a branch; otherwise you would have an infinite (or impossibly large) number of branches for just that one line of code. A branch is when you execute one set of code upon a given condition, and another if that condition is not met.

I didn't say every number is a different branch. But on many processors, divide by zero triggers an interrupt. That's semantically the same as a branch.

It depends on the language. In C it is not a branch because division by zero is undefined and not a path you consider. In Java you can argue that there are two branches. One branch that throws an exception and one that does not.

No coverage reporting library will attempt to tell you that kind of coverage. You are essentially in violent agreement with the op but turning it into an argument by using different words for the same concept.