[pulse] model random(3)

Summary: Useful to write other tests, and also probably worth modelling.

Reviewed By: ezgicicek

Differential Revision: D29232545

fbshipit-source-id: ecb24f6f7
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent fb69d8aca1
commit 61ade247cd

@ -1572,6 +1572,7 @@ module ProcNameDispatcher = struct
<>$ capt_exp
$--> Misc.alloc_no_leak_not_null ~desc:"new"
; +BuiltinDecl.(match_builtin __placement_new) &++> Cplusplus.placement_new
; -"random" <>$$--> Misc.nondet ~fn_name:"random"
; +BuiltinDecl.(match_builtin objc_cpp_throw) <>--> Misc.early_exit
; +BuiltinDecl.(match_builtin __cast)
<>$ capt_arg_payload $+...$--> Misc.id_first_arg ~desc:"cast"

@ -29,6 +29,8 @@ codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_
codetoanalyze/c/pulse/memory_leak.c, return_malloc_deref_bad, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/nullptr.c, FNlatent_random_modelled_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, FP_arithmetic_weakness_ok, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
@ -38,6 +40,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, random_non_functional_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,parameter `z` of several_dereferences_ok,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, unknown_from_parameters_latent, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, unknown_with_different_values_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]

@ -32,6 +32,8 @@ codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_
codetoanalyze/c/pulse/memory_leak.c, return_malloc_deref_bad, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/nullptr.c, FNlatent_random_modelled_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, FP_arithmetic_weakness_ok, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
@ -41,6 +43,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, random_non_functional_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, unknown_from_parameters_latent, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, unknown_with_different_values_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]

@ -163,3 +163,30 @@ void unknown_from_parameters_latent(int x) {
*p = 42;
}
}
// is pruned away without the model
void random_non_functional_bad() {
if (random() != random()) {
int* p = NULL;
*p = 42;
}
}
// quantifier elimination not powerful enough to discard [\exists v. y = v] in
// the pruned part
void FNlatent_random_modelled_bad(int y) {
int x = random();
if (x == y) {
int* p = NULL;
*p = 42;
}
}
void FP_arithmetic_weakness_ok() {
int x = random();
int y = random();
if (x < y && x > y) {
int* p = NULL;
*p = 42;
}
}

Loading…
Cancel
Save