Reviewed By: jvillard Differential Revision: D13552198 fbshipit-source-id: b9be4dd2emaster
parent
0e5a902ac6
commit
7f70251eff
@ -0,0 +1,50 @@
|
||||
# Copyright (c) 2018-present, Facebook, Inc.
|
||||
#
|
||||
# This source code is licensed under the MIT license found in the
|
||||
# LICENSE file in the root directory of this source tree.
|
||||
|
||||
ROOT_DIR = ../../../..
|
||||
|
||||
include $(ROOT_DIR)/Makefile.config
|
||||
|
||||
LEVEL1_DIR = level1
|
||||
LEVEL2_DIR = $(LEVEL1_DIR)/level2
|
||||
LEVEL3_DIR = $(LEVEL2_DIR)/level3
|
||||
|
||||
LEVELS = LEVEL1 LEVEL2 LEVEL3
|
||||
TESTS = $(LEVELS:%=%_TEST)
|
||||
PRINTS = $(LEVELS:%=%_PRINT)
|
||||
CLEANS = $(LEVELS:%=%_CLEAN)
|
||||
REPLACES = $(LEVELS:%=%_REPLACE)
|
||||
|
||||
.PHONY: default
|
||||
default: print
|
||||
|
||||
.PHONY: $(TESTS)
|
||||
$(TESTS): %_TEST:
|
||||
$(QUIET)$(MAKE) -C $($*_DIR) test
|
||||
|
||||
.PHONY: test
|
||||
test: $(TESTS)
|
||||
|
||||
.PHONY: $(PRINTS)
|
||||
$(PRINTS): %_PRINT:
|
||||
$(QUIET)$(MAKE) -C $($*_DIR) print
|
||||
|
||||
.PHONY: print
|
||||
print: $(PRINTS)
|
||||
|
||||
.PHONY: $(CLEANS)
|
||||
$(CLEANS): %_CLEAN:
|
||||
$(QUIET)$(MAKE) -C $($*_DIR) clean
|
||||
$(QUIET)$(REMOVE) $($*_DIR)/*.o
|
||||
|
||||
.PHONY: clean
|
||||
clean: $(CLEANS)
|
||||
|
||||
.PHONY: $(REPLACES)
|
||||
$(REPLACES): %_REPLACE:
|
||||
$(QUIET)$(MAKE) -C $($*_DIR) replace
|
||||
|
||||
.PHONY: replace
|
||||
replace: $(REPLACES)
|
@ -0,0 +1,12 @@
|
||||
# Copyright (c) 2018-present, Facebook, Inc.
|
||||
#
|
||||
# This source code is licensed under the MIT license found in the
|
||||
# LICENSE file in the root directory of this source tree.
|
||||
|
||||
CLANG_OPTIONS = -c
|
||||
INFER_OPTIONS = --backtrack-level $(BACKTRACK_LEVEL)
|
||||
INFERPRINT_OPTIONS = --issues-tests
|
||||
|
||||
SOURCES = $(TESTS_DIR)/build_systems/backtrack_level/hello.c
|
||||
|
||||
include $(TESTS_DIR)/clang.make
|
@ -0,0 +1,13 @@
|
||||
/*
|
||||
* Copyright (c) 2015-present, Facebook, Inc.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*/
|
||||
|
||||
#include <stdlib.h>
|
||||
|
||||
void test() {
|
||||
int* s = NULL;
|
||||
*s = 42;
|
||||
}
|
@ -0,0 +1,9 @@
|
||||
# Copyright (c) 2018-present, Facebook, Inc.
|
||||
#
|
||||
# This source code is licensed under the MIT license found in the
|
||||
# LICENSE file in the root directory of this source tree.
|
||||
|
||||
TESTS_DIR = ../../..
|
||||
BACKTRACK_LEVEL = 1
|
||||
|
||||
include $(TESTS_DIR)/build_systems/backtrack_level/backtrack_level.make
|
@ -0,0 +1 @@
|
||||
../hello.c, test, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure test()]
|
@ -0,0 +1,9 @@
|
||||
# Copyright (c) 2018-present, Facebook, Inc.
|
||||
#
|
||||
# This source code is licensed under the MIT license found in the
|
||||
# LICENSE file in the root directory of this source tree.
|
||||
|
||||
TESTS_DIR = ../../../..
|
||||
BACKTRACK_LEVEL = 2
|
||||
|
||||
include $(TESTS_DIR)/build_systems/backtrack_level/backtrack_level.make
|
@ -0,0 +1 @@
|
||||
../../hello.c, test, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure test()]
|
@ -0,0 +1,9 @@
|
||||
# Copyright (c) 2018-present, Facebook, Inc.
|
||||
#
|
||||
# This source code is licensed under the MIT license found in the
|
||||
# LICENSE file in the root directory of this source tree.
|
||||
|
||||
TESTS_DIR = ../../../../..
|
||||
BACKTRACK_LEVEL = 3
|
||||
|
||||
include $(TESTS_DIR)/build_systems/backtrack_level/backtrack_level.make
|
@ -0,0 +1 @@
|
||||
../../../hello.c, test, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure test()]
|
Loading…
Reference in new issue