[cfe-dev] [Analyzer] How to model `assert(condition)`?

[Henry Wong via cfe-dev]

Hi all,
I want to know if anyone has tried to model `assert()`? Or has some thoughts on it?

`assert()` is a macro defined as follows:
    #ifdef NDEBUG
        #define assert(condition) ((void)0)
    #else
        #define assert(condition) /*implementation defined*/
    #endif

It's difficult for analyzer to figure out which part is expanded from macro `assert()`. The ways I can think of immediately are as follows.

(1) Use some clang-based rewrit tools to replace `assert(condition)` with `if (!condition) exit(0)`.
This way will loose the semantics of `assert()` and only gurantee the `condition` must be true after the `assert` is evaluated.

(2) Add two CFGElement kinds, `AssertBegin` and `AssertEnd`, like `ScopeBegin` and `ScopeEnd`. In this way, analyzer can easily figure out whether the current program point is in `assert()`.

(3) Use `checkPreStmt(const Expr *)` and `checkPostStmt(const Expr *)` to figure out whether the current Stmt is expanded from `assert`.

Once the `assert()` part is located, the rest of the work is modeling. Like `__builtin_assume` in https://reviews.llvm.org/D33092, we can use `ProgramState::assume` to get two states, one is a sink state corresponding to the assertion failure and the other is the valid state.

Any suggestions?

Thanks in advance!

Henry Wong
Qihoo 360 Codesafe Team
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180807/4f1ff85d/attachment.html>