<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
</head>
<body dir="ltr">
<div id="divtagdefaultwrapper" style="font-size:12pt;color:#000000;background-color:#FFFFFF;font-family:Calibri,Arial,Helvetica,sans-serif;">
<p></p>
<div>Hello,</div>
<div><br>
</div>
<div>Is there a simple way to enumerate all of the constrained symbolic values (and constraints) required to reach a function call (where the call is outside the current translation unit) in a Clang checker? For example, `foo` in this case:</div>
<div><br>
</div>
<div>```</div>
<div>int x = read();</div>
<div>int y = read();</div>
<div>int z = read();</div>
<div>if (x > 1 && y > 2 && z > 3) {</div>
<div> foo(x);</div>
<div>}</div>
<div>```</div>
<div><br>
</div>
<div>The desired information would be something roughly analogous to { (x, [2, 2147483647]), (y, [3, 2147483647]), (z, [4, 2147483647]) }. <span style="font-size: 12pt;">I've tried a few different methods to elicit this information in the PreCall and PostCall
hooks, but it seems that the ConstraintManager only is tracking constraints on the arguments to `foo`. </span></div>
<div><br>
</div>
<div><span style="font-family: Calibri, Arial, Helvetica, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', NotoColorEmoji, 'Segoe UI Symbol', 'Android Emoji', EmojiSymbols; font-size: 16px;">I've reviewed the available documentation and re-watched the "Building a
Checker in 24 Hours" talk (which was great BTW). </span>I've also taken a look at some of the existing checkers to see how I might inform the execution to track constraints on these values, but nothing is jumping out at me.</div>
<div><br>
</div>
<div>I know there are some advertised limitations on symbolic execution but it seems like this should be possible. I'm new to clang internals so pardon if I missed something obvious.</div>
<div><br>
</div>
<div>Thanks,</div>
<div>Jon</div>
<p></p>
</div>
</body>
</html>