diff --git a/conf/svcomp.json b/conf/svcomp.json index 26ebdef14c..d945024cf2 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -1,8 +1,8 @@ { "ana": { "base": { - "partition-arrays": { - "enabled": true + "arrays": { + "domain": "partitioned" } }, "sv-comp": { @@ -69,4 +69,4 @@ "signed_overflow": "assume_none" } } -} +} \ No newline at end of file diff --git a/conf/svcomp21.json b/conf/svcomp21.json index 7fcbfbde14..2fd4cece64 100644 --- a/conf/svcomp21.json +++ b/conf/svcomp21.json @@ -1,10 +1,5 @@ { "ana": { - "base": { - "partition-arrays": { - "enabled": true - } - }, "sv-comp": { "enabled": true, "functions": true @@ -46,6 +41,11 @@ "kmalloc_array", "kcalloc" ] + }, + "base": { + "arrays": { + "domain": "partitioned" + } } }, "exp": { diff --git a/conf/svcomp22.json b/conf/svcomp22.json index aa3c4bdb5b..fbd32dd145 100644 --- a/conf/svcomp22.json +++ b/conf/svcomp22.json @@ -1,10 +1,5 @@ { "ana": { - "base": { - "partition-arrays": { - "enabled": true - } - }, "sv-comp": { "enabled": true, "functions": true @@ -46,6 +41,11 @@ "kmalloc_array", "kcalloc" ] + }, + "base": { + "arrays": { + "domain": "partitioned" + } } }, "exp": { diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml index 96042e6be3..3274b6bb6c 100644 --- a/src/cdomains/arrayDomain.ml +++ b/src/cdomains/arrayDomain.ml @@ -69,6 +69,94 @@ struct let update_length _ x = x end +module Unroll (Val: Lattice.S) (Idx:IntDomain.Z): S with type value = Val.t and type idx = Idx.t = +struct + module Factor = struct let x () = (get_int "ana.base.arrays.unrolling-factor") end + module Base = Lattice.ProdList (Val) (Factor) + include Lattice.ProdSimple(Base) (Val) + + let name () = "unrolled arrays" + type idx = Idx.t + type value = Val.t + let factor () = + match get_int "ana.base.arrays.unrolling-factor" with + | 0 -> failwith "ArrayDomain: ana.base.arrays.unrolling-factor needs to be set when using the unroll domain" + | x -> x + let join_of_all_parts (xl, xr) = List.fold_left Val.join xr xl + let show (xl, xr) = + let rec show_list xlist = match xlist with + | [] -> " --- " + | hd::tl -> (Val.show hd ^ " - " ^ (show_list tl)) in + "Array (unrolled to " ^ (Stdlib.string_of_int (factor ())) ^ "): " ^ + (show_list xl) ^ Val.show xr ^ ")" + let pretty () x = text "Array: " ++ text (show x) + let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y + let extract x = match x with + | Some c -> c + | None -> failwith "arrarDomain: that sould not happen" + let get (ask: Q.ask) (xl, xr) (_,i) = + let search_unrolled_values min_i max_i = + let mi = Z.to_int min_i in + let ma = Z.to_int max_i in + let rec subjoin l i = match l with + | [] -> Val.bot () + | hd::tl -> + begin + match i>ma,i subjoin tl (i+1) + | false,false -> Val.join hd (subjoin tl (i+1)) + | _,_ -> Val.bot () + end in + subjoin xl 0 in + let f = Z.of_int (factor ()) in + let min_i = extract (Idx.minimal i) in + let max_i = extract (Idx.maximal i) in + if Z.geq min_i f then xr + else if Z.lt max_i f then search_unrolled_values min_i max_i + else Val.join xr (search_unrolled_values min_i (Z.of_int ((factor ())-1))) + let set (ask: Q.ask) (xl,xr) (_,i) v = + let update_unrolled_values min_i max_i = + let mi = Z.to_int min_i in + let ma = Z.to_int max_i in + let rec weak_update l i = match l with + | [] -> [] + | hd::tl -> + if ima then (hd::tl) + else (Val.join hd v)::(weak_update tl (i+1)) in + let rec full_update l i = match l with + | [] -> [] + | hd::tl -> + if i\n\n + unrolled array\n + xl\n%a\n\n + xm\n%a\n\n + \n" Base.printXml xl Val.printXml xr + let smart_join _ _ = join + let smart_widen _ _ = widen + let smart_leq _ _ = leq + let update_length _ x = x +end + (** Special signature so that we can use the _with_length functions from PartitionedWithLength but still match the interface * * defined for array domains *) module type SPartitioned = @@ -689,59 +777,121 @@ struct let to_yojson (x, y) = `Assoc [ (Base.name (), Base.to_yojson x); ("length", Idx.to_yojson y) ] end +module UnrollWithLength (Val: Lattice.S) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t = +struct + module Base = Unroll (Val) (Idx) + include Lattice.Prod (Base) (Idx) + type idx = Idx.t + type value = Val.t + + let get (ask : Q.ask) (x, (l : idx)) ((e: ExpDomain.t), v) = + (array_oob_check (module Idx) (x, l) (e, v)); + Base.get ask x (e, v) + let set (ask: Q.ask) (x,l) i v = Base.set ask x i v, l + let make l x = Base.make l x, l + let length (_,l) = Some l + + let move_if_affected ?(replace_with_const=false) _ x _ _ = x + let map f (x, l):t = (Base.map f x, l) + let fold_left f a (x, l) = Base.fold_left f a x + let fold_left2 f a (x, l) (y, l) = Base.fold_left2 f a x y + let get_vars_in_e _ = [] + + let smart_join _ _ = join + let smart_widen _ _ = widen + let smart_leq _ _ = leq + + (* It is not necessary to do a least-upper bound between the old and the new length here. *) + (* Any array can only be declared in one location. The value for newl that we get there is *) + (* the one obtained by abstractly evaluating the size expression at this location for the *) + (* current state. If newl leq l this means that we somehow know more about the expression *) + (* determining the size now (e.g. because of narrowing), but this holds for all the times *) + (* the declaration is visited. *) + let update_length newl (x, l) = (x, newl) + + let printXml f (x,y) = + BatPrintf.fprintf f "\n\n\n%s\n\n%a\n%s\n\n%a\n\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y + + let to_yojson (x, y) = `Assoc [ (Base.name (), Base.to_yojson x); ("length", Idx.to_yojson y) ] +end + module FlagConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t = struct module P = PartitionedWithLength(Val)(Idx) module T = TrivialWithLength(Val)(Idx) + module U = UnrollWithLength(Val)(Idx) type idx = Idx.t type value = Val.t - include LatticeFlagHelper(P)(T)(struct - let msg = "FlagConfiguredArrayDomain received a value where not exactly one component is set" - let name = "FlagConfiguredArrayDomain" - end) + module K = struct + let msg = "FlagConfiguredArrayDomain received a value where not exactly one component is set" + let name = "FlagConfiguredArrayDomain" + end + + let to_t = function + | (Some p, None, None) -> (Some p, None) + | (None, Some t, None) -> (None, Some (Some t, None)) + | (None, None, Some u) -> (None, Some (None, Some u)) + | _ -> failwith "FlagConfiguredArrayDomain received a value where not exactly one component is set" + + module I = struct include LatticeFlagHelper (T) (U) (K) let name () = "" end + include LatticeFlagHelper (P) (I) (K) + + let binop' opp opt opu = binop opp (I.binop opt opu) + let unop' opp opt opu = unop opp (I.unop opt opu) + let binop_to_t' opp opt opu = binop_to_t opp (I.binop_to_t opt opu) + let unop_to_t' opp opt opu = unop_to_t opp (I.unop_to_t opt opu) (* Simply call appropriate function for component that is not None *) - let get a x (e,i) = unop (fun x -> - if e = `Top then - let e' = BatOption.map_default (fun x -> `Lifted (Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) x)) (`Top) (Idx.to_int i) in - P.get a x (e', i) - else - P.get a x (e, i) - ) (fun x -> T.get a x (e,i)) x - let set (ask:Q.ask) x i a = unop_to_t (fun x -> P.set ask x i a) (fun x -> T.set ask x i a) x - let length = unop P.length T.length - let get_vars_in_e = unop P.get_vars_in_e T.get_vars_in_e - let map f = unop_to_t (P.map f) (T.map f) - let fold_left f s = unop (P.fold_left f s) (T.fold_left f s) - let fold_left2 f s = binop (P.fold_left2 f s) (T.fold_left2 f s) - let move_if_affected ?(replace_with_const=false) (ask:Q.ask) x v f = unop_to_t (fun x -> P.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> T.move_if_affected ~replace_with_const:replace_with_const ask x v f) x - let smart_join f g = binop_to_t (P.smart_join f g) (T.smart_join f g) - let smart_widen f g = binop_to_t (P.smart_widen f g) (T.smart_widen f g) - let smart_leq f g = binop (P.smart_leq f g) (T.smart_leq f g) - let update_length newl x = unop_to_t (P.update_length newl) (T.update_length newl) x + let get a x (e,i) = unop' (fun x -> + if e = `Top then + let e' = BatOption.map_default (fun x -> `Lifted (Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) x)) (`Top) (Idx.to_int i) in + P.get a x (e', i) + else + P.get a x (e, i) + ) (fun x -> T.get a x (e,i)) (fun x -> U.get a x (e,i)) x + let set (ask:Q.ask) x i a = unop_to_t' (fun x -> P.set ask x i a) (fun x -> T.set ask x i a) (fun x -> U.set ask x i a) x + let length = unop' P.length T.length U.length + let map f = unop_to_t' (P.map f) (T.map f) (U.map f) + let fold_left f s = unop' (P.fold_left f s) (T.fold_left f s) (U.fold_left f s) + let fold_left2 f s = binop' (P.fold_left2 f s) (T.fold_left2 f s) (U.fold_left2 f s) + + let move_if_affected ?(replace_with_const=false) (ask:Q.ask) x v f = unop_to_t' (fun x -> P.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> T.move_if_affected ~replace_with_const:replace_with_const ask x v f) + (fun x -> U.move_if_affected ~replace_with_const:replace_with_const ask x v f) x + let get_vars_in_e = unop' P.get_vars_in_e T.get_vars_in_e U.get_vars_in_e + let smart_join f g = binop_to_t' (P.smart_join f g) (T.smart_join f g) (U.smart_join f g) + let smart_widen f g = binop_to_t' (P.smart_widen f g) (T.smart_widen f g) (U.smart_widen f g) + let smart_leq f g = binop' (P.smart_leq f g) (T.smart_leq f g) (U.smart_leq f g) + let update_length newl x = unop_to_t' (P.update_length newl) (T.update_length newl) (U.update_length newl) x (* Functions that make use of the configuration flag *) - let name () = "FlagConfiguredArrayDomain: " ^ if get_bool "ana.base.partition-arrays.enabled" then P.name () else T.name () + let chosen_domain () = get_string "ana.base.arrays.domain" - let partition_enabled () = get_bool "ana.base.partition-arrays.enabled" + let name () = "FlagConfiguredArrayDomain: " ^ match chosen_domain () with + | "trivial" -> T.name () + | "partitioned" -> P.name () + | "unroll" -> U.name () + | _ -> failwith "FlagConfiguredArrayDomain cannot name an array from set option" let bot () = - if partition_enabled () then - (Some (P.bot ()), None) - else - (None, Some (T.bot ())) + to_t @@ match chosen_domain () with + | "partitioned" -> (Some (P.bot ()), None, None) + | "trivial" -> (None, Some (T.bot ()), None) + | "unroll" -> (None, None, Some (U.bot ())) + | _ -> failwith "FlagConfiguredArrayDomain cannot construct a bot array from set option" let top () = - if partition_enabled () then - (Some (P.top ()), None) - else - (None, Some (T.top ())) + to_t @@ match chosen_domain () with + | "partitioned" -> (Some (P.top ()), None, None) + | "trivial" -> (None, Some (T.top ()), None) + | "unroll" -> (None, None, Some (U.top ())) + | _ -> failwith "FlagConfiguredArrayDomain cannot construct a top array from set option" let make i v = - if partition_enabled () then - (Some (P.make i v), None) - else - (None, Some (T.make i v)) + to_t @@ match chosen_domain () with + | "partitioned" -> (Some (P.make i v), None, None) + | "trivial" -> (None, Some (T.make i v), None) + | "unroll" -> (None, None, Some (U.make i v)) + | _ -> failwith "FlagConfiguredArrayDomain cannot construct an array from set option" end diff --git a/src/cdomains/arrayDomain.mli b/src/cdomains/arrayDomain.mli index 09d3609a18..b23263beef 100644 --- a/src/cdomains/arrayDomain.mli +++ b/src/cdomains/arrayDomain.mli @@ -76,4 +76,4 @@ module PartitionedWithLength (Val: LatticeWithSmartOps) (Idx:IntDomain.Z): S wit (** Like partitioned but additionally manages the length of the array. *) module FlagConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t -(** Switches between PartitionedWithLength and TrivialWithLength based on the value of ana.base.partition-arrays. *) +(** Switches between PartitionedWithLength, TrivialWithLength and Unroll based on the value of ana.base.arrays.domain. *) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index afae1c004c..1a63b31551 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -148,10 +148,10 @@ struct | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value fd.ftype) ci) | TComp ({cstruct=false; _},_) -> `Union (Unions.top ()) | TArray (ai, None, _) -> - `Array (CArrays.make (IndexDomain.bot ()) (if get_bool "ana.base.partition-arrays.enabled" then (init_value ai) else (bot_value ai))) + `Array (CArrays.make (IndexDomain.bot ()) (if (get_string "ana.base.arrays.domain"="partitioned" || get_string "ana.base.arrays.domain"="unroll") then (init_value ai) else (bot_value ai))) | TArray (ai, Some exp, _) -> let l = BatOption.map Cilint.big_int_of_cilint (Cil.getInteger (Cil.constFold true exp)) in - `Array (CArrays.make (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.bot ()) l) (if get_bool "ana.base.partition-arrays.enabled" then (init_value ai) else (bot_value ai))) + `Array (CArrays.make (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.bot ()) l) (if (get_string "ana.base.arrays.domain"="partitioned" || get_string "ana.base.arrays.domain"="unroll") then (init_value ai) else (bot_value ai))) (* | t when is_thread_type t -> `Thread (ConcDomain.ThreadSet.empty ()) *) | TNamed ({ttype=t; _}, _) -> init_value t | _ -> `Top @@ -163,10 +163,10 @@ struct | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> top_value fd.ftype) ci) | TComp ({cstruct=false; _},_) -> `Union (Unions.top ()) | TArray (ai, None, _) -> - `Array (CArrays.make (IndexDomain.top ()) (if get_bool "ana.base.partition-arrays.enabled" then (top_value ai) else (bot_value ai))) + `Array (CArrays.make (IndexDomain.top ()) (if (get_string "ana.base.arrays.domain"="partitioned" || get_string "ana.base.arrays.domain"="unroll") then (top_value ai) else (bot_value ai))) | TArray (ai, Some exp, _) -> let l = BatOption.map Cilint.big_int_of_cilint (Cil.getInteger (Cil.constFold true exp)) in - `Array (CArrays.make (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.top_of (Cilfacade.ptrdiff_ikind ())) l) (if get_bool "ana.base.partition-arrays.enabled" then (top_value ai) else (bot_value ai))) + `Array (CArrays.make (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.top_of (Cilfacade.ptrdiff_ikind ())) l) (if (get_string "ana.base.arrays.domain"="partitioned" || get_string "ana.base.arrays.domain"="unroll") then (top_value ai) else (bot_value ai))) | TNamed ({ttype=t; _}, _) -> top_value t | _ -> `Top diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml index c986949d53..5f0a1ab9cc 100644 --- a/src/domains/lattice.ml +++ b/src/domains/lattice.ml @@ -581,6 +581,29 @@ struct Pretty.dprintf "%a not leq %a" pretty x pretty y end +module type Num = sig val x : unit -> int end +module ProdList (Base: S) (N: Num) = +struct + include Printable.Liszt (Base) + + let bot () = BatList.make (N.x ()) (Base.bot ()) + let is_bot = List.for_all Base.is_bot + let top () = BatList.make (N.x ()) (Base.top ()) + let is_top = List.for_all Base.is_top + + let leq = + let f acc x y = Base.leq x y && acc in + List.fold_left2 f true + + let join = List.map2 Base.join + let widen = List.map2 Base.widen + let meet = List.map2 Base.meet + let narrow = List.map2 Base.narrow + + let pretty_diff () ((x:t),(y:t)): Pretty.doc = + Pretty.dprintf "%a not leq %a" pretty x pretty y +end + module Chain (P: Printable.ChainParams) = struct include Printable.Std diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 668857c705..c6fe54565b 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -624,13 +624,6 @@ "title": "ana.base.partition-arrays", "type": "object", "properties": { - "enabled": { - "title": "ana.base.partition-arrays.enabled", - "description": - "Employ the partitioning array domain. When this is on, make sure to enable the expRelation analysis as well.", - "type": "boolean", - "default": false - }, "keep-expr": { "title": "ana.base.partition-arrays.keep-expr", "description": @@ -656,6 +649,27 @@ }, "additionalProperties": false }, + "arrays":{ + "title": "ana.base.arrays", + "type": "object", + "properties": { + "domain": { + "title": "ana.base.arrays.domain", + "description": + "The domain that should be used for arrays. When employing the partition array domain, make sure to enable the expRelation analysis as well. When employing the unrolling array domain, make sure to set the ana.base.arrays.unrolling-factor >0.", + "type": "string", + "enum": ["trivial", "partitioned", "unroll"], + "default": "trivial" + }, + "unrolling-factor": { + "title": "ana.base.arrays.unrolling-factor", + "description": "Indicates how many values will the unrolled part of the unrolled array domain contain.", + "type": "integer", + "default": 0 + } + }, + "additionalProperties": false + }, "structs": { "title": "ana.base.structs", "type": "object", diff --git a/tests/regression/01-cpa/51-marshal.c b/tests/regression/01-cpa/51-marshal.c index 9922370637..c2b0c25c32 100644 --- a/tests/regression/01-cpa/51-marshal.c +++ b/tests/regression/01-cpa/51-marshal.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper']" --set ana.base.privatization none void callee(int j) { j++; } diff --git a/tests/regression/02-base/35-calloc_array.c b/tests/regression/02-base/35-calloc_array.c index 049c725ef1..7d63e733cb 100644 --- a/tests/regression/02-base/35-calloc_array.c +++ b/tests/regression/02-base/35-calloc_array.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/02-base/36-calloc_struct.c b/tests/regression/02-base/36-calloc_struct.c index ce290c173b..b99a03c367 100644 --- a/tests/regression/02-base/36-calloc_struct.c +++ b/tests/regression/02-base/36-calloc_struct.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/02-base/37-calloc_glob.c b/tests/regression/02-base/37-calloc_glob.c index 531972ee5c..8637746883 100644 --- a/tests/regression/02-base/37-calloc_glob.c +++ b/tests/regression/02-base/37-calloc_glob.c @@ -1,6 +1,6 @@ // Made after 02 22 -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/02-base/38-calloc_int.c b/tests/regression/02-base/38-calloc_int.c index ecd2cbb7ed..496ea6e6fb 100644 --- a/tests/regression/02-base/38-calloc_int.c +++ b/tests/regression/02-base/38-calloc_int.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/02-base/39-calloc_matrix.c b/tests/regression/02-base/39-calloc_matrix.c index fa7ca9cc7c..3923f88983 100644 --- a/tests/regression/02-base/39-calloc_matrix.c +++ b/tests/regression/02-base/39-calloc_matrix.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/02-base/40-calloc_loop.c b/tests/regression/02-base/40-calloc_loop.c index 5e29f45533..99482f23b2 100644 --- a/tests/regression/02-base/40-calloc_loop.c +++ b/tests/regression/02-base/40-calloc_loop.c @@ -1,5 +1,5 @@ // Made after 02 21 -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/02-base/41-calloc_globmt.c b/tests/regression/02-base/41-calloc_globmt.c index 1b88d9d2b0..50ddba8622 100644 --- a/tests/regression/02-base/41-calloc_globmt.c +++ b/tests/regression/02-base/41-calloc_globmt.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include #include diff --git a/tests/regression/02-base/42-calloc_zero_init.c b/tests/regression/02-base/42-calloc_zero_init.c index 59ac4ac893..d8485defd0 100644 --- a/tests/regression/02-base/42-calloc_zero_init.c +++ b/tests/regression/02-base/42-calloc_zero_init.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/02-base/43-calloc_struct_array.c b/tests/regression/02-base/43-calloc_struct_array.c index e7a8b6e3d1..f8ff8eefc6 100644 --- a/tests/regression/02-base/43-calloc_struct_array.c +++ b/tests/regression/02-base/43-calloc_struct_array.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/02-base/44-malloc_array.c b/tests/regression/02-base/44-malloc_array.c index 6342cd218e..e9a48fd220 100644 --- a/tests/regression/02-base/44-malloc_array.c +++ b/tests/regression/02-base/44-malloc_array.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.int.interval true --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include diff --git a/tests/regression/10-synch/23-tid-partitioned-array.c b/tests/regression/10-synch/23-tid-partitioned-array.c index 832410589b..0f4942ec0e 100644 --- a/tests/regression/10-synch/23-tid-partitioned-array.c +++ b/tests/regression/10-synch/23-tid-partitioned-array.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] thread --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.activated[+] thread --set ana.base.arrays.domain partitioned #include void *t_fun(void *arg) { diff --git a/tests/regression/10-synch/24-tid-partitioned-array-global.c b/tests/regression/10-synch/24-tid-partitioned-array-global.c index a17aab2585..b61daed77f 100644 --- a/tests/regression/10-synch/24-tid-partitioned-array-global.c +++ b/tests/regression/10-synch/24-tid-partitioned-array-global.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] thread --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.activated[+] thread --set ana.base.arrays.domain partitioned #include pthread_t t_ids[10000]; diff --git a/tests/regression/22-partitioned_arrays/01-simple_array.c b/tests/regression/22-partitioned_arrays/01-simple_array.c index 865c9b4bf1..64e9c180ce 100644 --- a/tests/regression/22-partitioned_arrays/01-simple_array.c +++ b/tests/regression/22-partitioned_arrays/01-simple_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int global; int main(void) diff --git a/tests/regression/22-partitioned_arrays/02-pointers_array.c b/tests/regression/22-partitioned_arrays/02-pointers_array.c index 6fc533a2ad..1c3c1be970 100644 --- a/tests/regression/22-partitioned_arrays/02-pointers_array.c +++ b/tests/regression/22-partitioned_arrays/02-pointers_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { example1(); example2(); diff --git a/tests/regression/22-partitioned_arrays/03-multidimensional_arrays.c b/tests/regression/22-partitioned_arrays/03-multidimensional_arrays.c index 5d34c4aae1..5b33384685 100644 --- a/tests/regression/22-partitioned_arrays/03-multidimensional_arrays.c +++ b/tests/regression/22-partitioned_arrays/03-multidimensional_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { example1(); example2(); diff --git a/tests/regression/22-partitioned_arrays/04-nesting_arrays.c b/tests/regression/22-partitioned_arrays/04-nesting_arrays.c index e0ed134575..b3e956501f 100644 --- a/tests/regression/22-partitioned_arrays/04-nesting_arrays.c +++ b/tests/regression/22-partitioned_arrays/04-nesting_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none struct kala { int i; int a[5]; diff --git a/tests/regression/22-partitioned_arrays/05-adapted_from_01_09_array.c b/tests/regression/22-partitioned_arrays/05-adapted_from_01_09_array.c index d452b2e0df..32d0e1ca51 100644 --- a/tests/regression/22-partitioned_arrays/05-adapted_from_01_09_array.c +++ b/tests/regression/22-partitioned_arrays/05-adapted_from_01_09_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none #include #include diff --git a/tests/regression/22-partitioned_arrays/06-interprocedural.c b/tests/regression/22-partitioned_arrays/06-interprocedural.c index 2d3d2f2713..5cf403e09c 100644 --- a/tests/regression/22-partitioned_arrays/06-interprocedural.c +++ b/tests/regression/22-partitioned_arrays/06-interprocedural.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { example1(); example2(); diff --git a/tests/regression/22-partitioned_arrays/07-global_array.c b/tests/regression/22-partitioned_arrays/07-global_array.c index a655b2c553..e65757e79d 100644 --- a/tests/regression/22-partitioned_arrays/07-global_array.c +++ b/tests/regression/22-partitioned_arrays/07-global_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int global_array[50]; int main(void) { diff --git a/tests/regression/22-partitioned_arrays/08-unsupported.c b/tests/regression/22-partitioned_arrays/08-unsupported.c index eeb2483666..51a0ee6247 100644 --- a/tests/regression/22-partitioned_arrays/08-unsupported.c +++ b/tests/regression/22-partitioned_arrays/08-unsupported.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --disable exp.fast_global_inits --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --disable exp.fast_global_inits --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none // This is just to test that the analysis does not cause problems for features that are not explicitly dealt with int main(void) { diff --git a/tests/regression/22-partitioned_arrays/09-one_by_one.c b/tests/regression/22-partitioned_arrays/09-one_by_one.c index c3817cb486..04a997feec 100644 --- a/tests/regression/22-partitioned_arrays/09-one_by_one.c +++ b/tests/regression/22-partitioned_arrays/09-one_by_one.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { int a[4]; int b[4]; diff --git a/tests/regression/22-partitioned_arrays/11-was_problematic.c b/tests/regression/22-partitioned_arrays/11-was_problematic.c index 94b42d8b68..e0ec9ac454 100644 --- a/tests/regression/22-partitioned_arrays/11-was_problematic.c +++ b/tests/regression/22-partitioned_arrays/11-was_problematic.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(int argc, char **argv) { int unLo; diff --git a/tests/regression/22-partitioned_arrays/12-was_problematic_2.c b/tests/regression/22-partitioned_arrays/12-was_problematic_2.c index d5bc02288e..f2e2dcc6a3 100644 --- a/tests/regression/22-partitioned_arrays/12-was_problematic_2.c +++ b/tests/regression/22-partitioned_arrays/12-was_problematic_2.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { int arr[260]; diff --git a/tests/regression/22-partitioned_arrays/13-was_problematic_3.c b/tests/regression/22-partitioned_arrays/13-was_problematic_3.c index ebd35fedcc..047b736778 100644 --- a/tests/regression/22-partitioned_arrays/13-was_problematic_3.c +++ b/tests/regression/22-partitioned_arrays/13-was_problematic_3.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none struct some_struct { int dir[7]; diff --git a/tests/regression/22-partitioned_arrays/14-with_def_exc.c b/tests/regression/22-partitioned_arrays/14-with_def_exc.c index 5e846e6193..41b329fb7f 100644 --- a/tests/regression/22-partitioned_arrays/14-with_def_exc.c +++ b/tests/regression/22-partitioned_arrays/14-with_def_exc.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.def_exc --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.def_exc --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { // Minimal and maximal in def_exc were broken. They are not directly used, but used in the MayBeLess and MayBeEqual queries, that // are in turn used by the partitioning arrays. This is why we run the arrays in combination with def_exc. diff --git a/tests/regression/22-partitioned_arrays/15-var_eq.c b/tests/regression/22-partitioned_arrays/15-var_eq.c index 318436c8bf..44f3d1a846 100644 --- a/tests/regression/22-partitioned_arrays/15-var_eq.c +++ b/tests/regression/22-partitioned_arrays/15-var_eq.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','var_eq']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','var_eq']" --set ana.base.privatization none int global; int main(void) diff --git a/tests/regression/22-partitioned_arrays/16-refine-meet.c b/tests/regression/22-partitioned_arrays/16-refine-meet.c index 74baac45ce..05a73a70ba 100644 --- a/tests/regression/22-partitioned_arrays/16-refine-meet.c +++ b/tests/regression/22-partitioned_arrays/16-refine-meet.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.base.partition-arrays.enabled +// PARAM: --set ana.base.arrays.domain partitioned int garr[7]; int main(int argc, char **argv) diff --git a/tests/regression/22-partitioned_arrays/17-large_arrays.c b/tests/regression/22-partitioned_arrays/17-large_arrays.c index 10e7482c8d..fc29839a36 100644 --- a/tests/regression/22-partitioned_arrays/17-large_arrays.c +++ b/tests/regression/22-partitioned_arrays/17-large_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.base.partition-arrays.enabled +// PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned #include #include #include diff --git a/tests/regression/22-partitioned_arrays/18-large_arrays-nocalloc.c b/tests/regression/22-partitioned_arrays/18-large_arrays-nocalloc.c index f571cdb9ef..09b6f94bd4 100644 --- a/tests/regression/22-partitioned_arrays/18-large_arrays-nocalloc.c +++ b/tests/regression/22-partitioned_arrays/18-large_arrays-nocalloc.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.base.partition-arrays.enabled +// PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned #include #include #include diff --git a/tests/regression/23-partitioned_arrays_last/01-simple_array.c b/tests/regression/23-partitioned_arrays_last/01-simple_array.c index 0b3f41e01f..711b0f6f1f 100644 --- a/tests/regression/23-partitioned_arrays_last/01-simple_array.c +++ b/tests/regression/23-partitioned_arrays_last/01-simple_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int global; int main(void) diff --git a/tests/regression/23-partitioned_arrays_last/02-pointers_array.c b/tests/regression/23-partitioned_arrays_last/02-pointers_array.c index 98b3acbdea..6d17b0af99 100644 --- a/tests/regression/23-partitioned_arrays_last/02-pointers_array.c +++ b/tests/regression/23-partitioned_arrays_last/02-pointers_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { example1(); example2(); diff --git a/tests/regression/23-partitioned_arrays_last/03-multidimensional_arrays.c b/tests/regression/23-partitioned_arrays_last/03-multidimensional_arrays.c index 933ac94d2d..e079baa37a 100644 --- a/tests/regression/23-partitioned_arrays_last/03-multidimensional_arrays.c +++ b/tests/regression/23-partitioned_arrays_last/03-multidimensional_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { example1(); example2(); diff --git a/tests/regression/23-partitioned_arrays_last/04-nesting_arrays.c b/tests/regression/23-partitioned_arrays_last/04-nesting_arrays.c index b93b34b781..fcc141def2 100644 --- a/tests/regression/23-partitioned_arrays_last/04-nesting_arrays.c +++ b/tests/regression/23-partitioned_arrays_last/04-nesting_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none struct kala { int i; int a[5]; diff --git a/tests/regression/23-partitioned_arrays_last/05-adapted_from_01_09_array.c b/tests/regression/23-partitioned_arrays_last/05-adapted_from_01_09_array.c index 22985a83bb..7765a179cc 100644 --- a/tests/regression/23-partitioned_arrays_last/05-adapted_from_01_09_array.c +++ b/tests/regression/23-partitioned_arrays_last/05-adapted_from_01_09_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none #include #include diff --git a/tests/regression/23-partitioned_arrays_last/06-interprocedural.c b/tests/regression/23-partitioned_arrays_last/06-interprocedural.c index 69a5f852be..71a41fa8da 100644 --- a/tests/regression/23-partitioned_arrays_last/06-interprocedural.c +++ b/tests/regression/23-partitioned_arrays_last/06-interprocedural.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { example1(); example2(); diff --git a/tests/regression/23-partitioned_arrays_last/07-global_array.c b/tests/regression/23-partitioned_arrays_last/07-global_array.c index 4d7794fd0a..2c94e934c1 100644 --- a/tests/regression/23-partitioned_arrays_last/07-global_array.c +++ b/tests/regression/23-partitioned_arrays_last/07-global_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int global_array[50]; int main(void) { diff --git a/tests/regression/23-partitioned_arrays_last/08-unsupported.c b/tests/regression/23-partitioned_arrays_last/08-unsupported.c index ebbba3489a..f20a142ea0 100644 --- a/tests/regression/23-partitioned_arrays_last/08-unsupported.c +++ b/tests/regression/23-partitioned_arrays_last/08-unsupported.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --disable exp.fast_global_inits --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --disable exp.fast_global_inits --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none // This is just to test that the analysis does not cause problems for features that are not explicitly dealt with int main(void) { diff --git a/tests/regression/23-partitioned_arrays_last/09-one_by_one.c b/tests/regression/23-partitioned_arrays_last/09-one_by_one.c index 5afc1bbf17..14f23c2318 100644 --- a/tests/regression/23-partitioned_arrays_last/09-one_by_one.c +++ b/tests/regression/23-partitioned_arrays_last/09-one_by_one.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { int a[4]; int b[4]; diff --git a/tests/regression/23-partitioned_arrays_last/11-was_problematic.c b/tests/regression/23-partitioned_arrays_last/11-was_problematic.c index 7e87b9ac52..4ac270f518 100644 --- a/tests/regression/23-partitioned_arrays_last/11-was_problematic.c +++ b/tests/regression/23-partitioned_arrays_last/11-was_problematic.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(int argc, char **argv) { int unLo; diff --git a/tests/regression/23-partitioned_arrays_last/12-was_problematic_2.c b/tests/regression/23-partitioned_arrays_last/12-was_problematic_2.c index 5d9bece121..2ee069b2e5 100644 --- a/tests/regression/23-partitioned_arrays_last/12-was_problematic_2.c +++ b/tests/regression/23-partitioned_arrays_last/12-was_problematic_2.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { int arr[260]; diff --git a/tests/regression/23-partitioned_arrays_last/13-advantage_for_last.c b/tests/regression/23-partitioned_arrays_last/13-advantage_for_last.c index fd43bd031c..f111565710 100644 --- a/tests/regression/23-partitioned_arrays_last/13-advantage_for_last.c +++ b/tests/regression/23-partitioned_arrays_last/13-advantage_for_last.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.partition-arrays.keep-expr last --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.partition-arrays.keep-expr last --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none void main(void) { example1(); } diff --git a/tests/regression/23-partitioned_arrays_last/14-replace_with_const.c b/tests/regression/23-partitioned_arrays_last/14-replace_with_const.c index aab2e20c9a..b349014424 100644 --- a/tests/regression/23-partitioned_arrays_last/14-replace_with_const.c +++ b/tests/regression/23-partitioned_arrays_last/14-replace_with_const.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --enable ana.base.partition-arrays.partition-by-const-on-return --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --enable ana.base.partition-arrays.partition-by-const-on-return --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { example1(); } diff --git a/tests/regression/24-octagon/01-octagon_simple.c b/tests/regression/24-octagon/01-octagon_simple.c index 9647cc1104..0ae7d9a912 100644 --- a/tests/regression/24-octagon/01-octagon_simple.c +++ b/tests/regression/24-octagon/01-octagon_simple.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // Example from https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf void main(void) { int X = 0; diff --git a/tests/regression/24-octagon/02-octagon_interprocedural.c b/tests/regression/24-octagon/02-octagon_interprocedural.c index b39f920198..e4989c643c 100644 --- a/tests/regression/24-octagon/02-octagon_interprocedural.c +++ b/tests/regression/24-octagon/02-octagon_interprocedural.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none int main(void) { f1(); } diff --git a/tests/regression/24-octagon/03-previously_problematic_a.c b/tests/regression/24-octagon/03-previously_problematic_a.c index b4647443b2..23a8468840 100644 --- a/tests/regression/24-octagon/03-previously_problematic_a.c +++ b/tests/regression/24-octagon/03-previously_problematic_a.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included int main(int argc, char const *argv[]) diff --git a/tests/regression/24-octagon/04-previously_problematic_b.c b/tests/regression/24-octagon/04-previously_problematic_b.c index c3f03988f3..cc67569af2 100644 --- a/tests/regression/24-octagon/04-previously_problematic_b.c +++ b/tests/regression/24-octagon/04-previously_problematic_b.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included typedef int wchar_t; diff --git a/tests/regression/24-octagon/05-previously_problematic_c.c b/tests/regression/24-octagon/05-previously_problematic_c.c index 70538c69c9..e7cff27305 100644 --- a/tests/regression/24-octagon/05-previously_problematic_c.c +++ b/tests/regression/24-octagon/05-previously_problematic_c.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included int main(int argc, char const *argv[]) diff --git a/tests/regression/24-octagon/06-previously_problematic_d.c b/tests/regression/24-octagon/06-previously_problematic_d.c index dace7947f7..1e2df54a3c 100644 --- a/tests/regression/24-octagon/06-previously_problematic_d.c +++ b/tests/regression/24-octagon/06-previously_problematic_d.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included int main(int argc, char const *argv[]) diff --git a/tests/regression/24-octagon/07-previously_problematic_e.c b/tests/regression/24-octagon/07-previously_problematic_e.c index 6876b67b1a..3d411069e9 100644 --- a/tests/regression/24-octagon/07-previously_problematic_e.c +++ b/tests/regression/24-octagon/07-previously_problematic_e.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included int main(int argc, char const *argv[]) diff --git a/tests/regression/24-octagon/08-previously_problematic_f.c b/tests/regression/24-octagon/08-previously_problematic_f.c index 2f485a332e..ec6e6a1d70 100644 --- a/tests/regression/24-octagon/08-previously_problematic_f.c +++ b/tests/regression/24-octagon/08-previously_problematic_f.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included int main(int argc, char const *argv[]) diff --git a/tests/regression/24-octagon/09-previously_problematic_g.c b/tests/regression/24-octagon/09-previously_problematic_g.c index c994f4aed8..b257e29d71 100644 --- a/tests/regression/24-octagon/09-previously_problematic_g.c +++ b/tests/regression/24-octagon/09-previously_problematic_g.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included int main(int argc, char const *argv[]) diff --git a/tests/regression/24-octagon/10-previously_problematic_h.c b/tests/regression/24-octagon/10-previously_problematic_h.c index 697db6bd35..630711d9a0 100644 --- a/tests/regression/24-octagon/10-previously_problematic_h.c +++ b/tests/regression/24-octagon/10-previously_problematic_h.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included int main(int argc, char const *argv[]) diff --git a/tests/regression/24-octagon/11-previously_problematic_i.c b/tests/regression/24-octagon/11-previously_problematic_i.c index 902cc4e810..341a042e20 100644 --- a/tests/regression/24-octagon/11-previously_problematic_i.c +++ b/tests/regression/24-octagon/11-previously_problematic_i.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none // These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might // resurface, these tests without asserts are included char buf2[67]; diff --git a/tests/regression/24-octagon/13-array_octagon.c b/tests/regression/24-octagon/13-array_octagon.c index f018ee4e84..8f355a88c4 100644 --- a/tests/regression/24-octagon/13-array_octagon.c +++ b/tests/regression/24-octagon/13-array_octagon.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --set sem.int.signed_overflow assume_none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --set sem.int.signed_overflow assume_none void main(void) { example0(); example1(); diff --git a/tests/regression/24-octagon/14-array_octagon_keep_last.c b/tests/regression/24-octagon/14-array_octagon_keep_last.c index cc8a9001fe..1c28435500 100644 --- a/tests/regression/24-octagon/14-array_octagon_keep_last.c +++ b/tests/regression/24-octagon/14-array_octagon_keep_last.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --set sem.int.signed_overflow assume_none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --set sem.int.signed_overflow assume_none void main(void) { example1(); example2(); diff --git a/tests/regression/24-octagon/15-array_octagon_prec.c b/tests/regression/24-octagon/15-array_octagon_prec.c index 51cd64bf24..4addf3b51f 100644 --- a/tests/regression/24-octagon/15-array_octagon_prec.c +++ b/tests/regression/24-octagon/15-array_octagon_prec.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint --set sem.int.signed_overflow assume_none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint --set sem.int.signed_overflow assume_none void main(void) __attribute__((goblint_precision("no-interval"))); void example1(void) __attribute__((goblint_precision("no-def_exc"))); diff --git a/tests/regression/24-octagon/16-array_octagon_keep_last_prec.c b/tests/regression/24-octagon/16-array_octagon_keep_last_prec.c index bd22bb637b..edaf75b0e9 100644 --- a/tests/regression/24-octagon/16-array_octagon_keep_last_prec.c +++ b/tests/regression/24-octagon/16-array_octagon_keep_last_prec.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint --set sem.int.signed_overflow assume_none +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint --set sem.int.signed_overflow assume_none void main(void) __attribute__((goblint_precision("no-interval"))); void example1(void) __attribute__((goblint_precision("no-def_exc"))); diff --git a/tests/regression/25-vla/01-simple.c b/tests/regression/25-vla/01-simple.c index 166942cb37..6a231e8bde 100644 --- a/tests/regression/25-vla/01-simple.c +++ b/tests/regression/25-vla/01-simple.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { int a[40]; diff --git a/tests/regression/25-vla/02-loop.c b/tests/regression/25-vla/02-loop.c index 7a73aac273..c0ff8348e7 100644 --- a/tests/regression/25-vla/02-loop.c +++ b/tests/regression/25-vla/02-loop.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none int main(void) { example1(); diff --git a/tests/regression/25-vla/03-calls.c b/tests/regression/25-vla/03-calls.c index 02ec74f0b1..9a39f6f6a8 100644 --- a/tests/regression/25-vla/03-calls.c +++ b/tests/regression/25-vla/03-calls.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none // Variable-sized arrays void foo(int n, int a[n]); void foo2(int n, int a[30][n]); diff --git a/tests/regression/25-vla/04-passing_ptr_to_array.c b/tests/regression/25-vla/04-passing_ptr_to_array.c index d6a02449d7..d1c226b888 100644 --- a/tests/regression/25-vla/04-passing_ptr_to_array.c +++ b/tests/regression/25-vla/04-passing_ptr_to_array.c @@ -1,4 +1,4 @@ -//PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +//PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none void foo(int (*a)[40]){ int x = (*(a + 29))[7]; diff --git a/tests/regression/25-vla/05-more_passing.c b/tests/regression/25-vla/05-more_passing.c index b237daf411..cab670118f 100644 --- a/tests/regression/25-vla/05-more_passing.c +++ b/tests/regression/25-vla/05-more_passing.c @@ -1,4 +1,4 @@ -//PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +//PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none # include void foo(int n, int a[n]) { diff --git a/tests/regression/25-vla/06-even_more_passing.c b/tests/regression/25-vla/06-even_more_passing.c index 3056c0fd34..eb87d718ce 100644 --- a/tests/regression/25-vla/06-even_more_passing.c +++ b/tests/regression/25-vla/06-even_more_passing.c @@ -1,4 +1,4 @@ -//PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +//PARAM: --set solver td3 --enable ana.int.interval --disable ana.int.def_exc --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none void foo2(int n , int (*a)[n] ) { diff --git a/tests/regression/30-fast_global_inits/01-on.c b/tests/regression/30-fast_global_inits/01-on.c index 81819d4baa..bfafcb5ed8 100644 --- a/tests/regression/30-fast_global_inits/01-on.c +++ b/tests/regression/30-fast_global_inits/01-on.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none // This checks that partitioned arrays and fast_global_inits are no longer incompatible int global_array[50]; int global_array_multi[50][2][2]; diff --git a/tests/regression/30-fast_global_inits/02-off.c b/tests/regression/30-fast_global_inits/02-off.c index d7ea40fb10..b1b13e749c 100644 --- a/tests/regression/30-fast_global_inits/02-off.c +++ b/tests/regression/30-fast_global_inits/02-off.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --disable exp.fast_global_inits +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --disable exp.fast_global_inits // This checks that partitioned arrays and fast_global_inits are no longer incompatible int global_array[50]; int global_array_multi[50][2][2]; diff --git a/tests/regression/30-fast_global_inits/03-performance.c b/tests/regression/30-fast_global_inits/03-performance.c index 5639128eb1..f8345b049d 100644 --- a/tests/regression/30-fast_global_inits/03-performance.c +++ b/tests/regression/30-fast_global_inits/03-performance.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --enable exp.fast_global_inits --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --enable exp.fast_global_inits --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none // Without fast_global_inits this takes >150s, when it is enabled < 0.1s int global_array[50][500][20]; diff --git a/tests/regression/30-fast_global_inits/04-non-zero.c b/tests/regression/30-fast_global_inits/04-non-zero.c index ebadef8a0f..6c9ac309a5 100644 --- a/tests/regression/30-fast_global_inits/04-non-zero.c +++ b/tests/regression/30-fast_global_inits/04-non-zero.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --enable exp.fast_global_inits +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --enable exp.fast_global_inits // This checks that partitioned arrays and fast_global_inits are no longer incompatible int global_array[5] = {9, 0, 3, 42, 11}; int global_array_multi[2][5] = {{9, 0, 3, 42, 11}, {9, 0, 3, 42, 11}}; diff --git a/tests/regression/30-fast_global_inits/05-non-zero-performance.c b/tests/regression/30-fast_global_inits/05-non-zero-performance.c index c525f7920f..b3812784d0 100644 --- a/tests/regression/30-fast_global_inits/05-non-zero-performance.c +++ b/tests/regression/30-fast_global_inits/05-non-zero-performance.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --enable exp.fast_global_inits +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --enable exp.fast_global_inits int global_array[10000] = {9, 0, 3, 42, 11 }; // All non-specified ones will be zero int global_array_multi[2][10000] = {{9, 0, 3, 42, 11}, {9, 0, 3, 42, 11}}; // All non-specified ones will be zero diff --git a/tests/regression/31-ikind-aware-ints/04-ptrdiff.c b/tests/regression/31-ikind-aware-ints/04-ptrdiff.c index ab68e36ec0..4fdd85d469 100644 --- a/tests/regression/31-ikind-aware-ints/04-ptrdiff.c +++ b/tests/regression/31-ikind-aware-ints/04-ptrdiff.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base', 'mallocWrapper', 'escape', 'expRelation', 'var_eq']" --set ana.base.privatization none +// PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base', 'mallocWrapper', 'escape', 'expRelation', 'var_eq']" --set ana.base.privatization none int *tmp; int main () diff --git a/tests/regression/31-ikind-aware-ints/05-shift.c b/tests/regression/31-ikind-aware-ints/05-shift.c index 0b65012b9e..f89e546729 100644 --- a/tests/regression/31-ikind-aware-ints/05-shift.c +++ b/tests/regression/31-ikind-aware-ints/05-shift.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base', 'mallocWrapper']" --set ana.base.privatization none +// PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base', 'mallocWrapper']" --set ana.base.privatization none int main(void) { // Shifting by a negative number is UB, but we should still not crash on it, but go to top instead int v = -1; diff --git a/tests/regression/31-ikind-aware-ints/06-structs.c b/tests/regression/31-ikind-aware-ints/06-structs.c index cbb5d42316..c0b198880b 100644 --- a/tests/regression/31-ikind-aware-ints/06-structs.c +++ b/tests/regression/31-ikind-aware-ints/06-structs.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base', 'threadflag', 'mallocWrapper']" --set ana.base.privatization none +// PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base', 'threadflag', 'mallocWrapper']" --set ana.base.privatization none struct rtl8169_private { unsigned int features ; }; diff --git a/tests/regression/36-apron/01-octagon_simple.c b/tests/regression/36-apron/01-octagon_simple.c index 10ee501ad9..89061d6929 100644 --- a/tests/regression/36-apron/01-octagon_simple.c +++ b/tests/regression/36-apron/01-octagon_simple.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy // Example from https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf void main(void) { int X = 0; diff --git a/tests/regression/36-apron/02-octagon_interprocudral.c b/tests/regression/36-apron/02-octagon_interprocudral.c index bca10c973c..923d451343 100644 --- a/tests/regression/36-apron/02-octagon_interprocudral.c +++ b/tests/regression/36-apron/02-octagon_interprocudral.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --set ana.apron.privatization dummy +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --set ana.apron.privatization dummy extern int __VERIFIER_nondet_int(); int main(void) { diff --git a/tests/regression/36-apron/94-simple-apron-interval.c b/tests/regression/36-apron/94-simple-apron-interval.c index b878e478d4..cb666120ce 100644 --- a/tests/regression/36-apron/94-simple-apron-interval.c +++ b/tests/regression/36-apron/94-simple-apron-interval.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy --set ana.apron.domain "interval" +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy --set ana.apron.domain "interval" // Example from https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf, adapted void main(void) { int X = 0; diff --git a/tests/regression/36-apron/95-simple-polyhedra.c b/tests/regression/36-apron/95-simple-polyhedra.c index 989f7481e4..32665b28d9 100644 --- a/tests/regression/36-apron/95-simple-polyhedra.c +++ b/tests/regression/36-apron/95-simple-polyhedra.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy --set ana.apron.domain "polyhedra" +// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy --set ana.apron.domain "polyhedra" // Example from https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf, adapted void main(void) { int X = 0; diff --git a/tests/regression/42-annotated-precision/08-22_01-simple_array.c b/tests/regression/42-annotated-precision/08-22_01-simple_array.c index 8ac2a26db8..ca378d3c50 100644 --- a/tests/regression/42-annotated-precision/08-22_01-simple_array.c +++ b/tests/regression/42-annotated-precision/08-22_01-simple_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint int global; int main(void) __attribute__((goblint_precision("no-interval"))); diff --git a/tests/regression/42-annotated-precision/09-22_02-pointers_array.c b/tests/regression/42-annotated-precision/09-22_02-pointers_array.c index c7fdaa6d58..64dbbc1166 100644 --- a/tests/regression/42-annotated-precision/09-22_02-pointers_array.c +++ b/tests/regression/42-annotated-precision/09-22_02-pointers_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint int main(void) __attribute__((goblint_precision("no-interval"))); void example1(void) __attribute__((goblint_precision("no-def_exc"))); diff --git a/tests/regression/42-annotated-precision/10-22_03-multidimensional_arrays.c b/tests/regression/42-annotated-precision/10-22_03-multidimensional_arrays.c index 672960b343..819f5515f3 100644 --- a/tests/regression/42-annotated-precision/10-22_03-multidimensional_arrays.c +++ b/tests/regression/42-annotated-precision/10-22_03-multidimensional_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint void example1(void) __attribute__((goblint_precision("no-def_exc","interval"))); void example2(void) __attribute__((goblint_precision("no-def_exc","interval"))); diff --git a/tests/regression/42-annotated-precision/11-22_04-nesting_arrays.c b/tests/regression/42-annotated-precision/11-22_04-nesting_arrays.c index d3c9b8f4dc..db52605ce2 100644 --- a/tests/regression/42-annotated-precision/11-22_04-nesting_arrays.c +++ b/tests/regression/42-annotated-precision/11-22_04-nesting_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint struct kala { int i; int a[5]; diff --git a/tests/regression/42-annotated-precision/12-22_06-interprocedural.c b/tests/regression/42-annotated-precision/12-22_06-interprocedural.c index 7cb991fe1f..b0d6525416 100644 --- a/tests/regression/42-annotated-precision/12-22_06-interprocedural.c +++ b/tests/regression/42-annotated-precision/12-22_06-interprocedural.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint void example1() __attribute__((goblint_precision("no-def_exc","interval"))); void init_array(int* arr, int val) __attribute__((goblint_precision("no-def_exc","interval"))); diff --git a/tests/regression/42-annotated-precision/13-22_07-global_array.c b/tests/regression/42-annotated-precision/13-22_07-global_array.c index 7b5ff06c29..cd1087fcd2 100644 --- a/tests/regression/42-annotated-precision/13-22_07-global_array.c +++ b/tests/regression/42-annotated-precision/13-22_07-global_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint int global_array[50]; int main(void) __attribute__((goblint_precision("no-def_exc","interval"))); diff --git a/tests/regression/42-annotated-precision/15-23_01-simple_array.c b/tests/regression/42-annotated-precision/15-23_01-simple_array.c index c9723f4aa6..5bf6f5a54d 100644 --- a/tests/regression/42-annotated-precision/15-23_01-simple_array.c +++ b/tests/regression/42-annotated-precision/15-23_01-simple_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint int global; int main(void) __attribute__((goblint_precision("no-interval"))); diff --git a/tests/regression/42-annotated-precision/16-23_02-pointers_array.c b/tests/regression/42-annotated-precision/16-23_02-pointers_array.c index ced23ebd6d..86b6ee4fca 100644 --- a/tests/regression/42-annotated-precision/16-23_02-pointers_array.c +++ b/tests/regression/42-annotated-precision/16-23_02-pointers_array.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint int main(void) __attribute__((goblint_precision("no-interval"))); void example1(void) __attribute__((goblint_precision("no-def_exc"))); diff --git a/tests/regression/42-annotated-precision/17-23_03-multidimensional_arrays.c b/tests/regression/42-annotated-precision/17-23_03-multidimensional_arrays.c index 4ae03cdd87..fce19576a2 100644 --- a/tests/regression/42-annotated-precision/17-23_03-multidimensional_arrays.c +++ b/tests/regression/42-annotated-precision/17-23_03-multidimensional_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint int main(void) { example1(); example2(); diff --git a/tests/regression/42-annotated-precision/18-23_04-nesting_arrays.c b/tests/regression/42-annotated-precision/18-23_04-nesting_arrays.c index eccfc1855e..6a72fe7634 100644 --- a/tests/regression/42-annotated-precision/18-23_04-nesting_arrays.c +++ b/tests/regression/42-annotated-precision/18-23_04-nesting_arrays.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.int.interval --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint struct kala { int i; int a[5]; diff --git a/tests/regression/42-annotated-precision/19-23_06-interprocedural.c b/tests/regression/42-annotated-precision/19-23_06-interprocedural.c index 1228d6d6b2..8edb78469b 100644 --- a/tests/regression/42-annotated-precision/19-23_06-interprocedural.c +++ b/tests/regression/42-annotated-precision/19-23_06-interprocedural.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint void example1() __attribute__((goblint_precision("no-def_exc","interval"))); void init_array(int* arr, int val) __attribute__((goblint_precision("no-def_exc","interval"))); diff --git a/tests/regression/42-annotated-precision/21-23_14-replace_with_const.c b/tests/regression/42-annotated-precision/21-23_14-replace_with_const.c index 013d2322c6..e81f3a1612 100644 --- a/tests/regression/42-annotated-precision/21-23_14-replace_with_const.c +++ b/tests/regression/42-annotated-precision/21-23_14-replace_with_const.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.base.partition-arrays.enabled --set ana.base.partition-arrays.keep-expr "last" --enable ana.base.partition-arrays.partition-by-const-on-return --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last" --enable ana.base.partition-arrays.partition-by-const-on-return --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --enable annotation.int.enabled --set ana.int.refinement fixpoint void example1() __attribute__((goblint_precision("no-def_exc","interval"))); void init_array(int* arr, int val) __attribute__((goblint_precision("no-def_exc","interval"))); diff --git a/tests/regression/42-annotated-precision/24-30_02-off.c b/tests/regression/42-annotated-precision/24-30_02-off.c index a87ae4ada0..4a5e660cf5 100644 --- a/tests/regression/42-annotated-precision/24-30_02-off.c +++ b/tests/regression/42-annotated-precision/24-30_02-off.c @@ -1,4 +1,4 @@ -// PARAM: --set solver td3 --enable ana.base.partition-arrays.enabled --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --disable exp.fast_global_inits --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set solver td3 --set ana.base.arrays.domain partitioned --set ana.activated "['base','threadid','threadflag','escape','expRelation','mallocWrapper']" --set ana.base.privatization none --disable exp.fast_global_inits --enable annotation.int.enabled --set ana.int.refinement fixpoint // This checks that partitioned arrays and fast_global_inits are no longer incompatible int global_array[50]; int global_array_multi[50][2][2]; diff --git a/tests/regression/42-annotated-precision/28-02_36-calloc_struct.c b/tests/regression/42-annotated-precision/28-02_36-calloc_struct.c index 3a5bc061a9..5be981f932 100644 --- a/tests/regression/42-annotated-precision/28-02_36-calloc_struct.c +++ b/tests/regression/42-annotated-precision/28-02_36-calloc_struct.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.base.partition-arrays.enabled --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set ana.base.arrays.domain partitioned --enable annotation.int.enabled --set ana.int.refinement fixpoint #include #include diff --git a/tests/regression/42-annotated-precision/33-02_36-calloc_struct_i.c b/tests/regression/42-annotated-precision/33-02_36-calloc_struct_i.c index ab816300e4..02a05c84ce 100644 --- a/tests/regression/42-annotated-precision/33-02_36-calloc_struct_i.c +++ b/tests/regression/42-annotated-precision/33-02_36-calloc_struct_i.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.base.partition-arrays.enabled --enable annotation.int.enabled --set ana.int.refinement fixpoint +// PARAM: --set ana.base.arrays.domain partitioned --enable annotation.int.enabled --set ana.int.refinement fixpoint #include #include diff --git a/tests/regression/54-unroll_arrays/01-simple_array.c b/tests/regression/54-unroll_arrays/01-simple_array.c new file mode 100644 index 0000000000..e05815f273 --- /dev/null +++ b/tests/regression/54-unroll_arrays/01-simple_array.c @@ -0,0 +1,41 @@ +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 +#include +int global; + +int main(void) +{ + example1(); + example2(); + return 0; +} + +void example1() { + int a[20]; + a[4] = 4; + a[6] = 6; + a[10] = 10; + assert(a[0] == 0); //UNKNOWN + assert(a[4] == 4); + assert(a[6] == 6); //UNKNOWN + + int i = 4; + a[i] = 7; + assert(a[4] == 7); +} + +//array same length of factor +void example2() { + int a[5]; + a[0] = 1; + a[1] = 2; + a[2] = 3; + a[3] = 4; + a[4] = 5; + + assert(a[0] == 1); + assert(a[1] == 2); + assert(a[2] == 3); + assert(a[3] == 0); //FAIL + assert(a[4] == 0); //FAIL +} + diff --git a/tests/regression/54-unroll_arrays/02-simple_array_in_loops.c b/tests/regression/54-unroll_arrays/02-simple_array_in_loops.c new file mode 100644 index 0000000000..57d74cbf2c --- /dev/null +++ b/tests/regression/54-unroll_arrays/02-simple_array_in_loops.c @@ -0,0 +1,48 @@ +// PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 2 +#include +int global; + +int main(void) +{ + example1(); + example2(); + return 0; +} + +// Simple example +void example1(void) +{ + int a[42]; + int i = 0; + int top; + + while (i < 42) { + a[i] = 0; + assert(a[i] == 0); // UNKNOWN + assert(a[0] == 0); // UNKNOWN + assert(a[17] == 0); + i++; + } + + assert(a[0] == 0); // UNKNOWN + assert(a[7] == 0); + assert(a[41] == 0); +} + + +// Check that arrays of types different from int are handeled correctly +void example2() { + char a[10]; + int n; + assert(a[3] == 800); // UNKNOWN + + for(int i=0;i < 10; i++) { + a[i] = 7; + } + + a[3] = (char) n; + assert(a[3] == 800); //FAIL + assert(a[3] == 127); //UNKNOWN + assert(a[3] == -128); //UNKNOWN + assert(a[3] == -129); //FAIL +}