From 15049ddf99a3d62a024d3972d1522474617a779a Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 11 Dec 2023 11:26:32 +0100 Subject: [PATCH] Add option ana.modular.auto-funs to automatically detect which functions should be analyzed modularly. --- src/analyses/base.ml | 2 +- src/common/util/cilfacade.ml | 50 ++++++---- src/common/util/modularHeuristics.ml | 98 +++++++++++++++++++ src/common/util/options.schema.json | 14 +++ src/util/modularUtil0.ml | 7 +- tests/regression/79-modular/01-modular.c | 2 +- tests/regression/79-modular/02-start-state.c | 2 +- .../79-modular/03-heap-blocks-non-unique.c | 2 +- .../79-modular/04-heap-pointers_maybe_null.c | 2 +- .../regression/79-modular/06-global_values.c | 2 +- .../79-modular/07-global_addresses.c | 2 +- .../08-global_addresses_and_values.c | 2 +- .../regression/79-modular/09-function-calls.c | 2 +- .../79-modular/10-shared-block-vals-top.c | 2 +- tests/regression/79-modular/13-lists.c | 2 +- tests/regression/79-modular/14-recursion.c | 2 +- tests/regression/79-modular/15-return.c | 2 +- .../79-modular/16-return-local-pointer.c | 2 +- .../79-modular/17-call-modifying-function.c | 2 +- tests/regression/79-modular/18-non-pointers.c | 2 +- tests/regression/79-modular/19-arrays.c | 2 +- tests/regression/79-modular/20-arrays-top.c | 2 +- .../21-call-global-modifying-function.c | 2 +- ...-call-global-modifying-function-with-ptr.c | 2 +- .../regression/79-modular/23-callee-writes.c | 2 +- .../79-modular/24-assign-at-function-call.c | 2 +- .../regression/79-modular/25-malloced-block.c | 2 +- .../79-modular/26-return-allocated-simple.c | 2 +- .../79-modular/27-return-allocated.c | 2 +- .../79-modular/28-return-void-allocated.c | 2 +- .../79-modular/29-partially-modular.c | 2 +- .../79-modular/30-accumulate-writes.c | 2 +- .../regression/79-modular/31-append-to-list.c | 2 +- tests/regression/79-modular/32-use-global.c | 2 +- .../regression/79-modular/33-multithreading.c | 2 +- .../79-modular/34-multithreading-mutexes.c | 2 +- ...5-multithreading-multiple-writes-wrapper.c | 2 +- .../79-modular/36-multithreading-no-wrapper.c | 2 +- .../37-multithreading-no-wrapper-simple.c | 2 +- .../regression/79-modular/38-modular-unions.c | 2 +- tests/regression/79-modular/42-termination.c | 2 +- .../79-modular/43-pointer-escaping.c | 2 +- tests/regression/79-modular/44-local-race.c | 2 +- tests/regression/79-modular/45-global-race.c | 2 +- .../regression/79-modular/46-global-no-race.c | 2 +- .../regression/79-modular/47-local-no-race.c | 2 +- .../79-modular/48-return-partially-modular.c | 2 +- tests/regression/79-modular/49-return-race.c | 2 +- .../79-modular/50-two-modualr-accesses.c | 2 +- .../79-modular/51-two-modular-returns.c | 2 +- .../79-modular/53-read-write-race.c | 2 +- .../54-read-write-race-assignment-lval.c | 2 +- .../55-read-write-race-assignment-rval.c | 2 +- .../56-read-write-race-function-call.c | 2 +- .../regression/79-modular/57-local-escaping.c | 2 +- .../58-escaped-local-pointer-comparison.c | 2 +- .../79-modular/59-write-to-escaped-local.c | 2 +- .../79-modular/60-global-in-condition.c | 2 +- tests/regression/79-modular/61-auto-modular.c | 27 +++++ 59 files changed, 229 insertions(+), 75 deletions(-) create mode 100644 src/common/util/modularHeuristics.ml create mode 100644 tests/regression/79-modular/61-auto-modular.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 6cf0fe69e5..9525a58b66 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -3071,7 +3071,7 @@ let after_config () = (* add ~dep:["expRelation"] after modifying test cases accordingly *) let dep = let base_dependencies = ["mallocWrapper"] in - let modular_dependencies = if is_any_modular () then ["modular_queries"; "is_modular"; "written"; "used_globals"] else [] in + let modular_dependencies = if get_bool "modular" then ["modular_queries"; "is_modular"; "written"; "used_globals"] else [] in base_dependencies @ modular_dependencies in MCP.register_analysis ~dep (module Main : MCPSpec) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index eccca829c6..e8c383ae7e 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -155,12 +155,40 @@ let is_exit = in_section (fun s -> s = ".exit.text") type startfuns = fundec list * fundec list * fundec list +module VarinfoH = Hashtbl.Make (CilType.Varinfo) + +let varinfo_fundecs: fundec VarinfoH.t ResettableLazy.t = + ResettableLazy.from_fun (fun () -> + let h = VarinfoH.create 111 in + iterGlobals !current_file (function + | GFun (fd, _) -> + VarinfoH.replace h fd.svar fd + | _ -> () + ); + h + ) + +(** Find [fundec] by the function's [varinfo] (has the function name and type). *) +let find_varinfo_fundec vi = VarinfoH.find (ResettableLazy.force varinfo_fundecs) vi (* vi argument must be explicit, otherwise force happens immediately *) + +let find_varinfo_fundec_option f = + match find_varinfo_fundec f with + | v -> Some v + | exception Not_found -> None + + +module StringSet = BatSet.Make (String) let getFuns fileAST : startfuns = let add_main f (m,e,o) = (f::m,e,o) in let add_exit f (m,e,o) = (m,f::e,o) in let add_other f (m,e,o) = (m,e,f::o) in - let modular_funs = get_string_list "ana.modular.funs" in - let only_modular_funs = get_bool "modular" && not (modular_funs = []) in + + let modular_funs = StringSet.of_list (get_string_list "ana.modular.funs") in + ModularHeuristics.compute_auto_modular_funs find_varinfo_fundec_option fileAST; + let auto_modular_functions = ModularHeuristics.auto_modular_funs () in + let modular_funs = StringSet.union modular_funs auto_modular_functions in + let only_modular_funs = get_bool "ana.modular.only" in + let f acc glob = match glob with | GFun({svar={vname=mn; _}; _} as def,_) when List.mem mn (get_string_list "mainfun") && not only_modular_funs -> add_main def acc @@ -172,7 +200,7 @@ let getFuns fileAST : startfuns = Printf.printf "Cleanup function: %s\n" mn; set_string "exitfun[+]" mn; add_exit def acc | GFun ({svar={vstorage=NoStorage; vattr; _}; _} as def, _) when get_bool "nonstatic" && not (Cil.hasAttribute "goblint_stub" vattr) -> add_other def acc | GFun ({svar={vattr; _}; _} as def, _) when get_bool "allfuns" && not (Cil.hasAttribute "goblint_stub" vattr) -> add_other def acc - | GFun ({svar={vattr; vname; _}; _} as def, _) when (get_bool "modular" && (not only_modular_funs || List.mem vname modular_funs)) && not (Cil.hasAttribute "goblint_stub" vattr) -> add_main def acc + | GFun ({svar={vattr; vname; _}; _} as def, _) when (get_bool "modular" && StringSet.mem vname modular_funs) && not (Cil.hasAttribute "goblint_stub" vattr) -> add_main def acc | _ -> acc in foldGlobals fileAST f ([],[],[]) @@ -542,22 +570,6 @@ let find_stmt_fundec stmt = with Not_found -> StmtH.find (ResettableLazy.force stmt_fundecs) stmt (* stmt argument must be explicit, otherwise force happens immediately *) -module VarinfoH = Hashtbl.Make (CilType.Varinfo) - -let varinfo_fundecs: fundec VarinfoH.t ResettableLazy.t = - ResettableLazy.from_fun (fun () -> - let h = VarinfoH.create 111 in - iterGlobals !current_file (function - | GFun (fd, _) -> - VarinfoH.replace h fd.svar fd - | _ -> () - ); - h - ) - -(** Find [fundec] by the function's [varinfo] (has the function name and type). *) -let find_varinfo_fundec vi = VarinfoH.find (ResettableLazy.force varinfo_fundecs) vi (* vi argument must be explicit, otherwise force happens immediately *) - module StringH = Hashtbl.Make (Printable.Strings) diff --git a/src/common/util/modularHeuristics.ml b/src/common/util/modularHeuristics.ml new file mode 100644 index 0000000000..3abd02c41a --- /dev/null +++ b/src/common/util/modularHeuristics.ml @@ -0,0 +1,98 @@ +open GoblintCil + +let contains_function_call_through_pointer (f : fundec) : bool = + let contains_call = ref false in + let visitor = object + inherit nopCilVisitor + + method! vinst (i : instr) : instr list visitAction = + match i with + | Call (_, Lval (Mem _, _), _, _, _) -> + (* TODO: Does this detect all calls via function pointer? *) + contains_call := true; + SkipChildren + (* Detect static call of pthread_create: *) + | Call (_, Lval (Var fptr, _), _, _, _) when fptr.vname = "pthread_create" -> + contains_call := true; + SkipChildren + | _ -> DoChildren + end in + ignore (visitCilFunction visitor f); + let result = !contains_call in + Printf.printf "contains_function_call_through_pointer: %s -> %b\n" f.svar.vname result; + result + +let collect_functions_without_call_through_pointers (file : file) : fundec list = + let functions_without_call_through_pointers = ref [] in + let visitor = object + inherit nopCilVisitor + + method! vfunc (f : fundec) : fundec visitAction = + if not (contains_function_call_through_pointer f) then + functions_without_call_through_pointers := f :: !functions_without_call_through_pointers; + SkipChildren + end in + visitCilFile visitor file; + !functions_without_call_through_pointers + +let get_called_functions (f : Cil.fundec) : Cil.varinfo list = + let called_functions = ref [] in + let visitor = object + inherit nopCilVisitor + + method! vinst (i : Cil.instr) : Cil.instr list visitAction = + match i with + | Call (_, Lval (Var fptr, _), _, _, _) when isFunctionType fptr.vtype -> + called_functions := fptr :: !called_functions; + SkipChildren + | _ -> DoChildren + end in + ignore (visitCilFunction visitor f); + !called_functions + + +(* TODO: Mark function that are passed to pthread_create as non-modular, or automatically analyze them non-modularly if they are created as threads *) +let collect_functions_without_function_pointers (find_varinfo_fundec) (file : Cil.file) : Cil.fundec list = + let functions_without_call_through_pointers = collect_functions_without_call_through_pointers file in + Printf.printf "functions_without_call_through_pointers: %s\n" (String.concat ", " (List.map (fun f -> f.svar.vname) functions_without_call_through_pointers)); + let only_good_callees (f: fundec) : bool = + let callees = get_called_functions f in + let callees = (List.map find_varinfo_fundec) callees in + Printf.printf "callees: %s\n" (String.concat ", " (List.map (fun f -> BatOption.map_default (fun f -> f.svar.vname) "None" f) callees)); + let is_good g = match g with + | None -> + (* Assume unknown functions do not spawn / execute function pointers *) + true + | Some g -> + List.mem g functions_without_call_through_pointers + in + let result = List.for_all is_good callees in + Printf.printf "only_good_callees: %s -> %b\n" f.svar.vname result; + result + in + let result = List.filter only_good_callees functions_without_call_through_pointers in + Printf.printf "functions_without_function_pointers: %s\n" (String.concat ", " (List.map (fun f -> f.svar.vname) result)); + result + +module StringSet = BatSet.Make(String) + +let auto_modular_funs = ref None + +let compute_auto_modular_funs (find_varinfo_fundec) (file : Cil.file) : unit = + let compute_and_set () = + let functions_without_function_pointers = collect_functions_without_function_pointers find_varinfo_fundec file in + let funs = List.map (fun f -> f.svar.vname) functions_without_function_pointers in + let funs = StringSet.of_list funs in + auto_modular_funs := Some funs + in + let set_to_empty () = + auto_modular_funs := Some StringSet.empty + in + if GobConfig.get_bool "ana.modular.auto-funs" then + compute_and_set () + else + set_to_empty () + +let auto_modular_funs () = match !auto_modular_funs with + | None -> failwith "auto_modular_functions not initialized" + | Some f -> f diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 7298e6dd88..206649d2d0 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -373,6 +373,20 @@ "type": "string" }, "default": [] + }, + "auto-funs": { + "title": "ana.modular.auto-funs", + "description": + "Automatically detect functions that are to be analayzed modularly.", + "type": "boolean", + "default": false + }, + "only": { + "title": "ana.modular.only", + "description": + "Only analyze functions that are to be analayzed modularly.", + "type": "boolean", + "default": false } }, "additionalProperties": false diff --git a/src/util/modularUtil0.ml b/src/util/modularUtil0.ml index 4123981575..d6b2c49f8a 100644 --- a/src/util/modularUtil0.ml +++ b/src/util/modularUtil0.ml @@ -23,6 +23,9 @@ let modular_funs () = match !modular_funs with | None -> let funs = get_string_list "ana.modular.funs" in let funs = StringSet.of_list funs in + let auto_funs = ModularHeuristics.auto_modular_funs () in + + let funs = StringSet.union funs auto_funs in modular_funs := Some funs; funs | Some funs -> @@ -32,10 +35,10 @@ let is_modular_fun f = let is_modular_fun f = StringSet.mem f (modular_funs ()) in - is_modular () || is_modular_fun f.vname + is_modular_fun f.vname let is_any_modular () = - is_modular () || not (StringSet.is_empty (modular_funs ())) + not (StringSet.is_empty (modular_funs ())) (** If [x] is global (but not a heap variable) and we are in ["modular"] mode, retrieves the varinfo_to_canonical for [x], else returns [x] itself *) let varinfo_or_canonical ~is_modular x = diff --git a/tests/regression/79-modular/01-modular.c b/tests/regression/79-modular/01-modular.c index ce698f8cd5..c2a886f6cf 100644 --- a/tests/regression/79-modular/01-modular.c +++ b/tests/regression/79-modular/01-modular.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include diff --git a/tests/regression/79-modular/02-start-state.c b/tests/regression/79-modular/02-start-state.c index ddbf042313..3b410293a4 100644 --- a/tests/regression/79-modular/02-start-state.c +++ b/tests/regression/79-modular/02-start-state.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include typedef struct node { diff --git a/tests/regression/79-modular/03-heap-blocks-non-unique.c b/tests/regression/79-modular/03-heap-blocks-non-unique.c index b866109f68..7595b5bee6 100644 --- a/tests/regression/79-modular/03-heap-blocks-non-unique.c +++ b/tests/regression/79-modular/03-heap-blocks-non-unique.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/04-heap-pointers_maybe_null.c b/tests/regression/79-modular/04-heap-pointers_maybe_null.c index e05724d69d..449c5cbaff 100644 --- a/tests/regression/79-modular/04-heap-pointers_maybe_null.c +++ b/tests/regression/79-modular/04-heap-pointers_maybe_null.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/06-global_values.c b/tests/regression/79-modular/06-global_values.c index b194b98ff5..846d63e069 100644 --- a/tests/regression/79-modular/06-global_values.c +++ b/tests/regression/79-modular/06-global_values.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/07-global_addresses.c b/tests/regression/79-modular/07-global_addresses.c index 18d52d1b2a..7d4c314dd2 100644 --- a/tests/regression/79-modular/07-global_addresses.c +++ b/tests/regression/79-modular/07-global_addresses.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include typedef struct node { diff --git a/tests/regression/79-modular/08-global_addresses_and_values.c b/tests/regression/79-modular/08-global_addresses_and_values.c index 8edc9fba0b..0160cf43af 100644 --- a/tests/regression/79-modular/08-global_addresses_and_values.c +++ b/tests/regression/79-modular/08-global_addresses_and_values.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/09-function-calls.c b/tests/regression/79-modular/09-function-calls.c index f75a269ed4..76cb94a6c9 100644 --- a/tests/regression/79-modular/09-function-calls.c +++ b/tests/regression/79-modular/09-function-calls.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['modify_x', 'modify_y']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['modify_x', 'modify_y']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #define X_VALUE 12 diff --git a/tests/regression/79-modular/10-shared-block-vals-top.c b/tests/regression/79-modular/10-shared-block-vals-top.c index 1bf54530f8..e4be6a51fb 100644 --- a/tests/regression/79-modular/10-shared-block-vals-top.c +++ b/tests/regression/79-modular/10-shared-block-vals-top.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" typedef struct { int x; diff --git a/tests/regression/79-modular/13-lists.c b/tests/regression/79-modular/13-lists.c index bfa6c4d6b5..b31579e02c 100644 --- a/tests/regression/79-modular/13-lists.c +++ b/tests/regression/79-modular/13-lists.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['prepend', 'prepend2']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['prepend', 'prepend2']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/14-recursion.c b/tests/regression/79-modular/14-recursion.c index 140ff944c6..3e78fde82e 100644 --- a/tests/regression/79-modular/14-recursion.c +++ b/tests/regression/79-modular/14-recursion.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['fib']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['fib']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include diff --git a/tests/regression/79-modular/15-return.c b/tests/regression/79-modular/15-return.c index 2638ca12bf..6a1925ebda 100644 --- a/tests/regression/79-modular/15-return.c +++ b/tests/regression/79-modular/15-return.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/16-return-local-pointer.c b/tests/regression/79-modular/16-return-local-pointer.c index 0dc4970357..af62ee20a2 100644 --- a/tests/regression/79-modular/16-return-local-pointer.c +++ b/tests/regression/79-modular/16-return-local-pointer.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" int *identity(int *p){ return p; diff --git a/tests/regression/79-modular/17-call-modifying-function.c b/tests/regression/79-modular/17-call-modifying-function.c index 964b97bcc9..abd52afb6c 100644 --- a/tests/regression/79-modular/17-call-modifying-function.c +++ b/tests/regression/79-modular/17-call-modifying-function.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['change_param', 'call_change_param']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['change_param', 'call_change_param']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include void change_param(int* p){ diff --git a/tests/regression/79-modular/18-non-pointers.c b/tests/regression/79-modular/18-non-pointers.c index 6a641bcfb8..67a2eb1634 100644 --- a/tests/regression/79-modular/18-non-pointers.c +++ b/tests/regression/79-modular/18-non-pointers.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['write_into_array']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['write_into_array']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" void write_into_array(int *a, int value){ *a = value; diff --git a/tests/regression/79-modular/19-arrays.c b/tests/regression/79-modular/19-arrays.c index ffbbdc770a..acb9c08890 100644 --- a/tests/regression/79-modular/19-arrays.c +++ b/tests/regression/79-modular/19-arrays.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" void write_into_array(int *a, int size){ a[size - 1] = 123; diff --git a/tests/regression/79-modular/20-arrays-top.c b/tests/regression/79-modular/20-arrays-top.c index 8be8fb0384..97c4a80cc7 100644 --- a/tests/regression/79-modular/20-arrays-top.c +++ b/tests/regression/79-modular/20-arrays-top.c @@ -1,4 +1,4 @@ -//SKIP PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//SKIP PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/21-call-global-modifying-function.c b/tests/regression/79-modular/21-call-global-modifying-function.c index 936f31e090..6640611aae 100644 --- a/tests/regression/79-modular/21-call-global-modifying-function.c +++ b/tests/regression/79-modular/21-call-global-modifying-function.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/22-call-global-modifying-function-with-ptr.c b/tests/regression/79-modular/22-call-global-modifying-function-with-ptr.c index 8ab235341d..10fce3c6dd 100644 --- a/tests/regression/79-modular/22-call-global-modifying-function-with-ptr.c +++ b/tests/regression/79-modular/22-call-global-modifying-function-with-ptr.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/23-callee-writes.c b/tests/regression/79-modular/23-callee-writes.c index 28e1b41bba..9513c4bfb0 100644 --- a/tests/regression/79-modular/23-callee-writes.c +++ b/tests/regression/79-modular/23-callee-writes.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['write_arg', 'delegate_writing']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['write_arg', 'delegate_writing']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include void write_arg(int *x){ diff --git a/tests/regression/79-modular/24-assign-at-function-call.c b/tests/regression/79-modular/24-assign-at-function-call.c index 70f8956883..186e08fdb5 100644 --- a/tests/regression/79-modular/24-assign-at-function-call.c +++ b/tests/regression/79-modular/24-assign-at-function-call.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['five', 'write_arg']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['five', 'write_arg']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include int five(){ diff --git a/tests/regression/79-modular/25-malloced-block.c b/tests/regression/79-modular/25-malloced-block.c index 8322f04fc4..8c3899f9c6 100644 --- a/tests/regression/79-modular/25-malloced-block.c +++ b/tests/regression/79-modular/25-malloced-block.c @@ -1,4 +1,4 @@ -//SKIP PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//SKIP PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/26-return-allocated-simple.c b/tests/regression/79-modular/26-return-allocated-simple.c index e9ec2287ce..49d17cc426 100644 --- a/tests/regression/79-modular/26-return-allocated-simple.c +++ b/tests/regression/79-modular/26-return-allocated-simple.c @@ -1,4 +1,4 @@ -//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/27-return-allocated.c b/tests/regression/79-modular/27-return-allocated.c index f5215406d1..e27f58d30c 100644 --- a/tests/regression/79-modular/27-return-allocated.c +++ b/tests/regression/79-modular/27-return-allocated.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['allocate_int', 'allocate_node', 'init_node', 'add_node']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['allocate_int', 'allocate_node', 'init_node', 'add_node']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/28-return-void-allocated.c b/tests/regression/79-modular/28-return-void-allocated.c index b0cfc5907f..64105cb5ba 100644 --- a/tests/regression/79-modular/28-return-void-allocated.c +++ b/tests/regression/79-modular/28-return-void-allocated.c @@ -1,4 +1,4 @@ -//SKIP PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//SKIP PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/29-partially-modular.c b/tests/regression/79-modular/29-partially-modular.c index e0417a558b..e646774813 100644 --- a/tests/regression/79-modular/29-partially-modular.c +++ b/tests/regression/79-modular/29-partially-modular.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include diff --git a/tests/regression/79-modular/30-accumulate-writes.c b/tests/regression/79-modular/30-accumulate-writes.c index bf898cc8d7..bf5bc26cf8 100644 --- a/tests/regression/79-modular/30-accumulate-writes.c +++ b/tests/regression/79-modular/30-accumulate-writes.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['append_new']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['append_new']" --set ana.modular.funs "['append_new']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/31-append-to-list.c b/tests/regression/79-modular/31-append-to-list.c index f63b49aff2..d8b1f091c2 100644 --- a/tests/regression/79-modular/31-append-to-list.c +++ b/tests/regression/79-modular/31-append-to-list.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['append_new']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['append_new']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/32-use-global.c b/tests/regression/79-modular/32-use-global.c index 4ea566899f..991d673b8b 100644 --- a/tests/regression/79-modular/32-use-global.c +++ b/tests/regression/79-modular/32-use-global.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['compare_to_global_addr', 'call_compare_to_global_addr']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['compare_to_global_addr', 'call_compare_to_global_addr']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/33-multithreading.c b/tests/regression/79-modular/33-multithreading.c index c79630b947..aa8587d369 100644 --- a/tests/regression/79-modular/33-multithreading.c +++ b/tests/regression/79-modular/33-multithreading.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['change_pointer', 'write_through_pointer']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['change_pointer', 'write_through_pointer']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include #include diff --git a/tests/regression/79-modular/34-multithreading-mutexes.c b/tests/regression/79-modular/34-multithreading-mutexes.c index feb7b0abbf..85102427ee 100644 --- a/tests/regression/79-modular/34-multithreading-mutexes.c +++ b/tests/regression/79-modular/34-multithreading-mutexes.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['change_pointer', 'write_through_pointer']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['change_pointer', 'write_through_pointer']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include #include diff --git a/tests/regression/79-modular/35-multithreading-multiple-writes-wrapper.c b/tests/regression/79-modular/35-multithreading-multiple-writes-wrapper.c index 0267e0af47..fc32c4542d 100644 --- a/tests/regression/79-modular/35-multithreading-multiple-writes-wrapper.c +++ b/tests/regression/79-modular/35-multithreading-multiple-writes-wrapper.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['change_pointer', 'write_through_pointer']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['change_pointer', 'write_through_pointer']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include #include diff --git a/tests/regression/79-modular/36-multithreading-no-wrapper.c b/tests/regression/79-modular/36-multithreading-no-wrapper.c index d742674105..a7c22625a0 100644 --- a/tests/regression/79-modular/36-multithreading-no-wrapper.c +++ b/tests/regression/79-modular/36-multithreading-no-wrapper.c @@ -1,4 +1,4 @@ -//SKIP PARAM: --set ana.modular.funs "['change_pointer', 'write_through_pointer']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//SKIP PARAM: --enable modular --set ana.modular.funs "['change_pointer', 'write_through_pointer']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include #include diff --git a/tests/regression/79-modular/37-multithreading-no-wrapper-simple.c b/tests/regression/79-modular/37-multithreading-no-wrapper-simple.c index 6e26d6c3c9..82328fbcef 100644 --- a/tests/regression/79-modular/37-multithreading-no-wrapper-simple.c +++ b/tests/regression/79-modular/37-multithreading-no-wrapper-simple.c @@ -1,4 +1,4 @@ -//SKIP PARAM: --set ana.modular.funs "['write_global']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//SKIP PARAM: --enable modular --set ana.modular.funs "['write_global']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include #include diff --git a/tests/regression/79-modular/38-modular-unions.c b/tests/regression/79-modular/38-modular-unions.c index 581882f75d..e80189b0f8 100644 --- a/tests/regression/79-modular/38-modular-unions.c +++ b/tests/regression/79-modular/38-modular-unions.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['write_node']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +// PARAM: --enable modular --set ana.modular.funs "['write_node']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include #include diff --git a/tests/regression/79-modular/42-termination.c b/tests/regression/79-modular/42-termination.c index ff454a6ecd..9c7d0ecc4c 100644 --- a/tests/regression/79-modular/42-termination.c +++ b/tests/regression/79-modular/42-termination.c @@ -1,4 +1,4 @@ -// PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['freadptrinc', 'freadseek']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" struct _IO_FILE { char *_IO_read_ptr; diff --git a/tests/regression/79-modular/43-pointer-escaping.c b/tests/regression/79-modular/43-pointer-escaping.c index 185157d04d..df9cabc510 100644 --- a/tests/regression/79-modular/43-pointer-escaping.c +++ b/tests/regression/79-modular/43-pointer-escaping.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['let_escape']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['let_escape']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/44-local-race.c b/tests/regression/79-modular/44-local-race.c index 3e5d928666..86f7f070da 100644 --- a/tests/regression/79-modular/44-local-race.c +++ b/tests/regression/79-modular/44-local-race.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/45-global-race.c b/tests/regression/79-modular/45-global-race.c index c48076ea31..918ae30448 100644 --- a/tests/regression/79-modular/45-global-race.c +++ b/tests/regression/79-modular/45-global-race.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/46-global-no-race.c b/tests/regression/79-modular/46-global-no-race.c index 21c5853bb2..2e927517a6 100644 --- a/tests/regression/79-modular/46-global-no-race.c +++ b/tests/regression/79-modular/46-global-no-race.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/47-local-no-race.c b/tests/regression/79-modular/47-local-no-race.c index 885c9a1ae1..684d996f3a 100644 --- a/tests/regression/79-modular/47-local-no-race.c +++ b/tests/regression/79-modular/47-local-no-race.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/48-return-partially-modular.c b/tests/regression/79-modular/48-return-partially-modular.c index 84c62c15d8..a5de39e9ec 100644 --- a/tests/regression/79-modular/48-return-partially-modular.c +++ b/tests/regression/79-modular/48-return-partially-modular.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval +//PARAM: --enable modular --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --enable ana.int.interval #include diff --git a/tests/regression/79-modular/49-return-race.c b/tests/regression/79-modular/49-return-race.c index 2e4c457a9e..07844fd16f 100644 --- a/tests/regression/79-modular/49-return-race.c +++ b/tests/regression/79-modular/49-return-race.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['value']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['value']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/50-two-modualr-accesses.c b/tests/regression/79-modular/50-two-modualr-accesses.c index 255820fa8c..70bc59bf3d 100644 --- a/tests/regression/79-modular/50-two-modualr-accesses.c +++ b/tests/regression/79-modular/50-two-modualr-accesses.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/51-two-modular-returns.c b/tests/regression/79-modular/51-two-modular-returns.c index b66d667b44..9d036c5eff 100644 --- a/tests/regression/79-modular/51-two-modular-returns.c +++ b/tests/regression/79-modular/51-two-modular-returns.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.modular.funs "['value']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +// PARAM: --enable modular --set ana.modular.funs "['value']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/53-read-write-race.c b/tests/regression/79-modular/53-read-write-race.c index 7791de2278..afab80cf83 100644 --- a/tests/regression/79-modular/53-read-write-race.c +++ b/tests/regression/79-modular/53-read-write-race.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['write', 'read']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['write', 'read']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include #include diff --git a/tests/regression/79-modular/54-read-write-race-assignment-lval.c b/tests/regression/79-modular/54-read-write-race-assignment-lval.c index bda83e64b7..fcfe964772 100644 --- a/tests/regression/79-modular/54-read-write-race-assignment-lval.c +++ b/tests/regression/79-modular/54-read-write-race-assignment-lval.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['write']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include #include diff --git a/tests/regression/79-modular/55-read-write-race-assignment-rval.c b/tests/regression/79-modular/55-read-write-race-assignment-rval.c index 38bf0c3710..1958dcceaf 100644 --- a/tests/regression/79-modular/55-read-write-race-assignment-rval.c +++ b/tests/regression/79-modular/55-read-write-race-assignment-rval.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['read']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['read']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include #include diff --git a/tests/regression/79-modular/56-read-write-race-function-call.c b/tests/regression/79-modular/56-read-write-race-function-call.c index 8b2af57eb1..a11b6a97aa 100644 --- a/tests/regression/79-modular/56-read-write-race-function-call.c +++ b/tests/regression/79-modular/56-read-write-race-function-call.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['access']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['access']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include #include diff --git a/tests/regression/79-modular/57-local-escaping.c b/tests/regression/79-modular/57-local-escaping.c index e07d008f64..c309568788 100644 --- a/tests/regression/79-modular/57-local-escaping.c +++ b/tests/regression/79-modular/57-local-escaping.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/58-escaped-local-pointer-comparison.c b/tests/regression/79-modular/58-escaped-local-pointer-comparison.c index 9ae414fd1e..6a5d9f136c 100644 --- a/tests/regression/79-modular/58-escaped-local-pointer-comparison.c +++ b/tests/regression/79-modular/58-escaped-local-pointer-comparison.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/59-write-to-escaped-local.c b/tests/regression/79-modular/59-write-to-escaped-local.c index d439b4d295..7f97fe0a6a 100644 --- a/tests/regression/79-modular/59-write-to-escaped-local.c +++ b/tests/regression/79-modular/59-write-to-escaped-local.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/60-global-in-condition.c b/tests/regression/79-modular/60-global-in-condition.c index c76b7067a9..2915e6de37 100644 --- a/tests/regression/79-modular/60-global-in-condition.c +++ b/tests/regression/79-modular/60-global-in-condition.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" +//PARAM: --enable modular --set ana.modular.funs "['foo']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" #include #include diff --git a/tests/regression/79-modular/61-auto-modular.c b/tests/regression/79-modular/61-auto-modular.c new file mode 100644 index 0000000000..7b2b20c2e2 --- /dev/null +++ b/tests/regression/79-modular/61-auto-modular.c @@ -0,0 +1,27 @@ +//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" + +#include + +int g; +int h; + +typedef int int_ptr_to_int(int*); + +int bar(int *i){ + __goblint_check(i == &g); //UNKNOWN + __goblint_check(i == &h); //UNKNOWN + return i; +} + +int foo(int_ptr_to_int *f){ + int *i = &g; + return f(i); +} + +int main(){ + foo(bar); +} + + + +