<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="HU" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span lang="EN-US">Hello,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">I have some trouble with symbolic expressions. Either I expect too much from the Static Analyzer, or – more probable – I use the wrong functions.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">I have two different problems where I do not get what I expect.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">The first problem seems very simple: I want to compare two symbolic expressions, one of them is something like {conj_1}, the other one is {conj_1} + 1. Using SValBuilder::evalBinOpNN() I get UnknownVal for comparison
with e.g. BO_GE or BO_LT. I thought that these very simple expressions are easy to evaluate. I only get concrete integer result (1) if the two sides of the comparison are exactly the same (e.g. {conj_1} >= {conj_1}).<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">I also tried subtracting them from each other. Using SValBuilder::evalBinOpNN() I also get UnknownVal for subtraction, and for Symbolmanager::getSymSymExpr() I get symbolic expression ({conj_1} + 1) - {conj_1}, and then
for the comparison to zero using SValBuilder::evalBinOpNN() I get symbolic expression ({conj_1} + 1) - {conj_1} > 0 instead of a concrete integer (1). This method is worse since it does not work for expressions like {conj_1} - {conj_1} >= 0 either.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">The second problem seems also simple: I make an assumption for the state, like {conj_1} == {conj_2}. If I dump the state, I see the range of {conj_1} == {conj_2} [1 .. max]. Later, I have comparison where I check e.g.
{conj_1} >= {conj_2}, but I get UnknownVal. Checking {conj_1} == {conj_2} does not help either. I also tried the subtraction here, thus to store {cont_1} – {cont_2} in the state (range was either [0..0] or [-max..-1], [1..max]), but it did not help either.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">So, how to do it correctly? I assume that such basic symbolic calculations are part of some checkers which work for a while now. Any ideas?<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">Thanks in advance!<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">Regards,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal">Ádám<o:p></o:p></p>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
</div>
</body>
</html>