The C standard does not speak of "errors" and "warnings", those are not formal terms. The compiler is only required to produce a diagnostic message, as specified in C11 22.214.171.124:
A conforming implementation shall produce at least one diagnostic message (identified in
an implementation-defined manner) if a preprocessing translation unit or translation unit
contains a violation of any syntax rule or constraint, even if the behavior is also explicitly
specified as undefined or implementation-defined. Diagnostic messages need not be
produced in other circumstances.
The nature of this diagnostic message could be anything: a compiler error, warning, log entry, blinking lights, blowing whistles or a hand-written letter delivered to the programmer's doorstep. As long as the compiler informs the programmer about the problem, it is compliant.
And the opposite: if the compiler does not inform the programmer about syntax or constraint violations, the compiler is non-conforming to the C language standard.
For this reason, you can't prove that your program is correct because "I only got a warning message". A warning message is sufficient for reporting that your program isn't valid C.
The informal term "compiles cleanly" typically refers to a compiled program that did not get any diagnostic messages reported, including warnings.
Popular compilers such as gcc, clang and icc can be configured to always produce errors instead of warnings, in case of syntax or constraint violations, by using
-std=c11 -pedantic-errors which forces these compilers into a strict mode. I strongly recommend beginners learning the language to compile with these settings.
Notably, there is no requirement to produce a diagnostic message in case of undefined behavior or potential run-time bugs. For example the compiler need not inform about
even though it is an obvious bug that can be detected by static analysis in compile-time. Array out of bounds access does not violate a constraint and the syntax is ok, even though this code is explicitly invoking undefined behavior.
For this reason, you can't prove that something is not undefined behavior with "it compiles cleanly".
There is no requirement about what the compiler should do with its output files in case of syntax errors or constraint violations. It isn't specified if the compiler should refuse to generate an object file/binary executable, or if it may do so regardless. In case it does produce such output, despite the C program being non-conforming, there are no guarantees of how that executable will behave. It is no longer valid C, but a non-standard extension of the language.
For this reason, you can't prove that your program is correct because "it runs". It could still contain C language violations as well as undefined behavior.