Summary: procnames will depend on Typ.t soon and we need to go from `type_ptr` to `Typ.t` when creating procnames. `CType_decl` does this translation it can't depend on `mk_procname_` functions.
Reviewed By: jvillard
Differential Revision: D4620560
fbshipit-source-id: 9524178
Summary:
Passing the context was a bit messy and there was duplicated code. The flow is as follows:
For each node, we analyze that node and then it's children, and in some cases we use the parent node
for specifying a context for its children. Now this should be a bit more clear.
In the case of if, we specify a context based on the condition that is expected to be true inside the
if body, but not inside the else body. Here only the framework is set, more if conditions will be added to the
context in future diffs.
Reviewed By: martinoluca
Differential Revision: D4462247
fbshipit-source-id: 3512bd2
Summary:
Remove the remaining uses of polymorphic equality `=`.
In case of basic types, this is replaced by String.equal or Int.equal.
In case of `= []`, this is replaced by `List.is_empty`.
In case of `= None`, this is replaced by `is_none`.
In case of a datatype definition such as `type a = A | B`,
a `compare_a` function is defined by adding `type a = A | B [@deriving compare]`
and a `equal_a` function is defined as `let equal_a = [%compare.equal : a]`.
In case of comparison with a polymorphic variant `= `Yes`, the equality
defined in `PVariant.(=)` is used. Typically, `open! Pvariant` is added
at the beginning of the file to cover all the uses.
Reviewed By: jberdine
Differential Revision: D4456129
fbshipit-source-id: f31c433
Summary:
Module CFrontend_utils is a container for two modules: Ast_utils and General_utils.
Instead of opening CFrontend_utils in several places, it is now split into two separate modules CAst_utils and CGeneral_utils, which are now accessed directly.
Reviewed By: jberdine
Differential Revision: D4392710
fbshipit-source-id: ea756a2
Summary:
This diff allows to use the linters written in DSL to check for bugs.
Now new checkers can be written directly in the DSL.
The diff also remove some weirdness and simplify the CTL semantics.
For example no need to unwrap a node when evaluating the IN operator.
Also no need to distinguish anymore between stmt and decl in the
semantics of EX and EF.
Moreover, the diff de-couple hard-coded checkers (eg checks on component kit)
from those checkers parsed in the .al files.
Reviewed By: martinoluca
Differential Revision: D4375207
fbshipit-source-id: 9ac2d47
Summary:
This will simplify the InferPrint logic of checking what should/should-not be reported.
I will remove the issue names in Localise in a next diff.
Reviewed By: ddino
Differential Revision: D4334327
fbshipit-source-id: ebcfd6c
Summary:
This change is to support the development of CTL's DSL, where issues can be specified directly from the language, in the form of strings.
Severity is specified locally to the place where the check is defined
Reviewed By: ddino
Differential Revision: D4326594
fbshipit-source-id: 7b146ac
Summary:
This diff introduces place-holders strings in error messages and evaluates them
when an error needs to be reported.
Place-holders strings are of the form %name_of_helper_function%. They will be evaluated
using and helper function that gives a value.
For example if we need to display the name of a variable in the error message we will have:
".... %var_name%...."
then %var_name% will be evaluated in the ast node calling the appropriate
helper function and the results will replace %var_name% in the message.
Reviewed By: dulmarod
Differential Revision: D4313133
fbshipit-source-id: bf521ca
Summary:
In checkers we use "let" clause to define formulas abbreviation.
This diff expands the use of such formula id when used.
This allows to evaluate the formula.
For example.
let f = f_def
let g = g_def
let h = f or g
will expand the use of f and g with their definition.
Reviewed By: martinoluca
Differential Revision: D4299542
fbshipit-source-id: 9d37dd0
Summary:
Utils contains definitions intended to be in the global namespace for
all of the infer code-base, as well as pretty-printing functions, and
assorted utility functions mostly for dealing with files and processes.
This diff changes the module opened into the global namespace to
IStd (Std conflict with extlib), and moves the pretty-printing
definitions from Utils to Pp.
Reviewed By: jvillard
Differential Revision: D4232457
fbshipit-source-id: 1e070e0
Summary:
It was defined in two places and I'm about to add a third, so let's share
instead.
Reviewed By: sblackshear
Differential Revision: D4153420
fbshipit-source-id: 3d2c519
Summary:
This is needed for later: InferClang will no longer be started once for each
source file to be analysed. Instead, it will be called to analyse several files
at once, and will analyse them one by one. Thus, `clang_lang` and `source_file`
are moved to `cFrontend_config` as references.
The biggest change this entailed was the new logging infrastructure, which was
depending on `Config.source_file`. This diff moves the logic entirely to
`Logging`, and changes the API so that executables wishing to log into files
have to set it up using `Logging.set_log_file_identifier`. This can be called
several times during the execution, allowing to dynamically change the log file
(eg, when analysing several source files one by one!).
Reviewed By: jberdine
Differential Revision: D3944148
fbshipit-source-id: 6129090
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
Summary:
Adding a new mode linters. Now if the analyzer is linters, we do the linters and don't translate,
then, if the analyzer is Infer, we do the translation and the backend and not the linters checks, and the
default is that we do capture, backend and lint checks.
Made the tests separated, which saves time and also shows that the linters mode works.
Reviewed By: jvillard
Differential Revision: D3723472
fbshipit-source-id: 9d828d8
Summary:
Enable warning 23 (Useless record with clause), make fatal, and fix the
existing instance.
Reviewed By: sblackshear
Differential Revision: D3685950
fbshipit-source-id: 8ee415d
Martino Luca
Dino Distefano
Dulma Churchill
Andrzej Kotulski
Cristiano Calcagno
Ryan Rhee
Josh Berdine
Jules Villard
Sam Blackshear