<html>
<head>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
</head>
<body text="#000000" bgcolor="#FFFFFF">
If 'x' is 100 or greater, it'd mean that undefined behavior has
already occured, and it's pointless to explore that path further.<br>
<br>
Same with 'x' being less than 0, so the checker should have added
that as well.<br>
<br>
So i believe that this is a valid behavior. A similar approach is
taken by, say, DivZeroChecker that refutes the "y == 0" patch after
"x / y" is evaluated. NullDereferenceChecker also assumes that all
dereferenced pointers are non-null.<br>
<br>
If they can prove that the operation is indeed unsafe on the current
path, then the assumption would fail, and these checkers would
report a warning instead.<br>
<br>
What sort of problem are you having with these assumptions? Why are
they affecting your checker? With constraints it shouldn't normally
ever be an issue, because adding constraints doesn't really "mutate"
the program state, it just "clarifies" it.<br>
<br>
<div class="moz-cite-prefix">On 7/11/18 3:27 AM, Henry Wong via
cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:PS1PR0401MB1993D9C55AC7B29A380DD658A45A0@PS1PR0401MB1993.apcprd04.prod.outlook.com">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
Hi all,</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
For the code below, the `ArrayBoundCheckerV2` will add the
constraint `x < 100` after the `buf[x] = 1`, see
<a href="https://reviews.llvm.org/D23112" id="LPlnk612572"
moz-do-not-send="true">https://reviews.llvm.org/D23112</a>. </div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
```</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<span>void test_assume_after_access(unsigned long x) {<br>
</span>
<div> int buf[100];<br>
</div>
<div> buf[x] = 1;<br>
</div>
<div> clang_analyzer_eval(x <= 99); //
expected-warning{{TRUE}}<br>
</div>
<span>}</span><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
```</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<span style=" background-color: rgb(255, 255, 255); display:
inline !important">1.<span> </span></span><span style="
background-color: rgb(255, 255, 255); display: inline
!important">What is the purpose for doing this? </span></div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<span style=" background-color: rgb(255, 255, 255); display:
inline !important">2. why not add `x >= 0</span><span
style=" background-color: rgb(255, 255, 255); display: inline
!important">` as well?</span><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
I <span style="color: rgb(0, 0, 0); font-family: Calibri,
Helvetica, sans-serif; font-size: 12pt;">
used</span><span style="color: rgb(0, 0, 0); font-family:
Calibri, Helvetica, sans-serif; font-size: 12pt;">
`checkLocation()</span><span style="color: rgb(0, 0, 0);
font-family: Calibri, Helvetica, sans-serif; font-size: 12pt;">`,
same as `ArrayBoundCheckerV2</span><span style="color: rgb(0,
0, 0); font-family: Calibri, Helvetica, sans-serif; font-size:
12pt;">`, in my</span><span style="color: rgb(0, 0, 0);
font-family: Calibri, Helvetica, sans-serif; font-size: 12pt;"> own
</span><span style="color: rgb(0, 0, 0); font-family: Calibri,
Helvetica, sans-serif; font-size: 12pt;">c</span><span
style="color: rgb(0, 0, 0); font-family: Calibri, Helvetica,
sans-serif; font-size: 12pt;">hecker too</span><span
style="color: rgb(0, 0, 0); font-family: Calibri, Helvetica,
sans-serif; font-size: 12pt;">.
</span><span style="color: rgb(0, 0, 0); font-family: Calibri,
Helvetica, sans-serif; font-size: 12pt;">Due to the uncertain
calling order,</span><span style="color: rgb(0, 0, 0);
font-family: Calibri, Helvetica, sans-serif; font-size: 12pt;"> I
got the
</span><span style="color: rgb(0, 0, 0); font-family: Calibri,
Helvetica, sans-serif; font-size: 12pt;">wrong constraints on
`</span><span style="color: rgb(0, 0, 0); font-family:
Calibri, Helvetica, sans-serif; font-size: 12pt;">x` in my own
checker.
</span><span style="color: rgb(0, 0, 0); font-family: Calibri,
Helvetica, sans-serif; font-size: 12pt;">T</span><span
style="color: rgb(0, 0, 0); font-family: Calibri, Helvetica,
sans-serif; font-size: 12pt;">hat's why I
</span><span style="color: rgb(0, 0, 0); font-family: Calibri,
Helvetica, sans-serif; font-size: 12pt;">pay attention to this
problem.</span></div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
Thanks in advance!</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div style="font-family:Calibri,Helvetica,sans-serif;
font-size:12pt; color:rgb(0,0,0)">
Henry Wong</div>
<div style="font-family:Calibri,Helvetica,sans-serif;
font-size:12pt; color:rgb(0,0,0)">
Qihoo 360 Codesafe Team</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
cfe-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>