[cfe-dev] [StaticAnalyzer] How to give hint on path execution

[Artem Dergachev via cfe-dev]

Yay: It turns out that it might be a lot easier to accomplish with body 
farms(!)

Generally, the idea is to provide a fake body instead of the unavailable 
body of your close() function which would probably look like:

   void close(FILE *fp, void (*callback)(void)) {
     fclose(fp);
     callback();
   }

See how, for example, dispatch_sync() is modeled in 
lib/Analysis/BodyFarm.cpp.

Once you have a fake body, the path-sensitive engine would be able to 
execute it with the desired effect. It's much easier than what i 
originally proposed.

Adding Gábor because it's his realm :)

On 5/8/17 8:08 PM, Artem Dergachev wrote:
> Unfortunately, allowing checkers to trigger an immediate inlining of a 
> function is quite tricky to implement, and we don't have a ready-made 
> mechanism for that (though some of the existing checkers could make 
> use of such functionality).
>
> It might theoretically be possible, within a checker callback, to 
> manually construct an exploded graph node that represents entering a 
> stack frame of the callback function, and then addTransition() to such 
> node (similarly to how ExprEngine does that) and see what happens. 
> That'd be an interesting problem to tackle, and such mechanism would 
> be good to have.
>
> Also, are you sure it is necessary to model the callback exactly in 
> your use case? Maybe a simple invalidation/escape pass would suffice 
> to avoid false positives?
>
>
> On 5/7/17 11:03 PM, Paul Bert via cfe-dev wrote:
>> Hi,
>>
>> I wrote a checker similar to the  SimpleStreamChecker except that the 
>> close function that moves the state of the stream to released,  takes 
>> a second parameter, a callback, for instance
>>
>> close(FILE *, mycallback).
>>
>> When the stream moves to release state, the callback is executed.
>>
>> The "close" function is defined externally so that the checker cannot 
>> reason on it except using the rules I give it in checkPostCall 
>> callback. How can I make the analyzer  aware that the callback has to 
>> be executed when the state move to release?
>>
>> Thanks for any help,
>>
>> Paul
>>
>>
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>