<div dir="ltr"><div dir="ltr"><div>Hi,</div><div>I'm pretty confident that this is a bug.<br></div><div>Btw we can minimize the example even more:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><span style="font-family:monospace">typedef unsigned long long size_t;<br>const char a[] = "aabbcc";<br><br>char f1(size_t len) {<br>  return a[len+1];<br>}<br>char f2(size_t len) {<br>  return a[len];<br>}<br>char f3(int len) {<br>  return a[len+1];<br>}</span><br></div></blockquote></div><div><br></div><div class="gmail_attr">After some investigation, I narrowed down to the <span style="font-family:monospace">`ArrayBoundCheckerV2::checkLocation`</span> function, so your guess was right.<br></div><div class="gmail_attr">I will dig deeper and create a patch if I'm done.<br><br></div><div class="gmail_attr">Regards Balazs.<br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">Loïc Joly via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> ezt írta (időpont: 2020. márc. 3., K, 15:58):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hello, I have the following code (you can see it live here: <br>
<a href="https://godbolt.org/z/iiki_w" rel="noreferrer" target="_blank">https://godbolt.org/z/iiki_w</a>)<br>
<br>
typedefunsignedlonglong size_t;<br>
<br>
char f1(size_t len) {<br>
char a[] = "Hello world!";<br>
auto p = a+len+1;<br>
return *p;<br>
}<br>
<br>
char f2(size_t len) {<br>
char a[] = "Hello world!";<br>
auto p = a+len;<br>
return *p;<br>
}<br>
<br>
char f3(int len) {<br>
char a[] = "Hello world!";<br>
auto p = a+len+1;<br>
return *p;<br>
}<br>
<br>
For f1, the static analyzer reports an  of bounds memory access, not for <br>
the other 2 cases, that look quite similar (one is removing adding 1 to <br>
an unknown SVal, the other one is working with int instead of size_t).<br>
<br>
I tried to look into the exploded graph, and I got the following <br>
constraint appearing right on the last node of the graph:<br>
   "constraints": ["symbol": "reg_$0<size_t len>", "range": "{ <br>
[18446744073709551615, 18446744073709551615] }<br>
<br>
I fail to see where this constraint on "len" come from. I know I4m using <br>
an alpha checker, but I'm not sure this is meaningful in this case?<br>
<br>
<br>
Do you have any idea?<br>
<br>
<br>
Thank you!<br>
<br>
<br>
---<br>
<br>
Loïc Joly<br>
<br>
<br>
<br>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote></div></div>