infer_clone

Commit Graph

Author	SHA1	Message	Date
Martino Luca	cab20f4a6e	[Infer][iOS][Linters][CTL] Rewrite BAD_POINTER_COMPARISON rule into Computation Tree Logics formula Reviewed By: ddino Differential Revision: D3930047 fbshipit-source-id: bb90e92	8 years ago
Dino Distefano	05bb4a0db7	Defining an AST specification language based on CTL for front-end checkers Summary: This diff introduces a first version of a front-end checkers specification language. The language is based on the CTL temporal logic that is interpreted on trees. In this case the model for a formula is the AST of the program produced by clang. This diff introduce the language and translate most of the existing checks on this new language. In other diff I will translate all the other checks. Then I will generalize the framework to allow the developer to specify only the CTL formula. Reviewed By: martinoluca Differential Revision: D3819211 fbshipit-source-id: f8e01eb	8 years ago

Author

SHA1

Message

Date

Martino Luca

cab20f4a6e

[Infer][iOS][Linters][CTL] Rewrite BAD_POINTER_COMPARISON rule into Computation Tree Logics formula

Reviewed By: ddino

Differential Revision: D3930047

fbshipit-source-id: bb90e92

Dino Distefano

05bb4a0db7

Defining an AST specification language based on CTL for front-end checkers

Summary:
This diff introduces a first version of a front-end checkers specification
language. The language is based on the CTL temporal logic that is interpreted
on trees. In this case the model for a formula is the AST of the program produced
by clang.

This diff introduce the language and translate most of the existing checks on
this new language. In other diff I will translate all the other checks.
Then I will generalize the framework to allow the developer to specify only
the CTL formula.

Reviewed By: martinoluca

Differential Revision: D3819211

fbshipit-source-id: f8e01eb

2 Commits (7d49e16d63838ebeb5a15e9495f385d04a94855f)