(whoops, re-added the mailing list)

Due to the short circuit nature of logical binary operators, the value

of the expression `x && y` is equal to the value of `y` as long as `y`

gets evaluated at all, and to `false` otherwise. You can see which

branch is evaluated in the callback for `x` by figuring out if `x`

evaluates to `false`, and in this case you already know that the value

of `x && y` would be false. You can see which branch is evaluated in the

callback for `y` - it is definitely the branch on which `y` is

evaluated. In this callback the value of `x && y` can be computed as `y`.

P.S. If you are trying to prove that some expressions in the code are

always false or always true, you won't be able to do it that way,

because all computations within checker callbacks are based on the

assumptions that allowed the program to reach the respective point in a

certain state, and may be incorrect on other paths to the same program

point in which the state of the program is different or different

assumptions have been made. For example, in code

if (a < 10) {

}

if (a < 10) {

}

you would "prove" that the second branch condition is both "always true"

(i.e., assuming you take the true branch on the first if(), the

condition is definitely true on the second if) and "always false" (i.e.,

assuming you take the false branch on the first if(), the condition is

definitely false on the second if).

Static Analyzer's path-sensitive engine is only useful for problems that

consist in finding execution paths with special properties

("may"-problems), not for proving that paths with certain properties do

not exist ("must"-problems). The only on-by-default "must"-checker in

the Static Analyzer is the DeadStores checker (assigned value is

discarded or overwritten before use on all paths after the assignment),

and it works by exploring the CFG manually and doesn't rely on the

Static Analyzer's path-sensitive engine.

On 11/19/18 7:56 PM, illiop via cfe-dev wrote:

> Hello,

> Thanks in advance for any help!

> If I have the following code:

> void function()

> {

> int a = 1;

> if ( ( a<10 ) && ( a > 20 ) ) // always false

> {

> }

> }

> How can I evaluate the whole condition expression '( a<10 ) && ( a >

> 20 ) ' ?

> When I write code like:

> class MyChecker : public Checker< check::BranchCOndition >

> {

> public:

> void checkBranchCondition(const Stmt* cond, CheckerContext& ctx) const;

> }

> I found that checkBranchCondition() only be called back 2 times, once

> for 'a<10' , once for 'a > 20 '. And it's done. No further call back.

> But my goal is to get the 'value' for the whole '( a<10 ) && ( a > 20

> ) '.

> I tried the following in vain:

> 1. in checkBranchCondition(), find the 'father' node(it is '( a<10 )

> && ( a > 20 ) ' ), and evaluate its 'sval', but the sval is

> invalid/undifined

> 2. Use check::PostStmt<CompoundStmt> call back. It does NOT called

> back at all

> 3. Use check::PostStmt<Stmt> call back, and try to find the 'father'

> by : if(isa<IfStmt>(stmt)), useless.

> 4. Use check::PostStmt<BinaryOperator>, but it still only called back

> 2 times: once for 'a<10' , once for 'a > 20 '

> I am a fresh man in the static analyzer, please help, thanks!

> illiop

>

>

>

>

> _______________________________________________

> cfe-dev mailing list

>

[hidden email]
>

http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev_______________________________________________

cfe-dev mailing list

[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev