
<html><head></head><body><div style="font-family:Helvetica Neue, Helvetica, Arial, sans-serif;font-size:13px;"><div>Hello,</div><div><br></div><div>I'm attempting to write a checker to look for certain signedness issues. I have code similar to the following:</div><div><br></div><div>int32_t z = -1;</div><div>read (STDIN_FILENO, &z, sizeof(z));</div><div><br></div><div>if (z > 20) exit (EXIT_FAILURE);</div><div><br></div><div>memcpy (x, y, z);</div><div><br></div><div>Inside the checker I am printing the constraints on the SVal 'z' with a PreCall, filtering on memcpy:</div><div><br></div><div>ProgramStateRef State = C.getState();<br></div><div>State->getConstraintManager().print(State, llvm::outs(), "\n", " ");<br></div><div><br></div><div>I have two questions related to this:</div><div><br></div><div>1. The constraint on the above value is printed as 'conj_$0{int32_t} : { [-2147483648, -1], [1, 20] }'. What happened to zero? My best guess is the static analyzer realizing that 'memcpy(x, y, 0)' is a nop and pruning that program state?</div><div><br></div><div>2. The above code, aside from the zero exception, makes sense when z is an int8_t, int16_t, or an int32_t:</div><div><br></div><div> conj_$0{int8_t} : { [-128, -1], [1, 20] }<br></div><div> conj_$0{int16_t} : { [-32768, -1], [1, 20] }<br></div><div> conj_$0{int32_t} : { [-2147483648, -1], [1, 20] }<br></div><div><br></div><div>However, if I switch this to an int64_t I get:</div><div><br></div><div> conj_$0{int64_t} : { [1, 20] }<br></div><div><br></div><div>What happened to all the negative numbers?</div><div><br></div><div>Apologies if I've missed something obvious.</div><div><br></div><div>Cheers!</div><div>-yrp</div></div></body></html>