<div dir="ltr">Hi,<div><br></div><div>I am registering my own map in the program state using the the following:</div><div><br></div><div>REGISTER_MAP_WITH_PROGRAMSTATE(ConstantMap, SymbolRef, VariableConstVal)<br></div><div><br></div><div>where VariableConstVal is the structure containing the information I want in this map. </div><div><br></div><div>I am populating this map in the callback checkPostStmt() using state = state->set<ConstantMap>(sym, ...) while the state graph is being constructed.</div><div><br></div><div>At the end of analysis, I want to now read the information stored in this map in the callback checkEndAnalysis(ExplodedGraph &G, BugReporter &B, ExprEngine &Eng). However, I am not sure how to get the SymbolRef associated with an ExplodedNode which is what I get when I iterate over the ExplodedGraph at the end of the analysis.</div><div><br></div><div>How can I get the SymbolRef that I can use to index into my map? In checkPostStmt(stmt* S, CheckerContext &C), I used the following code to get the SymbolRef that I can use to store the information in the map:</div><div><br></div><div><div> SVal val = state->getSVal(S, lctx);</div><div> SymbolRef Sym = val.getAsSymbol();</div></div><div><br></div><div>but in checkEndAnalysis(ExplodedGraph &G, BugReporter &B, ExprEngine &Eng) I do not seem to have a handle to stmt* to get the SVal.</div><div><br></div><div>I guess my question is probably not phrased very well, but I hope some one can make some sense out of it. Also, I guess I have a long way to go before I understand the data structures in the analyzer well. I checked the other checkers, but none of them seem to exhibit exactly my requirement.</div><div><br></div><div>Thanks.</div><div><br></div><div>Regards,</div><div>Venugopal Raghavan.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jan 25, 2017 at 3:19 PM, Venugopal Raghavan <span dir="ltr"><<a href="mailto:venur2005@gmail.com" target="_blank">venur2005@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi Aleksei,<div><br></div><div>Thanks. I will check this.</div><div><br></div><div>Regards,</div><div>Venu.</div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jan 25, 2017 at 3:15 PM, Aleksei Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<div class="m_-1222624000317224944m_8180934762430575759moz-cite-prefix">Hello Venugopal,<br>
<br>
During analysis, you have access to a single path only. But after
the analysis is done, you can summarize information across
different paths using checkEndAnalysis() callback. You will get
full ExplodedGraph built for the function so you will be able to
look into its every node.<br>
<br>
<br>
25.01.2017 09:25, Venugopal Raghavan via cfe-dev пишет:<br>
</div>
<blockquote type="cite"><div><div class="m_-1222624000317224944h5">
<div dir="ltr">Hi,
<div><br>
</div>
<div>Firstly, apologies for the long email below.</div>
<div><br>
</div>
<div>I am new to the Clang Static Analyzer (CLA). My interest in
CLA was more to see if I can solve quickly path-sensitive
data-flow analysis problems than as a vehicle to build
bug-finding checkers. I needed the solutions to such data flow
problems to extract some behavioral properties from some test
cases I have. For example, consider the following piece of
code:</div>
<div><br>
</div>
<div>if (cond) {</div>
<div> x = 4;</div>
<div>}</div>
<div>else {</div>
<div> x = 5;</div>
<div>}</div>
<div><br>
</div>
<div>L: .... = ...x..; // Use of variable x</div>
<div><br>
</div>
<div>I want to identify program locations such as "L" in the
code above where x is not a constant if you aggregate
data-flow information across paths, but, on the other hand, is
actually a constant if you have path-specific data flow
information. Since CFA does path-specific analysis, I was
curious to know if it would help me with such tasks. The
"bug-report" I want at location L is that x has a value 4,
given the path constraint for the path including the
"then-path" of the if statement and that x has a value 5 along
the else-path.</div>
<div><br>
</div>
<div>I started writing a checker to accomplish the above task,
but was quickly blocked by some basic doubts. My rough plan
for the checker was to maintain a map in ProgramState which
maps ProgramPoints (or, maybe program symbols) to constants
when those variables indeed have constant values at the
ProgramPoint. For example, when CFA expands states along the
then-path and reaches "L", my map would say that at
ProgramPoint "L", variable x has a constant value 4. Then,
when CFA expands nodes along the else-path, I guess it would
again create a state corresponding to L which now says that x
has the constant value 5. I want to be able to catch this
scenario where the same variable at the same ProgramPoint has
two different constant values depending on the path taken.</div>
<div><br>
</div>
<div>However, the issue is that, when the state graph along the
else-path is expanded, it would no longer have any of the map
contents that was built along the disjoint then-path. How then
can I get access to the then-path information when I am
expanding the path along the else-path? Since the checker is
also required to be stateless, I cannot maintain auxiliary
information in the checker that is persistent across multiple
calls to the call-back function. </div>
<div><br>
</div>
<div>Can you help me with this question? Maybe, I am trying to
use CFA in ways it was not meant to be used viz. as a vehicle
to solve data flow problems which consults information cutting
across paths. Maybe, the CFA is meant to handle problems which
require the examination of information restricted to single
paths. Is that the case? Or, am I missing something?</div>
<div><br>
</div>
<div>Thanks.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Venugopal Raghavan.</div>
</div>
<br>
<fieldset class="m_-1222624000317224944m_8180934762430575759mimeAttachmentHeader"></fieldset>
<br>
</div></div><pre>______________________________<wbr>_________________
cfe-dev mailing list
<a class="m_-1222624000317224944m_8180934762430575759moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>
<a class="m_-1222624000317224944m_8180934762430575759moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><span class="m_-1222624000317224944HOEnZb"><font color="#888888">
</font></span></pre><span class="m_-1222624000317224944HOEnZb"><font color="#888888">
</font></span></blockquote><span class="m_-1222624000317224944HOEnZb"><font color="#888888">
<br>
<p><br>
</p>
<pre class="m_-1222624000317224944m_8180934762430575759moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre>
</font></span></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>