[erlang] test remote specs in topl

Summary: Adding tests to check topl properties from specs when specs are remote

Reviewed By: hajduakos

Differential Revision: D49454557

fbshipit-source-id: 31169dae523cb38bca5a585bbf6d250284fbcfdc

infer/tests/codetoanalyze/erlang/topl/specs/Makefile

@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../../..
 
-INFER_OPTIONS = --topl-only --topl-properties property.topl --erlang-check-return --enable-issue-type TOPL_ERROR_LATENTß --project-root $(TESTS_DIR)
+INFER_OPTIONS = --topl-only --topl-properties property.topl --erlang-check-return --enable-issue-type TOPL_ERROR_LATENT --project-root $(TESTS_DIR)
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.erl)

infer/tests/codetoanalyze/erlang/topl/specs/issues.exp

@@ -1,3 +1,6 @@
-specs.erl, test_arg1_Bad/1, 0, TOPL_ERROR, no_bucket, ERROR, [call to __infer_assume_type_dirty/1,call to sink/1]
-specs.erl, test_ret1_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to __infer_assume_type_dirty/1,call to sink/1]
-specs.erl, test_ret2_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to __infer_assume_type_dirty/1,call to sinksink/1,call to sink/1]
+codetoanalyze/erlang/topl/specs/remote_specs.erl, test_arg1_Bad/1, 0, TOPL_ERROR_LATENT, no_bucket, ERROR, [call to __infer_assume_type_dirty/1,call to sink/1]
+codetoanalyze/erlang/topl/specs/remote_specs.erl, test_ret1_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to __infer_assume_type_dirty/1,call to sink/1]
+codetoanalyze/erlang/topl/specs/remote_specs.erl, test_ret2_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to source/0,call to __infer_assume_type_dirty/1,call to sink/1]
+codetoanalyze/erlang/topl/specs/specs.erl, test_arg1_Bad/1, 0, TOPL_ERROR_LATENT, no_bucket, ERROR, [call to __infer_assume_type_dirty/1,call to sink/1]
+codetoanalyze/erlang/topl/specs/specs.erl, test_ret1_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to __infer_assume_type_dirty/1,call to sink/1]
+codetoanalyze/erlang/topl/specs/specs.erl, test_ret2_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to __infer_assume_type_dirty/1,call to sinksink/1,call to sink/1]

infer/tests/codetoanalyze/erlang/topl/specs/property.topl

@@ -1,4 +1,4 @@
 property SourceIsSpec
   start -> start: *
-  start -> track: ".*:__infer_assume_type_dirty/1"(Arg, Ret) when Ret != 0 => dirty := Arg
+  start -> track: "specs:__infer_assume_type_dirty/1"(Arg, Ret) when Ret != 0 => dirty := Arg
   track -> error: ".*:sink/1"(Arg, Ret) when Arg == dirty

infer/tests/codetoanalyze/erlang/topl/specs/remote_specs.erl

@@ -0,0 +1,33 @@
+% Copyright (c) Facebook, Inc. and its affiliates.
+%
+% This source code is licensed under the MIT license found in the
+% LICENSE file in the root directory of this source tree.
+-module(remote_specs).
+-export([
+    test_arg1_Bad/1,
+    test_arg2_Ok/1,
+    test_ret1_Bad/0,
+    test_ret2_Bad/0
+]).
+
+-type dirty() :: atom().
+
+-spec test_arg1_Bad(specs:dirty()) -> any().
+test_arg1_Bad(X) ->
+    sink(X).
+
+-spec test_arg2_Ok(dirty()) -> any().
+test_arg2_Ok(X) ->
+    sink(X).
+
+test_ret1_Bad() ->
+    sink(specs:source()).
+
+test_ret2_Bad() ->
+    sink(source()).
+
+-spec source() -> specs:dirty().
+source() ->
+    specs:source().
+
+sink(_) -> ok.

infer/tests/codetoanalyze/erlang/topl/specs/specs.erl

@@ -10,9 +10,12 @@
     test_ret1_Bad/0,
     test_ret2_Bad/0,
     test_ret3_Ok/0,
-    test_ret4_Ok/0
+    test_ret4_Ok/0,
+    source/0
 ]).
 
+-export_type([dirty/0]).
+
 -type dirty() :: atom().
 
 -spec test_arg1_Bad(dirty()) -> any().
@@ -44,6 +47,7 @@ sinksink(X) ->
 
 -spec source() -> dirty().
 source() -> dirty.
+
 sink(_) -> ok.
 
 nonsource() -> clean.