void is the unit type, which has a single inhabitant, so those functions have a codomain; you can think of the unit type as the set containing the empty set. Sure, you don't explicitly write a return statement in C for `void` functions, but as long as the function still terminates, it can still be thought of as producing a value. Admittedly, not a very useful one, since all having a value of type void tells you is that whatever function produced it completed, but that mostly reflects the fact that `void` functions generally do other non-functional stuff; there's nothing inherently wrong with returning or having such a value, and it can be quite useful for generic code. For example, a map from keys to unit can be used to implement a set "for free."
Even in non-generic, purely functional code, the unit type is still useful--as the domain for a constant function! In most C-like languages, this is of course just represented by a function that takes no arguments, but type theoretically it's equivalent to taking a single void argument (or any number of void arguments, of course, since the Cartesian product of two sets with one inhabitant produces another set with one inhabitant). In strict functional languages that insist that everything has a type, you will often use this encoding explicitly, to implement thunks (call-by-name evaluation).
In partial languages (aka every language you're likely to practically use) or total languages which have the principle of explosion (which covers most of the remaining languages in existence), there is also the bottom type (the empty set) which has no inhabitants; this represents falsity or impossibility, which is computationally meaningful as a (perhaps not terribly informative) type for programs that can't return a value; for instance, nonterminating ones, or ones that always throw an exception. However, since in general you shouldn't be able to produce a closed value of that type, it can usually be freely cast to any other type you want, so many languages lack explicit syntax for it.
That said, it can still be convenient at times to have a way of explicitly talking about the empty type; for example, in Rust (behind a feature flag currently), if you use a sum type where all but one of the variants includes the bottom type `!`, the compiler will recognize that only one variant is possible, and allow you to directly extract data from the inhabited variant (and can optimize out the tag, or at least that's the intent). This is useful when writing generic code that has to implement an API that returns (for instance) a `Result<T, E>`, but your implementation doesn't have an
error condition; in such cases, you can set `E = !`.
In total, dependently typed languages with the principle of explosion (which are certainly functional!), the type is also useful for another reason; a function from A to False is the equivalent (constructively anyway) of the negation of A, `~A`. Therefore, False ends up getting used quite a lot in type-level expressions, for the same reason as tests against the empty set occur a lot in set theory; even though strictly speaking you shouldn't be able to produce a closed value of type False (or else you should file a bug), when you're doing proofs by contradiction you can end up with one due to some false assumption in your context (which you can immediately use to prove that anything you wish derives from that context; this can be particularly useful to discharge impossible arms of pattern match expressions). This also happens implicitly in languages that perform flow-sensitive analysis of pattern match expressions; if they detect that one arm never returns (e.g. because it throws an exception or runs a loop that clearly doesn't terminate) they can implicitly assign it the bottom type, which can then be automatically cast to the type of the full expression.
In short: not only are function types with void (and even empty!) domain and codomain functional, they are actually remarkably useful :) In fact, they are so fundamental, that almost all of (standard) dependent type theory can be constructed from just three base types: the empty type, the unit type, and bool! It's a bit unfortunate that two of these three fundamental types don't have direct syntax in a lot of languages, but as you can see this is mostly because they are so ubiquitous that they are largely hidden within other language features.
> void is the unit type, which has a single inhabitant
Not in C. void is an incomplete type, with an empty domain. There is no value which is an instance of void.
The void type cannot be completed, and so there is no way to instantiate an object of void type. An object of type void cannot be defined or declared. There can be no array of void, nor a structure member of type void.
The void keyword in C and C++ just serves as a syntactic/semantic hack.
Casting an expression to (void) is a gesture which indicates that the value is deliberately being discarded (and is not an actual conversion).
A function declared as returning void returns nothing; and a return statement with a value must not be used in its body: even a value that has been cast to (void) type. Because, remember, that is not actually a conversion to a void type, and the function has no return type.
In ANSI C, (void) was introduced to distinguish the syntax of a declared-empty parameter list from that of an unspecified parameter list. That's a pure syntactic hack. It could easily have been something else, like (static) or (--).
There can be a pointer to void, and that is loaded with yet more hacks. Such a pointer can't be dereferenced or subject to arithmetic (that being possible is a GCC extension).
I enjoy pedantry too, so I guess I kind of understand why you keep making this point. However, it's not relevant to what the OP asked, which was about the mathematical modeling of C functions that return void, rather than trivia related to C syntax. In the two positions in C and C++ that I discussed, the domain and codomain of a function, void is functionally identical to unit, despite your protestations to the contrary (there is literally no semantic distinction between them). In Rust, none of these restrictions exist and we can freely use unit in all the ways you described, but in the domain and codomain of a function it still works just like void does in C (we can't cast from arbitrary types to void, but this is more because Rust takes a hard stance against stupid casts than because it would be difficult to implement, and it has other ways of representing deliberately throwing away a value).
The C standard, of course, may disagree, and claim that there is no value of type "void" and that void functions "have no return type." That I can call and successfully return from a void function, call a function taking void, and even cast a value to void, provide ample evidence (which would also be backed up by reading the standard) that what it means by "type" is not the same thing as what a mathematician means by "type" (and "completed" is a complete red herring here). The fact that you don't explicitly return a void value doesn't really mean anything--no return or return with no value are pure syntactic sugar for returning a void value, which is also how it's implemented in many other languages that enjoy explicit unit types.
What I can't do in C is bind one of the many values of type void to a variable (and do a few other things, like call `sizeof` on the type, or explicitly name the inhabitant of void as a literal, which again have pretty much nothing to do with the semantics of the thing). That is a much weaker restriction, for the same reason that defining a binding as `const` is much weaker than a guarantee that the underlying value isn't mutated; bindings are a largely syntactic artifact and don't affect the mathematical model of a C function in any way. This is especially true for unit types, since having an instance of one is completely uninformative as they both always exist and are all definitionally equal!
Of course, this doesn't apply to void * , which as you point out is really its own bizarre thing that is mostly unrelated to void itself (I'd like to call it a pointer to the top type, but I'm not certain even that would cover its semantics). I think it's fair to say that despite some degree of overlap, void * is an unrelated concept overloading the "void" keyword, and that the actual interpretation of bare "void" is indeed equivalent to unit, not that every other use of `void` in C is completely arbitrary and unprincipled. The reason, AFAIK, why C doesn't just add all those void-related features it's missing is because it has baked in decisions like "every type has a nonzero size" and "arrays are pointers" (conflicting with void * ) that make adding stuff like this after the fact very complicated, not because it wouldn't make sense semantically (in a proper semantic model, where void * was called something like any * and zero sized types were legal, many of these issues would go away, including--I'm pretty sure--all the reasons why C and C++ must insist that void values not be completed). In any case, none of this helps with or is relevant to reasoning about C functions as mathematical objects.
And just to be extra clear--even if C had no keyword at all for `void` functions and didn't have `void` as an option for argument lists, these functions would still be modeled as taking / returning values of type unit.