Summary:
When analyzing C model in C++, we were seeing some SKIP function triggered by generated constructors/operators= for C structs.
In C they weren't present, but in C++ compiler generates them for us. To avoid this (and future) problems
with models, translate all functions that are needed when computing the model
Reviewed By: dulmarod
Differential Revision: D3561873
fbshipit-source-id: f8ad2a0
Summary:
Array types where the length is not statically known were represented
using fresh variables. This diff:
- Makes array type length optional, reducing the amount of work needed
for renaming, substitution, and normalization.
- Revises uses of array length so that the length component of a
Tarray type represents only the statically determined constant
length of an array type, and the length component of a Sizeof
expression represents the dynamically determined length of an array
value.
- Restricts the type of static lengths from a general expression
(Sil.exp) to an integer (Sil.Int.t), enforcing that static types are
constant. This in particular ensures that types contain no
variables, and so are invariant under operations such as renaming
and substitution.
- Removes the type substitution and renaming functions typ_sub,
typ_normalize, and typ_captured_ren. Now that array type lengths
are constant integers, all of these functions are the identity.
Reviewed By: cristianoc
Differential Revision: D3387343
fbshipit-source-id: b5db768
Summary:
Hardcoding `variable@` in Makefiles is Bad™ because it prevents the users from
overwriting them easily with `make variable="my custom value"`. The right way
to do it is thus:
```
variable = variable@
# then use $(variable) everywhere
```
This diff puts all the `variable = variable@` lines in Makefile.config.in, and
changes every occurrence of a `variable@` to `$(variable)` everywhere else.
I mostly automated generating this diff. Here are the steps I did:
- find out which `variable@`s we use:
find . -name 'Makefile*' -exec grep -e '@[^@ []\+@' -o -h \{\} \+ | sort | uniq > config_variables
- write this `replace.sh` script to replace every `variable@` with `$(variable)`:
```
#!/bin/sh
config_vars_file=$1
shift
for line in $(cat $config_vars_file); do
var=$(echo $line | tr -d @)
sed -i -e "s/$line/\$($var)/g" $@ > /dev/null
done
```
- run the script as such:
find . -name 'Makefile.*in' \( -not -wholename './Makefile.config.in' \) -exec ./replace.sh config_variables \{\} \+
- put all the `VARIABLE = VARIABLE@` lines in Makefile.config.in
- move all `Makefile.in` to `Makefile`, since they don't need to be generated by `./configure` anymore:
```
for i in $(find . -name 'Makefile.*in' \( -not -wholename './Makefile.config.in' \)); do \
rm $(dirname $i)/$(basename $i .in) && git mv $i $(dirname $i)/$(basename $i .in) ; \
done
```
- delete all Makefile except Makefile.config from configure.ac
- manually inspect and remove remaining instances of `VAR = $(VAR)` in makefiles, looking at the output of `git grep '^\(\w\+\) = $(\1)'`
Reviewed By: jberdine
Differential Revision: D3358379
fbshipit-source-id: 5d37f02
Summary:public
Create separate specs for C models compiled in C++. It will allow us to tweak behavior/names of certain
functions based on the compilation language (such as adding `std::` namespace in C++).
Reviewed By: jvillard
Differential Revision: D2938992
fb-gh-sync-id: 73902f8
shipit-source-id: 73902f8
Summary:
public
When building models, make was invoked explicitly with `make -j` rather
than with `$(MAKE)`. This prevented controlling parallelism from the
top-level make invocation.
Reviewed By: akotulski
Differential Revision: D2786812
fb-gh-sync-id: 7f6d58c
Summary:
public
Lines other than the first of multi-line comments in non-ocaml files
were flush right instead of aligned.
Reviewed By: jvillard
Differential Revision: D2739752
fb-gh-sync-id: c85f56e
Summary:
public
Use autoconf's detection of xcode-select to decide whether to build the ObjC
models or not.
Reviewed By: jeremydubreil
Differential Revision: D2703864
fb-gh-sync-id: e6dadca
Summary: @publicThe first argument of builtin calls in C gets translated twice, which is bad if the argument is a side-effecting expression like a function call.
Test Plan: Attached test previously reported a memory leak because the translation introduces an extra call to malloc(), now reports nothing.
Summary:
@public
Remove setjmp that is causing problems in the models in linux.
Will investigate and add it again later.
Test Plan: All the models are now created. In particular strcpy, strdup and a few others in the beginning of the file.
Andrzej Kotulski
Josh Berdine
Jules Villard
Dulma Churchill
Jeremy Dubreil
Dino Distefano
Cristiano Calcagno
Sam Blackshear
Open Source Synchronization