implied: certain states should be left as is
commit2cffc12007bbfc38e6b01ed529b769bd2b1cd376
authorDan Carpenter <dan.carpenter@oracle.com>
Tue, 29 May 2012 07:14:09 +0000 (29 10:14 +0300)
committerDan Carpenter <dan.carpenter@oracle.com>
Tue, 29 May 2012 07:14:09 +0000 (29 10:14 +0300)
treed451ace1f15e163d9cfcff8c0207cdc01296e67e
parent162aa09d3d08d67d1a5778af2e6f65137dc0c6df
implied: certain states should be left as is

This is very complicated and I'm not sure the fix is complete, but it fixes
the new test case in sm_implied11.c.

I've invented some new vocabulary.  The Base Slist is what the slist is
when you are indented one tab.  In other words you are not inside an if
or else block.  The Base Slist can never be merged with another slist so
the ->pool is never set.

Right before a branch from the Base Slist, I'm calling that the
Last Base Slist.  I save a copy of that before the branch.

Also I've modified merge_slist() to give all the slists an slists ID.
Slists with low slist IDs flow into slists with higher slist IDs.

There are two more vocabulary words I want to introduce.  When we have the
following if statement:
if (x == 99) {...
We want to figure out the implications of the statement then we can say
that "x" is the Gateway Element, or the Gateway SM.  The slists from the
->pool pointers for "x" are Gateway Slists.

How Smatch implied works is that it tracks the state back through the
->left and ->right merges and lops off the branches which are not true.
The problem is that states which were set in the Base Slist are true on
every path.  But we lop it off and we can't add it back.

That's complicated to explain...

Anyway, what is easy to understand is that I handle this as a special case.
If a state is true in the Base Slist and the Gateway SM was set after the
state then the state is going to be the same no matter what the Gateway
Slists are.

Signed-off-by: Dan Carpenter <dan.carpenter@oracle.com>
smatch.h
smatch_flow.c
smatch_implied.c
smatch_slist.c
smatch_slist.h
smatch_states.c
validation/sm_implied11.c [new file with mode: 0644]