Infer采用OCaml編寫，可標識Null指針訪問、資源和內存泄漏，以及其它一些C、Java和Objective-C代碼中的可檢測錯誤。據(jù)Facebook介紹，在他們的iOS和Android移動應用中，80%的軟件缺陷是由Infer正確地檢測出的。
AL易于擴展，這克服了一個局限Infer的問題。實現(xiàn)擴展不僅需要具備靜態(tài)分析的專門技能驗，而且需要掌握Infer的內部機制。具體而言，AL意在簡化對過程內（Intra-procedural）軟件缺陷新類型分析程序（Checker）的定義，即局限于過程代碼內的軟件缺陷。這類軟件缺陷可使用更簡單的分析手段檢測到，包括借助于程序語法、通用語言習語和自定義約定。舉個例子，在Objective-C中，為避免存留環(huán)路，對象的delegate通常不應做為strong引用。針對需求的分析程序可使用AL定義為：
DEFINE-CHECKER STRONG_DELEGATE_WARNING = { LET name_contains_delegate = declaration_has_name(REGEXP("[dD]elegate")); SET report_when = WHEN name_contains_delegate AND is_strong_property() HOLDS-IN-NODE ObjCPropertyDecl; SET message = "Property or ivar %decl_name% declared strong"; SET suggestion = "In general delegates should be declared weak or assign"; };在上面的AL代碼中，亮點在report_when語句。該語句在ObjCPropertyDecl對象上定義了一個條件，聲明為一個strong引用（is_strong_property）。ObjCPropertyDecl對象就是關聯(lián)到Objective-C屬性定義的AST節(jié)點。
據(jù)Facebook介紹，通常使用數(shù)行AL代碼就能新定義一個分析程序，并可立即投入使用，無需重新構建Infer，確保了對新分析程序的快速反饋。AL還支持定義基于時態(tài)邏輯模型的更復雜公式，其中一個AST節(jié)點可關聯(lián)到時間上某一點，其所有的后代節(jié)點均看作是未來可驗證的。例如，為保證程序的正確性，HOLDS-EVENTUALLY所關聯(lián)的表達式可在未來某個時間點上得以驗證。
AL是Infer的一個組成部分，已開源于GitHub上，適用于C、C++和Objective-C。
京公網安備 11010502049343號