In embedded C code, we don't explicitly initialize global variables to 0, as the boot code will do that when system boots.
There are two global variables in my code, for example, A and B. My code will promise that A will no longer be larger than B as long as they have a zero initial value.
But when I check a Coverity reported issue, it supposed A might be larger than B. It seems that Coverity didn't think they both have an initial value 0.
From Synopsys's reply, Coverity doesn't track global variables. It infers from context that a defect is possible when the values of the variables are unknown.
Here's a reference article.