Summary:
a) An update to build-infer.sh to avoid downloading/building 4.02.3
ocaml compiler when it is already present.
b) Add the ifdef to avoid this error on glibc systems:
clang -c -w libc_basic.c -o libc_basic.o
libc_basic.c:692:12: error: unknown type name '__WAIT_STATUS'
pid_t wait(__WAIT_STATUS stat_loc) {
^
Closes https://github.com/facebook/infer/pull/429
Reviewed By: akotulski
Differential Revision: D3704604
Pulled By: jvillard
fbshipit-source-id: d557f1b
Summary:
- make sure former options of `./infer/lib/python/infer.py --help`, `./infer/lib/python/infer.py --help -- make`, ... all appear in `infer --help`
- add some options to config.ml and infer.ml to fix missing options
- have `infer --help` output help info for Toplevel + Backend + Clang + Java
- wrap help lines at 80 characters
Reviewed By: jberdine
Differential Revision: D3669865
fbshipit-source-id: 1ceff2d
Summary:
Refactor module Prop disentangling the various normalization functions, and moving them inside a new module Normalize.
There is quite a reshuffling of functions, including some dead code removal, but there should be no computational difference.
Reviewed By: jvillard
Differential Revision: D3696491
fbshipit-source-id: 68dd719
Summary:
Clean up the API to access component of propositions.
Use uniform naming for getting and setting components.
Reviewed By: jberdine
Differential Revision: D3696180
fbshipit-source-id: a8aedb0
Summary:
Add module `Core` in Prop to contain the implementation of a prop as a record. The record is private so that pattern matching is unchanged.
Added new function to set individual fields, enforcing that the type becomes exposed when constructing explicitly.
Added function unsafe_cast_to_normal to mark all the cases where a coercion to a normalized type is used.
This is purely a refactoring diff that only affects types, it should have no runtime consequence.
Reviewed By: jberdine
Differential Revision: D3691342
fbshipit-source-id: fa06e29
Summary:
Make necessary changes so that the clang frontend compiles with the
corresponding changes to the facebook clang plugins. Does not actually use the
extra qualifier information yet.
depends on D3684150
Reviewed By: akotulski
Differential Revision: D3684173
fbshipit-source-id: f715f75
Summary:
Attribute.remove was performing an ad hoc form of normalization on
atoms, replace with the standard normalization from Prop.
Reviewed By: cristianoc
Differential Revision: D3686041
fbshipit-source-id: b89e59e
Summary:
This diff lifts the Prop.Attribute module out of Prop. This required
moving several Prop functions that depend on Attribute
(find_arithmetic_problem, deallocate_stack_vars, find_equal_formal_path)
and adding numerous calls to Prop.normalize to fix normal/exposed
mismatches. Also note that the type of Prop.normalize is generalized to
allow calling it on normalized props.
Reviewed By: cristianoc
Differential Revision: D3684523
fbshipit-source-id: f37af8b
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
Summary:
Move the Sil.attribute type and associated types and operations to a new
PredSymb module.
Reviewed By: cristianoc
Differential Revision: D3683834
fbshipit-source-id: d3606a8
Summary:
Change the Aobjc_null attribute from a family of unary predicates, one
for each Pvar.t * Ident.fieldname list, to a single binary predicate.
This diff should not change behavior except for printing of Aobjc_null
attributes. Also, operations such as free variables, etc. should now
behave correctly with respect to variables occurring in the arguments of
Aobjc_null.
Reviewed By: cristianoc
Differential Revision: D3669392
fbshipit-source-id: fe4434a
Summary:
Add support for nary predicates, not just unary ones. Many operations
don't make much sense for nullary predicates, and are generally treated
as no-ops. The first argument is treated specially, as the "anchor" of
the predicate application. For example, adding or removing an attribute
uses the anchor to identify the atom to operate on. Also, abstraction
and normalization operations treat the anchor specially.
Reviewed By: cristianoc
Differential Revision: D3669391
fbshipit-source-id: 3d142ea
Summary:
There is no need to call exp_normalize on the sub-expressions of
arguments to atom_normalize, as it calls exp_normalize on its
sub-expressions.
Reviewed By: cristianoc
Differential Revision: D3669390
fbshipit-source-id: 468b6b1
Summary:
Simplify the (implementation and) interface of Prop by using the atom
type directly instead of a tuple type that duplicates the fields.
This change does not weaken the type guarantees, while reducing
redundancy between types thereby making future changes easier.
Reviewed By: cristianoc
Differential Revision: D3669388
fbshipit-source-id: 65f7493
Summary:
Change representation of pure predicate applications to distinguish
between positive and negative literals using the Apred and Anpred
constructors instead of a boolean field.
This representation is more compact, and is uniform with the treatment
of equalities and disequalities. Some code is simpler, but there isn't
much in it.
Reviewed By: cristianoc
Differential Revision: D3669387
fbshipit-source-id: 07cdea6
Summary:
Treat attributes as unary predicates in classical first-order logic.
This diff extends predicates with a polarity and uses classical 2-valued
semantics. This potentially changes the behavior of negating
attributes, which was not previously relied on.
Reviewed By: sblackshear
Differential Revision: D3669365
fbshipit-source-id: 2f26776
Summary:
Replace disequalities to Attribute expressions with predicate symbol
application pure atomic formulas.
This diff should preserve existing behavior, up to the comparison order
of attribute disequalities versus predicate applications.
Reviewed By: sblackshear
Differential Revision: D3647049
fbshipit-source-id: c39a901
Summary:
Cosmetic changes to comments to improve the results of the Reason
comment attachment logic.
These were found using `git grep -nH -e 'in[ ]*(\*'` although the
attachment logic seems ok if the associated `let` is on the same line.
Some others were found with `git grep -nH -e ')[ ]*(\*'` although the
attachment logic seems ok if the associated `(` is on the same line.
Reviewed By: jvillard
Differential Revision: D3654027
fbshipit-source-id: 122aa3b
Summary:
Make checks context-aware, to increase flexibility.
As an example application of this change, whenever an atomic property is accessed from within a synchronized block, skip reporting a `DIRECT_ATOMIC_PROPERTY_ACCESS` warning.
Reviewed By: jvillard
Differential Revision: D3648831
fbshipit-source-id: c033f45
Summary: Follow up D3579581. We forget about memory acquired in resources with assumption that developers use raii and free memory in destructors.
Reviewed By: jvillard
Differential Revision: D3614056
fbshipit-source-id: 08fa112
Summary:
This is needed on osx, where one of {`Sys.executable_name`, `Unix.readlink`}
does not behave the same as Linux.
Reviewed By: jberdine
Differential Revision: D3614254
fbshipit-source-id: a376636
Summary:
Previously, we would translate `throw` with `return`. However, `throw` in
ObjC/C++ is often used to mean "abort". We now translate `throw` the same as
`exit` to prune these paths.
Reviewed By: akotulski
Differential Revision: D3594156
fbshipit-source-id: 81083bb
Summary:
Minor stuff:
- GCCAst -> GCCAsm
- separate constants and mutable global state in cFrontend_config
- alphabetical ordering in cFrontend_config
Reviewed By: akotulski
Differential Revision: D3593858
fbshipit-source-id: 6f4d9c3
Summary:
No longer allow pointer types to be passed inside var_exp_typ. We used to accept both forms,
but it won't be possible any longer once shared_ptr becomes pointer type.
Reviewed By: dulmarod
Differential Revision: D3593003
fbshipit-source-id: a830914
Summary:
1. Attempt to simplify callExpr_trans by merging multiple if-else branches into one in `CTrans_utils.builtin_trans`. Not every special case works that way, so some of them are still there.
2. On top of that, make type of parameters in `CTrans_models` functions `Procname.t` instead `Procname.t option`. This triggered some more changes to `callExpr_trans`.
3. Semi-randomly reorder instructions in `callExpr_trans`
This is mainly an attempt to clean up the code so any suggestions how to make it better are welcome.
Reviewed By: jvillard
Differential Revision: D3586419
fbshipit-source-id: aef8580
Summary:
Python needs to know about these because it does different things depending on
whether these flags are passed or not.
Reviewed By: cristianoc
Differential Revision: D3593381
fbshipit-source-id: fe3194d
Summary:
Since clang -### can silently return nothing when passed bogus arguments (eg,
trying to compile a non-existent file), run the original command in that case
in case it's a genuine error. This prevents puzzling behaviours such as
`infer -- clang -c bogus_file.c` succeeding with 0 files analyzed.
Reviewed By: martinoluca
Differential Revision: D3592924
fbshipit-source-id: 5d8bc81
Sam Blackshear
Lázaro Clapp Jiménez Labora
Ryan Rhee
Raghavendra Prabhu
Andrzej Kotulski
Martino Luca
Jules Villard
Cristiano Calcagno
Josh Berdine
Vaibhav Tulsyan
Zac Sweers
Dulma Churchill
Daiva Naudziuniene