[lab] fix issues discovered during POPL tutorial

Summary: .

Reviewed By: ngorogiannis

Differential Revision: D13750261

fbshipit-source-id: 4ec935b99
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent 9bd1191669
commit 13e8c21bef

@ -54,9 +54,8 @@ RUN eval $(opam env) && \
SKIP_SUBMODULES=true ./autogen.sh && \ SKIP_SUBMODULES=true ./autogen.sh && \
./configure --disable-c-analyzers ./configure --disable-c-analyzers
# Install Infer # "Install" Infer. The tutorial assumes /infer-host is the working copy of infer so let's put it in the PATH too.
ENV INFER_HOME /infer/infer ENV PATH /infer-host/infer/bin:/infer/bin:$PATH
ENV PATH ${INFER_HOME}/bin:${PATH}
# build in non-optimized mode by default to speed up build times # build in non-optimized mode by default to speed up build times
ENV BUILD_MODE=default ENV BUILD_MODE=default
@ -66,3 +65,10 @@ ENV IGNOREEOF=9
# should be moved earlier # should be moved earlier
ENV INFER_OPAM_SWITCH=4.07.1 ENV INFER_OPAM_SWITCH=4.07.1
# export `opam env`
ENV OPAM_SWITCH_PREFIX=/root/.opam/4.07.1
ENV CAML_LD_LIBRARY_PATH=/root/.opam/4.07.1/lib/stublibs:/root/.opam/4.07.1/lib/ocaml/stublibs:/root/.opam/4.07.1/lib/ocaml
ENV OCAML_TOPLEVEL_PATH=/root/.opam/4.07.1/lib/toplevel
ENV MANPATH=$MANPATH:/root/.opam/4.07.1/man
ENV PATH=/root/.opam/4.07.1/bin:$PATH

@ -14,13 +14,13 @@ Using Docker is the fastest way: you do not need to clone the Infer repository a
2. Run the infer Docker image with `docker run -it -v $HOME/infer-docker:/infer-host infer/infer:infer-latest-java-dev /bin/bash`. This will give you a prompt *inside the Docker image*. Do not close that terminal for the duration of the lab. 2. Run the infer Docker image with `docker run -it -v $HOME/infer-docker:/infer-host infer/infer:infer-latest-java-dev /bin/bash`. This will give you a prompt *inside the Docker image*. Do not close that terminal for the duration of the lab.
3. Within Docker, pull the latest version of infer, copy the /infer directory to your mount point, then set up the opam environment for OCaml: 3. Within Docker, pull the latest version of infer, copy the /infer directory to your mount point, then fully build infer once:
```shell ```shell
cd /infer cd /infer
git pull git pull
cp -av /infer/. /infer-host cp -av /infer/. /infer-host
eval $(opam env) make -C /infer-host -j 4
``` ```
4. Outside Docker, you will likely need to change the permissions of `$HOME/infer-docker` to make the files editable by your user: `sudo chown $USER -R $HOME/infer-docker`. 4. Outside Docker, you will likely need to change the permissions of `$HOME/infer-docker` to make the files editable by your user: `sudo chown $USER -R $HOME/infer-docker`.
@ -37,10 +37,10 @@ See [CONTRIBUTING.md](https://github.com/facebook/infer/blob/master/CONTRIBUTING
## (1) Warm up: running, testing, and debugging Infer ## (1) Warm up: running, testing, and debugging Infer
(a) Change to the test directory (`cd infer/tests/codetoanalyze/java/lab`) and run infer: (a) Change to the test directory (`cd infer/tests/codetoanalyze/java/lab`) and run infer in its default configuration:
``` ```
infer --resource-leak-only -- javac Leaks.java infer -- javac Leaks.java
``` ```
Infer should report 7 resource leaks. These reports come from the separation logic based biabduction analysis. Infer should report 7 resource leaks. These reports come from the separation logic based biabduction analysis.
@ -83,7 +83,7 @@ Finally, look again at the HTML debug output of infer on [Leaks.java](https://gi
```OCaml ```OCaml
let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in
let message = F.asprintf "Leaked %d resource(s)" ResourceLeakDomain.pp leak_count in let message = F.asprintf "Leaked %a resource(s)" ResourceLeakDomain.pp post in
Reporting.log_error summary ~loc:last_loc IssueType.resource_leak message Reporting.log_error summary ~loc:last_loc IssueType.resource_leak message
``` ```

Loading…
Cancel
Save