From 6899d444f27c1f434ade07565ab5d23a631ea753 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 27 Oct 2023 15:10:48 +0300 Subject: [PATCH] Add --enable ana.sv-comp.functions to 20-race-2_1-container_of.c --- tests/regression/10-synch/20-race-2_1-container_of.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/10-synch/20-race-2_1-container_of.c b/tests/regression/10-synch/20-race-2_1-container_of.c index 6083cf4ca0..940649c43b 100644 --- a/tests/regression/10-synch/20-race-2_1-container_of.c +++ b/tests/regression/10-synch/20-race-2_1-container_of.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] thread --set ana.path_sens[+] threadflag +// PARAM: --set ana.activated[+] thread --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions #include #include #include @@ -60,7 +60,7 @@ int my_drv_probe(struct my_data *data) { ldv_assert(data->shared.a==0); // NORACE ldv_assert(data->shared.b==0); // NORACE - int res = __VERIFIER_nondet_int(); + int res = magic(); if(res) goto exit; //register callback