diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 685fdc0afd..343882ebd5 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -25,6 +25,9 @@ jobs:
runs-on: ${{ matrix.os }}
+ env:
+ OCAMLRUNPARAM: b
+
steps:
- name: Checkout code
uses: actions/checkout@v3
@@ -73,6 +76,12 @@ jobs:
- name: Test incremental regression with cfg comparison
run: ruby scripts/update_suite.rb -c
+ - uses: actions/upload-artifact@v3
+ if: always()
+ with:
+ name: suite_result
+ path: tests/suite_result/
+
extraction:
if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index ef070afa96..cf363d9b06 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -24,9 +24,12 @@ struct
module G = AccessDomain.EventSet
let collect_local = ref false
+ let emit_single_threaded = ref false
let init _ =
- collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed"
+ collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
+ let activated = get_string_list "ana.activated" in
+ emit_single_threaded := List.mem (ModifiedSinceLongjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;
@@ -40,7 +43,7 @@ struct
+ [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *)
let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
if M.tracing then M.traceli "access" "access_one_top %a %b %a:\n" AccessKind.pretty kind reach d_exp exp;
- if force || !collect_local || ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) then (
+ if force || !collect_local || !emit_single_threaded || ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) then (
if deref then
do_access ctx kind reach exp;
Access.distribute_access_exp (do_access ctx Read false) exp
diff --git a/src/analyses/activeLongjmp.ml b/src/analyses/activeLongjmp.ml
new file mode 100644
index 0000000000..185cdfca0e
--- /dev/null
+++ b/src/analyses/activeLongjmp.ml
@@ -0,0 +1,41 @@
+(** Analysis tracking which longjmp is currently active *)
+
+open Prelude.Ana
+open Analyses
+
+module Spec =
+struct
+ include Analyses.IdentitySpec
+
+ let name () = "activeLongjmp"
+
+ (* The first component are the longjmp targets, the second are the longjmp callers *)
+ module D = JmpBufDomain.ActiveLongjmps
+ module C = Lattice.Unit
+
+ let context _ _ = ()
+
+ let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+ let desc = LibraryFunctions.find f in
+ match desc.special arglist, f.vname with
+ | Longjmp {env; value}, _ ->
+ (* Set target to current value of env *)
+ let bufs = ctx.ask (EvalJumpBuf env) in
+ bufs, JmpBufDomain.NodeSet.singleton(ctx.prev_node)
+ | _ -> ctx.local
+
+ (* Initial values don't really matter: overwritten at longjmp call. *)
+ let startstate v = D.bot ()
+ let threadenter ctx lval f args = [D.bot ()]
+ let exitstate v = D.top ()
+
+ let query ctx (type a) (q: a Queries.t): a Queries.result =
+ match q with
+ | ActiveJumpBuf ->
+ (* Does not compile without annotation: "This instance (...) is ambiguous: it would escape the scope of its equation" *)
+ (ctx.local:JmpBufDomain.ActiveLongjmps.t)
+ | _ -> Queries.Result.top q
+end
+
+let _ =
+ MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/activeSetjmp.ml b/src/analyses/activeSetjmp.ml
new file mode 100644
index 0000000000..904ad12ae7
--- /dev/null
+++ b/src/analyses/activeSetjmp.ml
@@ -0,0 +1,39 @@
+(** Analysis tracking which setjmp(s) are currently active *)
+
+open Prelude.Ana
+open Analyses
+
+module Spec =
+struct
+ include Analyses.IdentitySpec
+
+ let name () = "activeSetjmp"
+
+ module D = JmpBufDomain.JmpBufSet
+ module C = JmpBufDomain.JmpBufSet
+
+ let should_join a b = D.equal a b
+
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask): D.t =
+ ctx.local (* keep local as opposed to IdentitySpec *)
+
+ let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+ let desc = LibraryFunctions.find f in
+ match desc.special arglist with
+ | Setjmp _ ->
+ let entry = (ctx.prev_node, ctx.control_context ()) in
+ D.add (Target entry) ctx.local
+ | _ -> ctx.local
+
+ let startstate v = D.bot ()
+ let threadenter ctx lval f args = [D.bot ()]
+ let exitstate v = D.top ()
+
+ let query ctx (type a) (q: a Queries.t): a Queries.result =
+ match q with
+ | ValidLongJmp -> (ctx.local: D.t)
+ | _ -> Queries.Result.top q
+end
+
+let _ =
+ MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 460f2e7b0f..c7ec23a217 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -147,6 +147,8 @@ struct
let return_var () = AD.from_var (return_varinfo ())
let return_lval (): lval = (Var (return_varinfo ()), NoOffset)
+ let longjmp_return = ref dummyFunDec.svar
+
let heap_var ctx =
let info = match (ctx.ask Q.HeapVar) with
| `Lifted vinfo -> vinfo
@@ -162,6 +164,7 @@ struct
| None -> ()
end;
return_varstore := Goblintutil.create_var @@ makeVarinfo false "RETURN" voidType;
+ longjmp_return := Goblintutil.create_var @@ makeVarinfo false "LONGJMP_RETURN" intType;
Priv.init ()
let finalize () =
@@ -528,6 +531,7 @@ struct
| `Int _ -> empty
| `Float _ -> empty
| `Thread _ -> empty (* thread IDs are abstract and nothing known can be reached from them *)
+ | `JmpBuf _ -> empty (* Jump buffers are abstract and nothing known can be reached from them *)
| `Mutex -> empty (* mutexes are abstract and nothing known can be reached from them *)
(* Get the list of addresses accessable immediately from a given address, thus
@@ -669,6 +673,7 @@ struct
| `Int _ -> (empty, TS.bot (), false)
| `Float _ -> (empty, TS.bot (), false)
| `Thread _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
+ | `JmpBuf _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
| `Mutex -> (empty, TS.bot (), false) (* TODO: is this right? *)
in
reachable_from_value (get (Analyses.ask_of_ctx ctx) ctx.global ctx.local adr None)
@@ -1247,6 +1252,20 @@ struct
let fs = eval_funvar ctx e in
List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
end
+ | Q.EvalJumpBuf e ->
+ begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+ | `Address jmp_buf ->
+ if AD.mem Addr.UnknownPtr jmp_buf then
+ M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e;
+ begin match get ~top:(VD.bot ()) (Analyses.ask_of_ctx ctx) ctx.global ctx.local jmp_buf None with
+ | `JmpBuf (x, copied) ->
+ if copied then
+ M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
+ x
+ | y -> failwith (Pretty.sprint ~width:max_int (Pretty.dprintf "problem?! is %a %a:\n state is %a" CilType.Exp.pretty e VD.pretty y D.pretty ctx.local))
+ end
+ | _ -> failwith "problem?!"
+ end
| Q.EvalInt e ->
query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
| Q.EvalLength e -> begin
@@ -1452,6 +1471,7 @@ struct
Priv.read_global a priv_getg st x
in
let new_value = update_offset old_value in
+ M.tracel "hgh" "update_offset %a -> %a\n" VD.pretty old_value VD.pretty new_value;
let r = Priv.write_global ~invariant a priv_getg (priv_sideg ctx.sideg) st x new_value in
if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a\n\n" x.vname D.pretty r;
r
@@ -1524,9 +1544,12 @@ struct
(* within invariant, a change to the way arrays are partitioned is not necessary *)
List.fold_left (fun x y -> effect_on_array (not invariant) y x) st affected_arrays
in
- let x_updated = update_variable x t new_value st.cpa in
- let with_dep = add_partitioning_dependencies x new_value {st with cpa = x_updated } in
- effect_on_arrays a with_dep
+ if VD.is_bot new_value && invariant && not (CPA.mem x st.cpa) then
+ st
+ else
+ let x_updated = update_variable x t new_value st.cpa in
+ let with_dep = add_partitioning_dependencies x new_value {st with cpa = x_updated } in
+ effect_on_arrays a with_dep
end
in
let update_one x store =
@@ -1667,6 +1690,7 @@ struct
in
char_array_hack ();
let rval_val = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local rval in
+ let rval_val = VD.mark_jmpbufs_as_copied rval_val in
let lval_val = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
(* let sofa = AD.short 80 lval_val^" = "^VD.short 80 rval_val in *)
(* M.debug ~category:Analyzer @@ sprint ~width:max_int @@ dprintf "%a = %a\n%s" d_plainlval lval d_plainexp rval sofa; *)
@@ -1691,7 +1715,7 @@ struct
| _ -> ()
);
match lval with (* this section ensure global variables contain bottom values of the proper type before setting them *)
- | (Var v, offs) when AD.is_definite lval_val && v.vglob ->
+ | (Var v, offs) when v.vglob ->
(* Optimization: In case of simple integral types, we not need to evaluate the old value.
v is not an allocated block, as v directly appears as a variable in the program;
so no explicit check is required here (unlike in set) *)
@@ -2226,6 +2250,42 @@ struct
st
end
| Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
+ | Setjmp { env }, _ ->
+ let ask = Analyses.ask_of_ctx ctx in
+ let st' = match eval_rv ask gs st env with
+ | `Address jmp_buf ->
+ let value = `JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false) in
+ let r = set ~ctx ask gs st jmp_buf (Cilfacade.typeOf env) value in
+ if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env D.pretty st D.pretty r;
+ r
+ | _ -> failwith "problem?!"
+ in
+ begin match lv with
+ | Some lv ->
+ set ~ctx ask gs st' (eval_lv ask ctx.global st lv) (Cilfacade.typeOfLval lv) (`Int (ID.of_int IInt BI.zero))
+ | None -> st'
+ end
+ | Longjmp {env; value}, _ ->
+ let ask = Analyses.ask_of_ctx ctx in
+ let ensure_not_zero rv = match rv with
+ | `Int i ->
+ begin match ID.to_bool i with
+ | Some true -> rv
+ | Some false ->
+ M.error "Must: Longjmp with a value of 0 is silently changed to 1";
+ `Int (ID.of_int (ID.ikind i) Z.one)
+ | None ->
+ M.warn "May: Longjmp with a value of 0 is silently changed to 1";
+ let ik = ID.ikind i in
+ `Int (ID.join (ID.meet i (ID.of_excl_list ik [Z.zero])) (ID.of_int ik Z.one))
+ end
+ | _ ->
+ M.warn ~category:Program "Arguments to longjmp are strange!";
+ rv
+ in
+ let rv = ensure_not_zero @@ eval_rv ask ctx.global ctx.local value in
+ let t = Cilfacade.typeOf value in
+ set ~ctx ~t_override:t ask ctx.global ctx.local (AD.from_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
| _, _ ->
let st =
special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args
@@ -2285,7 +2345,7 @@ struct
let tainted = f_ask.f Q.MayBeTainted in
if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname Q.LS.pretty tainted;
if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
- if (Q.LS.is_top tainted) then
+ if Q.LS.is_top tainted then
let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in
let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *)
if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty cpa';
@@ -2293,9 +2353,12 @@ struct
else
(* remove variables from caller cpa, that are global and not in the callee cpa *)
let cpa_caller = CPA.filter (fun x _ -> (not (is_global ask x)) || CPA.mem x fun_st.cpa) st.cpa in
+ if M.tracing then M.trace "taintPC" "cpa_caller: %a\n" CPA.pretty cpa_caller;
(* add variables from callee that are not in caller yet *)
let cpa_new = CPA.filter (fun x _ -> not (CPA.mem x cpa_caller)) cpa_noreturn in
+ if M.tracing then M.trace "taintPC" "cpa_new: %a\n" CPA.pretty cpa_new;
let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in
+ if M.tracing then M.trace "taintPC" "cpa_caller': %a\n" CPA.pretty cpa_caller';
(* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*)
let tainted = Q.LS.filter (fun (v, _) -> not (CPA.mem v cpa_new)) tainted in
let st_combined = combine_st ctx {st with cpa = cpa_caller'} fun_st tainted in
@@ -2508,6 +2571,13 @@ struct
assert_fn ctx exp true
| Events.Unassume {exp; uuids} ->
Timing.wrap "base unassume" (unassume ctx exp) uuids
+ | Events.Longjmped {lval} ->
+ begin match lval with
+ | Some lval ->
+ let st' = assign ctx lval (Lval (Cil.var !longjmp_return)) in
+ {st' with cpa = CPA.remove !longjmp_return st'.cpa}
+ | None -> ctx.local
+ end
| _ ->
ctx.local
end
diff --git a/src/analyses/baseUtil.ml b/src/analyses/baseUtil.ml
index 202aa54410..b2903bf534 100644
--- a/src/analyses/baseUtil.ml
+++ b/src/analyses/baseUtil.ml
@@ -6,6 +6,7 @@ let is_global (a: Q.ask) (v: varinfo): bool =
v.vglob || ThreadEscape.has_escaped a v
let is_static (v:varinfo): bool = v.vstorage = Static
+let is_volatile variable = Ciltools.is_volatile_tp variable.vtype
let is_always_unknown variable = variable.vstorage = Extern || Ciltools.is_volatile_tp variable.vtype
diff --git a/src/analyses/baseUtil.mli b/src/analyses/baseUtil.mli
index 60e41ffb80..d01d57b146 100644
--- a/src/analyses/baseUtil.mli
+++ b/src/analyses/baseUtil.mli
@@ -2,6 +2,7 @@ open GoblintCil
val is_global: Queries.ask -> varinfo -> bool
val is_static: varinfo -> bool
+val is_volatile: varinfo -> bool
val is_always_unknown: varinfo -> bool
val is_excluded_from_earlyglobs: varinfo -> bool
val is_excluded_from_invalidation: varinfo -> bool
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index d2f908a69a..32c2f40744 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -51,15 +51,29 @@ struct
emit_splits ctx d
let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) =
- let d = match f.vname with
- | "__goblint_split_begin" ->
+ let d = match (LibraryFunctions.find f).special arglist, f.vname with
+ | _, "__goblint_split_begin" ->
let exp = List.hd arglist in
let ik = Cilfacade.get_ikind_exp exp in
(* TODO: something different for pointers, currently casts pointers to ints and loses precision (other than NULL) *)
D.add exp (ID.top_of ik) ctx.local (* split immediately follows *)
- | "__goblint_split_end" ->
+ | _, "__goblint_split_end" ->
let exp = List.hd arglist in
D.remove exp ctx.local
+ | Setjmp { env }, _ ->
+ Option.map_default (fun lval ->
+ match GobConfig.get_string "ana.setjmp.split" with
+ | "none" -> ctx.local
+ | "precise" ->
+ let e = Lval lval in
+ let ik = Cilfacade.get_ikind_exp e in
+ D.add e (ID.top_of ik) ctx.local
+ | "coarse" ->
+ let e = Lval lval in
+ let e = BinOp (Eq, e, integer 0, intType) in
+ D.add e (ID.top_of IInt) ctx.local
+ | _ -> failwith "Invalid value for ana.setjmp.split"
+ ) ctx.local lval
| _ ->
ctx.local
in
@@ -75,6 +89,8 @@ struct
| UpdateExpSplit exp ->
let value = ctx.ask (EvalInt exp) in
D.add exp value ctx.local
+ | Longjmped _ ->
+ emit_splits_ctx ctx
| _ ->
ctx.local
end
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index 3e848c45db..a477fc1809 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -62,6 +62,8 @@ type special =
| Strcpy of { dest: Cil.exp; src: Cil.exp } (* TODO: add count for strncpy when actually used *)
| Abort
| Identity of Cil.exp (** Identity function. Some compiler optimization annotation functions map to this. *)
+ | Setjmp of { env: Cil.exp; }
+ | Longjmp of { env: Cil.exp; value: Cil.exp; }
| Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 09023ab719..dd3015e33d 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -50,6 +50,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("abs", unknown [drop "j" []]);
("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
+ ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
+ ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
+ ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
]
(** C POSIX library functions.
@@ -130,6 +133,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("semget", unknown [drop "key" []; drop "nsems" []; drop "semflg" []]);
("semctl", unknown (drop "semid" [] :: drop "semnum" [] :: drop "cmd" [] :: VarArgs (drop "semun" [r_deep])));
("semop", unknown [drop "semid" []; drop "sops" [r]; drop "nsops" []]);
+ ("__sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env }); (* has two underscores *)
+ ("sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env });
+ ("siglongjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
]
(** Pthread functions. *)
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 8d3abc754a..f4640f8ea2 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -130,7 +130,6 @@ struct
let startstate v = map (fun (n,{spec=(module S:MCPSpec); _}) -> n, repr @@ S.startstate v) !activated
let morphstate v x = map (fun (n,(module S:MCPSpec),d) -> n, repr @@ S.morphstate v (obj d)) (spec_list x)
-
let rec assoc_replace (n,c) = function
| [] -> failwith "assoc_replace"
| (n',c')::xs -> if n=n' then (n,c)::xs else (n',c') :: assoc_replace (n,c) xs
@@ -576,4 +575,9 @@ struct
do_sideg ctx !sides;
let d = do_emits ctx !emits d q in
if q then raise Deadcode else d
+
+ let event (ctx:(D.t, G.t, C.t, V.t) ctx) e _ = do_emits ctx [e] ctx.local false
+
+ (* Just to satisfy signature *)
+ let paths_as_set ctx = [ctx.local]
end
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
new file mode 100644
index 0000000000..62af3451a5
--- /dev/null
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -0,0 +1,67 @@
+(** Locally track the variables that may have been written since the corresponding jumpbuffer was set *)
+
+open Prelude.Ana
+open Analyses
+
+module Spec =
+struct
+ include Analyses.IdentitySpec
+
+ let name () = "modifiedSinceLongjmp"
+ module D = JmpBufDomain.LocallyModifiedMap
+ module VS = D.VarSet
+ module C = Lattice.Unit
+
+ let context _ _ = ()
+
+ let add_to_all_defined vs d =
+ D.map (fun vs' -> VS.union vs vs') d
+
+ let is_relevant v =
+ (* Only checks for v.vglob on purpose, acessing espaced locals after longjmp is UB like for any local *)
+ not v.vglob (* *) && not (BaseUtil.is_volatile v) && v.vstorage <> Static
+
+ let relevants_from_ls ls =
+ if Queries.LS.is_top ls then
+ VS.top ()
+ else
+ Queries.LS.fold (fun (v, _) acc -> if is_relevant v then VS.add v acc else acc) ls (VS.empty ())
+
+ (* transfer functions *)
+ let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+ [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)
+
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =
+ let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in
+ add_to_all_defined taintedcallee ctx.local
+
+ let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+ let desc = LibraryFunctions.find f in
+ match desc.special arglist with
+ | Setjmp _ ->
+ let entry = (ctx.prev_node, ctx.control_context ()) in
+ let v = D.find entry ctx.local in (* Will make bot binding explicit here *)
+ (* LHS of setjmp not marked as tainted on purpose *)
+ D.add entry v ctx.local
+ | _ ->
+ ctx.local
+
+ let startstate v = D.bot ()
+ let threadenter ctx lval f args = [D.bot ()]
+ let exitstate v = D.top ()
+
+ let query ctx (type a) (q: a Queries.t): a Queries.result =
+ match q with
+ | Queries.MayBeModifiedSinceSetjmp entry -> D.find entry ctx.local
+ | _ -> Queries.Result.top q
+
+ let event ctx (e: Events.t) octx =
+ match e with
+ | Access {lvals; kind = Write; _} ->
+ add_to_all_defined (relevants_from_ls lvals) ctx.local
+ | _ ->
+ ctx.local
+end
+
+let _ =
+ MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
new file mode 100644
index 0000000000..42529dd9c3
--- /dev/null
+++ b/src/analyses/poisonVariables.ml
@@ -0,0 +1,104 @@
+open Prelude.Ana
+open Analyses
+
+module Spec =
+struct
+ include Analyses.IdentitySpec
+ module VS = SetDomain.ToppedSet(CilType.Varinfo) (struct let topname = "All vars" end)
+
+ let name () = "poisonVariables"
+ module D = VS
+ module C = Lattice.Unit
+
+ let context _ _ = ()
+
+ let check_lval tainted ((v, offset): Queries.LS.elt) =
+ if not v.vglob && VS.mem v tainted then
+ M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" d_varinfo v
+
+ let rem_lval tainted ((v, offset): Queries.LS.elt) = match offset with
+ | `NoOffset -> VS.remove v tainted
+ | _ -> tainted (* If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *)
+
+
+ (* transfer functions *)
+ let return ctx (exp:exp option) (f:fundec) : D.t =
+ (* remove locals, except ones which need to be weakly updated*)
+ if D.is_top ctx.local then
+ ctx.local
+ else (
+ let locals = f.sformals @ f.slocals in
+ D.filter (fun v ->
+ not (List.exists (fun local ->
+ CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))
+ ) locals)
+ ) ctx.local
+ )
+
+ let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+ if VS.is_empty ctx.local then
+ [ctx.local,ctx.local]
+ else (
+ let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
+ if Queries.LS.is_top reachable_from_args || VS.is_top ctx.local then
+ [ctx.local, ctx.local]
+ else
+ let reachable_vars =
+ Queries.LS.elements reachable_from_args
+ |> List.map fst
+ |> VS.of_list
+ in
+ [VS.diff ctx.local reachable_vars, VS.inter reachable_vars ctx.local]
+ )
+
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+ VS.join au ctx.local
+
+ let startstate v = D.bot ()
+ let threadenter ctx lval f args = [D.bot ()]
+ let exitstate v = D.top ()
+
+ let event ctx e octx =
+ match e with
+ | Events.Longjmped {lval} ->
+ let modified_locals = ctx.ask (MayBeModifiedSinceSetjmp (ctx.prev_node, ctx.control_context ())) in
+ let modified_locals = match lval with
+ | Some (Var v, NoOffset) -> Queries.VS.remove v modified_locals
+ | _ -> modified_locals (* Does usually not really occur, if it does, this is sound *)
+ in
+ let (_, longjmp_nodes) = ctx.ask ActiveJumpBuf in
+ JmpBufDomain.NodeSet.iter (fun longjmp_node ->
+ if Queries.VS.is_top modified_locals then
+ M.info ~category:(Behavior (Undefined Other)) ~loc:(Node longjmp_node) "Since setjmp at %a, potentially all locals were modified! Reading them will yield Undefined Behavior." Node.pretty ctx.prev_node
+ else if not (Queries.VS.is_empty modified_locals) then
+ M.info ~category:(Behavior (Undefined Other)) ~loc:(Node longjmp_node) "Since setjmp at %a, locals %a were modified! Reading them will yield Undefined Behavior." Node.pretty ctx.prev_node Queries.VS.pretty modified_locals
+ else
+ ()
+ ) longjmp_nodes;
+ D.join modified_locals ctx.local
+ | Access {lvals; kind = Read; _} ->
+ if Queries.LS.is_top lvals then (
+ if not (VS.is_empty octx.local) then
+ M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!"
+ )
+ else (
+ Queries.LS.iter (fun lv ->
+ (* Use original access state instead of current with removed written vars. *)
+ check_lval octx.local lv
+ ) lvals
+ );
+ ctx.local
+ | Access {lvals; kind = Write; _} ->
+ if Queries.LS.is_top lvals then
+ ctx.local
+ else (
+ Queries.LS.fold (fun lv acc ->
+ rem_lval acc lv
+ ) lvals ctx.local
+ )
+ | _ -> ctx.local
+
+end
+
+let _ =
+ MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index 11853e7961..f7eb266900 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -21,7 +21,7 @@ struct
(* Add Lval or any Lval which it may point to to the set *)
let taint_lval ctx (lval:lval) : D.t =
let d = ctx.local in
- (match lval with
+ (match lval with
| (Var v, offs) -> D.add (v, resolve offs) d
| (Mem e, _) -> D.union (ctx.ask (Queries.MayPointTo e)) d
)
@@ -36,9 +36,18 @@ struct
let return ctx (exp:exp option) (f:fundec) : D.t =
(* remove locals, except ones which need to be weakly updated*)
let d = ctx.local in
- let locals = (f.sformals @ f.slocals) in
- let locals_noweak = List.filter (fun v_info -> not (ctx.ask (Queries.IsMultiple v_info))) locals in
- let d_return = if D.is_top d then d else D.filter (fun (v, _) -> not (List.mem v locals_noweak)) d in
+ let d_return =
+ if D.is_top d then
+ d
+ else (
+ let locals = f.sformals @ f.slocals in
+ D.filter (fun (v, _) ->
+ not (List.exists (fun local ->
+ CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))
+ ) locals)
+ ) d
+ )
+ in
if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a\n" f.svar.vname D.pretty d D.pretty d_return;
d_return
@@ -52,7 +61,7 @@ struct
let d =
match lvalOpt with
| Some lv -> taint_lval ctx lv
- | None -> ctx.local
+ | None -> ctx.local
in
D.union d au
@@ -61,7 +70,7 @@ struct
let d =
match lvalOpt with
| Some lv -> taint_lval ctx lv
- | None -> ctx.local
+ | None -> ctx.local
in
let desc = LibraryFunctions.find f in
let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in
@@ -86,9 +95,9 @@ struct
d
let startstate v = D.bot ()
- let threadenter ctx lval f args =
+ let threadenter ctx lval f args =
[D.bot ()]
- let threadspawn ctx lval f args fctx =
+ let threadspawn ctx lval f args fctx =
match lval with
| Some lv -> taint_lval ctx lv
| None -> ctx.local
@@ -107,5 +116,5 @@ let _ =
module VS = SetDomain.ToppedSet(Basetype.Variables) (struct let topname = "All" end)
(* Convert Lval set to (less precise) Varinfo set. *)
-let conv_varset (lval_set : Spec.D.t) : VS.t =
+let conv_varset (lval_set : Spec.D.t) : VS.t =
if Spec.D.is_top lval_set then VS.top () else VS.of_list (List.map (fun (v, _) -> v) (Spec.D.elements lval_set))
diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml
index b45cd51fbe..bc1fc9da30 100644
--- a/src/analyses/threadReturn.ml
+++ b/src/analyses/threadReturn.ml
@@ -29,7 +29,11 @@ struct
ctx.local
let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
- [ctx.local, false]
+ if !Goblintutil.global_initialization then
+ (* We are inside enter_with inside a startfun, and thus the current function retruning is the main function *)
+ [ctx.local, true]
+ else
+ [ctx.local, false]
let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
ctx.local
diff --git a/src/analyses/tutorials/constants.ml b/src/analyses/tutorials/constants.ml
index e7973147e7..8908545ce4 100644
--- a/src/analyses/tutorials/constants.ml
+++ b/src/analyses/tutorials/constants.ml
@@ -83,7 +83,7 @@ struct
)
|_ -> state
- let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask): D.t =
(* If we have a function call with assignment
x = f (e1, ... , ek)
with a local int variable x on the left, we set it to top *)
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 672e08c10a..023305b9d2 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -104,7 +104,7 @@ struct
(** For a function call "lval = f(args)" or "f(args)",
computes the state of the caller after the call.
Argument [callee_local] is the state of [f] at its return node. *)
- let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask) : D.t =
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
let caller_state = ctx.local in
(* TODO: Record whether lval was tainted. *)
caller_state
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 01b6185d90..383ff69f2f 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -431,7 +431,7 @@ struct
let combine ctx lval fexp f args fc st2 (f_ask : Queries.ask) =
let tainted = f_ask.f Queries.MayBeTainted in
- let d_local =
+ let d_local =
(* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top
TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *)
if Queries.LS.is_top tainted || not (ctx.ask Queries.MustBeSingleThreaded) then
diff --git a/src/analyses/vla.ml b/src/analyses/vla.ml
new file mode 100644
index 0000000000..1cc67dc282
--- /dev/null
+++ b/src/analyses/vla.ml
@@ -0,0 +1,41 @@
+(** An analysis to detect if an invocation is in the scope of a variably modified variable. *)
+
+open Prelude.Ana
+open Analyses
+
+module Spec =
+struct
+ include Analyses.IdentitySpec
+
+ let name () = "vla"
+ module D = BoolDomain.MayBool
+ module C = Lattice.Unit
+
+ let context _ _ = ()
+
+ let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+ [ctx.local, false]
+
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+ ctx.local
+
+ let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+ match (LibraryFunctions.find f).special arglist with
+ | Setjmp _ ->
+ (* Checking if this within the scope of an identifier of variably modified type *)
+ if ctx.local then
+ M.warn ~category:(Behavior (Undefined Other)) "setjmp called within the scope of a variably modified type. If a call to longjmp is made after this scope is left, the behavior is undefined.";
+ ctx.local
+ | _ ->
+ ctx.local
+
+ let vdecl ctx (v:varinfo) : D.t =
+ ctx.local || Cilfacade.isVLAType v.vtype
+
+ let startstate v = D.bot ()
+ let threadenter ctx lval f args = [D.top ()]
+ let exitstate v = D.top ()
+end
+
+let _ =
+ MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml
index 637f7cb829..f78010c14b 100644
--- a/src/cdomains/baseDomain.ml
+++ b/src/cdomains/baseDomain.ml
@@ -31,7 +31,7 @@ struct
let name () = "array partitioning deps"
end
-(** Maintains a set of local variables that need to be weakly updated, because multiple reachbale copies of them may *)
+(** Maintains a set of local variables that need to be weakly updated, because multiple reachable copies of them may *)
(* exist on the call stack *)
module WeakUpdates =
struct
diff --git a/src/cdomains/jmpBufDomain.ml b/src/cdomains/jmpBufDomain.ml
new file mode 100644
index 0000000000..e5c3c96e74
--- /dev/null
+++ b/src/cdomains/jmpBufDomain.ml
@@ -0,0 +1,64 @@
+module BufferEntry = Printable.ProdSimple(Node)(ControlSpecC)
+
+module BufferEntryOrTop = struct
+ include Printable.Std
+ type t = AllTargets | Target of BufferEntry.t [@@deriving eq, ord, hash, to_yojson]
+ let show = function AllTargets -> "All" | Target x -> BufferEntry.show x
+
+ include Printable.SimpleShow (struct
+ type nonrec t = t
+ let show = show
+ end)
+end
+
+module JmpBufSet =
+struct
+ include SetDomain.Make (BufferEntryOrTop)
+ let top () = singleton BufferEntryOrTop.AllTargets
+ let name () = "Jumpbuffers"
+
+ let inter x y =
+ if mem BufferEntryOrTop.AllTargets x || mem BufferEntryOrTop.AllTargets y then
+ let fromx = if mem BufferEntryOrTop.AllTargets y then x else bot () in
+ let fromy = if mem BufferEntryOrTop.AllTargets x then y else bot () in
+ union fromx fromy
+ else
+ inter x y
+
+ let meet = inter
+end
+
+module JmpBufSetTaint =
+struct
+ module Bufs = JmpBufSet
+ include Lattice.Prod(JmpBufSet)(BoolDomain.MayBool)
+ let buffers (a,_) = a
+ let copied (_,b) = b
+ let name () = "JumpbufferCopyTaint"
+end
+
+
+(* module JmpBufSet =
+ struct
+ include SetDomain.ToppedSet (BufferEntry) (struct let topname = "All jumpbufs" end)
+ let name () = "Jumpbuffers"
+ end *)
+
+module NodeSet =
+struct
+ include SetDomain.ToppedSet (Node) (struct let topname = "All longjmp callers" end)
+ let name () = "Longjumps"
+end
+
+module ActiveLongjmps =
+struct
+ include Lattice.ProdSimple(JmpBufSet)(NodeSet)
+end
+
+module LocallyModifiedMap =
+struct
+ module VarSet = SetDomain.ToppedSet(CilType.Varinfo) (struct let topname = "All vars" end)
+ include MapDomain.MapBot_LiftTop (BufferEntry)(VarSet)
+
+ let name () = "Locally modified variables since the corresponding setjmp"
+end
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 8161f994ee..bf2be79815 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -35,6 +35,7 @@ sig
val zero_init_value: ?varAttr:attributes -> typ -> t
val project: Q.ask -> int_precision option-> ( attributes * attributes ) option -> t -> t
+ val mark_jmpbufs_as_copied: t -> t
end
module type Blob =
@@ -68,6 +69,7 @@ struct
end
module Threads = ConcDomain.ThreadSet
+module JmpBufs = JmpBufDomain.JmpBufSetTaint
module rec Compound: S with type t = [
| `Top
@@ -79,6 +81,7 @@ module rec Compound: S with type t = [
| `Array of CArrays.t
| `Blob of Blobs.t
| `Thread of Threads.t
+ | `JmpBuf of JmpBufs.t
| `Mutex
| `Bot
] and type offs = (fieldinfo,IndexDomain.t) Lval.offs =
@@ -93,6 +96,7 @@ struct
| `Array of CArrays.t
| `Blob of Blobs.t
| `Thread of Threads.t
+ | `JmpBuf of JmpBufs.t
| `Mutex
| `Bot
] [@@deriving eq, ord, hash]
@@ -108,6 +112,10 @@ struct
| TNamed ({tname = "pthread_t"; _}, _) -> true
| _ -> false
+ let is_jmp_buf_type = function
+ | TNamed ({tname = "jmp_buf"; _}, _) -> true
+ | _ -> false
+
let array_length_idx default length =
let l = BatOption.bind length (fun e -> Cil.getInteger (Cil.constFold true e)) in
BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) default l
@@ -115,6 +123,7 @@ struct
let rec bot_value ?(varAttr=[]) (t: typ): t =
match t with
| _ when is_mutex_type t -> `Mutex
+ | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.bot ())
| TInt _ -> `Bot (*`Int (ID.bot ()) -- should be lower than any int or address*)
| TFloat _ -> `Bot
| TPtr _ -> `Address (AD.bot ())
@@ -125,6 +134,7 @@ struct
let len = array_length_idx (IndexDomain.bot ()) length in
`Array (CArrays.make ~varAttr ~typAttr len (bot_value ai))
| t when is_thread_type t -> `Thread (ConcDomain.ThreadSet.empty ())
+ | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.Bufs.empty (), false)
| TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t)
| _ -> `Bot
@@ -138,6 +148,7 @@ struct
| `Array x -> CArrays.is_bot x
| `Blob x -> Blobs.is_bot x
| `Thread x -> Threads.is_bot x
+ | `JmpBuf x -> JmpBufs.is_bot x
| `Mutex -> true
| `Bot -> true
| `Top -> false
@@ -145,6 +156,7 @@ struct
let rec init_value ?(varAttr=[]) (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *)
match t with
| t when is_mutex_type t -> `Mutex
+ | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
| TInt (ik,_) -> `Int (ID.top_of ik)
| TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.top_of fkind)
| TPtr _ -> `Address AD.top_ptr
@@ -162,6 +174,7 @@ struct
let rec top_value ?(varAttr=[]) (t: typ): t =
match t with
| _ when is_mutex_type t -> `Mutex
+ | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
| TInt (ik,_) -> `Int (ID.(cast_to ik (top_of ik)))
| TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.top_of fkind)
| TPtr _ -> `Address AD.top_ptr
@@ -185,6 +198,7 @@ struct
| `Array x -> CArrays.is_top x
| `Blob x -> Blobs.is_top x
| `Thread x -> Threads.is_top x
+ | `JmpBuf x -> JmpBufs.is_top x
| `Mutex -> true
| `Top -> true
| `Bot -> false
@@ -192,6 +206,7 @@ struct
let rec zero_init_value ?(varAttr=[]) (t:typ): t =
match t with
| _ when is_mutex_type t -> `Mutex
+ | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
| TInt (ikind, _) -> `Int (ID.of_int ikind BI.zero)
| TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.of_const fkind 0.0)
| TPtr _ -> `Address AD.null_ptr
@@ -215,7 +230,7 @@ struct
| _ -> `Top
let tag_name : t -> string = function
- | `Top -> "Top" | `Int _ -> "Int" | `Float _ -> "Float" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Mutex -> "Mutex" | `Bot -> "Bot"
+ | `Top -> "Top" | `Int _ -> "Int" | `Float _ -> "Float" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Mutex -> "Mutex" | `JmpBuf _ -> "JmpBuf" | `Bot -> "Bot"
include Printable.Std
let name () = "compound"
@@ -240,6 +255,7 @@ struct
| `Array n -> CArrays.pretty () n
| `Blob n -> Blobs.pretty () n
| `Thread n -> Threads.pretty () n
+ | `JmpBuf n -> JmpBufs.pretty () n
| `Mutex -> text "mutex"
| `Bot -> text bot_name
| `Top -> text top_name
@@ -254,6 +270,7 @@ struct
| `Array n -> CArrays.show n
| `Blob n -> Blobs.show n
| `Thread n -> Threads.show n
+ | `JmpBuf n -> JmpBufs.show n
| `Mutex -> "mutex"
| `Bot -> bot_name
| `Top -> top_name
@@ -268,6 +285,7 @@ struct
| (`Array x, `Array y) -> CArrays.pretty_diff () (x,y)
| (`Blob x, `Blob y) -> Blobs.pretty_diff () (x,y)
| (`Thread x, `Thread y) -> Threads.pretty_diff () (x, y)
+ | (`JmpBuf x, `JmpBuf y) -> JmpBufs.pretty_diff () (x, y)
| _ -> dprintf "%s: %a not same type as %a" (name ()) pretty x pretty y
(************************************************************
@@ -376,7 +394,8 @@ struct
match v with
| `Bot
| `Thread _
- | `Mutex ->
+ | `Mutex
+ | `JmpBuf _ ->
v
| _ ->
let log_top (_,l,_,_) = Messages.tracel "cast" "log_top at %d: %a to %a is top!\n" l pretty v d_type t in
@@ -462,7 +481,7 @@ struct
let warn_type op x y =
if GobConfig.get_bool "dbg.verbose" then
- ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name x) (tag_name y) CilType.Location.pretty !Tracing.current_loc pretty x pretty y
+ ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y
let rec leq x y =
match (x,y) with
@@ -485,6 +504,7 @@ struct
| (`Thread x, `Thread y) -> Threads.leq x y
| (`Int x, `Thread y) -> true
| (`Address x, `Thread y) -> true
+ | (`JmpBuf x, `JmpBuf y) -> JmpBufs.leq x y
| (`Mutex, `Mutex) -> true
| _ -> warn_type "leq" x y; false
@@ -517,6 +537,7 @@ struct
| (`Address x, `Thread y)
| (`Thread y, `Address x) ->
`Thread y (* TODO: ignores address! *)
+ | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.join x y)
| (`Mutex, `Mutex) -> `Mutex
| _ ->
warn_type "join" x y;
@@ -551,6 +572,7 @@ struct
| (`Thread y, `Address x) ->
`Thread y (* TODO: ignores address! *)
| (`Mutex, `Mutex) -> `Mutex
+ | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.widen x y)
| _ ->
warn_type "widen" x y;
`Top
@@ -609,6 +631,7 @@ struct
| (`Thread y, `Address x) ->
`Address x (* TODO: ignores thread! *)
| (`Mutex, `Mutex) -> `Mutex
+ | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.meet x y)
| _ ->
warn_type "meet" x y;
`Bot
@@ -625,6 +648,7 @@ struct
| (`Array x, `Array y) -> `Array (CArrays.narrow x y)
| (`Blob x, `Blob y) -> `Blob (Blobs.narrow x y)
| (`Thread x, `Thread y) -> `Thread (Threads.narrow x y)
+ | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.narrow x y)
| (`Int x, `Thread y)
| (`Thread y, `Int x) ->
`Int x (* TODO: ignores thread! *)
@@ -661,6 +685,7 @@ struct
`Array (CArrays.set ask n (array_idx_top) v)
| t , `Blob n -> `Blob (Blobs.invalidate_value ask t n)
| _ , `Thread _ -> state (* TODO: no top thread ID set! *)
+ | _ , `JmpBuf _ -> state (* TODO: no top jmpbuf *)
| _, `Bot -> `Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
| t , _ -> top_value t
@@ -865,7 +890,22 @@ struct
(* consider them in VD *)
let l', o' = shift_one_over l o in
let x = zero_init_calloced_memory orig x (TComp (f.fcomp, [])) in
- mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
+ (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
+ let do_strong_update =
+ match v with
+ | (Var var, Field (fld,_)) ->
+ let toptype = fld.fcomp in
+ let blob_size_opt = ID.to_int s in
+ not @@ ask.f (Q.IsMultiple var)
+ && not @@ Cil.isVoidType t (* Size of value is known *)
+ && Option.is_some blob_size_opt (* Size of blob is known *)
+ && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.bitsSizeOf (TComp (toptype, []))/8)
+ | _ -> false
+ in
+ if do_strong_update then
+ `Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
+ else
+ mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
end
| `Blob (x,s,orig), _ ->
begin
@@ -898,6 +938,17 @@ struct
else
`Top
end
+ | `JmpBuf _, _ ->
+ (* hack for jmp_buf variables *)
+ begin match value with
+ | `JmpBuf t -> value (* if actually assigning jmpbuf, use value *)
+ | `Blob(`Bot, _, _) -> `Bot (* TODO: Stopgap for malloced jmp_bufs, there is something fundamentally flawed somewhere *)
+ | _ ->
+ if !GU.global_initialization then
+ `JmpBuf (JmpBufs.Bufs.empty (), false) (* if assigning global init, use empty set instead *)
+ else
+ `Top
+ end
| _ ->
let result =
match offs with
@@ -1057,6 +1108,14 @@ struct
end
| _ -> v
+ let rec mark_jmpbufs_as_copied (v:t):t =
+ match v with
+ | `JmpBuf (v,t) -> `JmpBuf (v, true)
+ | `Array n -> `Array (CArrays.map (fun (x: t) -> mark_jmpbufs_as_copied x) n)
+ | `Struct n -> `Struct (Structs.map (fun (x: t) -> mark_jmpbufs_as_copied x) n)
+ | `Union (f, n) -> `Union (f, mark_jmpbufs_as_copied n)
+ | `Blob (a,b,c) -> `Blob (mark_jmpbufs_as_copied a, b,c)
+ | _ -> v
let printXml f state =
match state with
@@ -1068,6 +1127,7 @@ struct
| `Array n -> CArrays.printXml f n
| `Blob n -> Blobs.printXml f n
| `Thread n -> Threads.printXml f n
+ | `JmpBuf n -> JmpBufs.printXml f n
| `Mutex -> BatPrintf.fprintf f "\n\nmutex\n\n\n"
| `Bot -> BatPrintf.fprintf f "\n\nbottom\n\n\n"
| `Top -> BatPrintf.fprintf f "\n\ntop\n\n\n"
@@ -1081,6 +1141,7 @@ struct
| `Array n -> CArrays.to_yojson n
| `Blob n -> Blobs.to_yojson n
| `Thread n -> Threads.to_yojson n
+ | `JmpBuf n -> JmpBufs.to_yojson n
| `Mutex -> `String "mutex"
| `Bot -> `String "⊥"
| `Top -> `String "⊤"
diff --git a/src/domains/events.ml b/src/domains/events.ml
index d2fba2abb7..4b96e1c1b0 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -12,6 +12,7 @@ type t =
| UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
| Assert of exp
| Unassume of {exp: CilType.Exp.t; uuids: string list}
+ | Longjmped of {lval: CilType.Lval.t option}
(** Should event be emitted after transfer function raises [Deadcode]? *)
let emit_on_deadcode = function
@@ -26,7 +27,8 @@ let emit_on_deadcode = function
| Assign _
| UpdateExpSplit _ (* Pointless to split on dead. *)
| Unassume _ (* Avoid spurious writes. *)
- | Assert _ -> (* Pointless to refine dead. *)
+ | Assert _ (* Pointless to refine dead. *)
+ | Longjmped _ ->
false
let pretty () = function
@@ -41,3 +43,4 @@ let pretty () = function
| UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
| Assert exp -> dprintf "Assert %a" d_exp exp
| Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids
+ | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
diff --git a/src/domains/flagHelper.ml b/src/domains/flagHelper.ml
index f9ea023d08..7ddf493048 100644
--- a/src/domains/flagHelper.ml
+++ b/src/domains/flagHelper.ml
@@ -6,7 +6,7 @@ end
module FlagHelper (L:Printable.S) (R:Printable.S) (Msg: FlagError) =
struct
- type t = L.t option * R.t option
+ type t = L.t option * R.t option [@@deriving eq, ord, hash]
let unop opl opr (h,r) = match (h, r) with
| (Some l, None) -> opl l
@@ -28,9 +28,6 @@ struct
| (None, Some t1), (None, Some t2) -> (None, Some(opr t1 t2))
| _ -> failwith Msg.msg
- let equal = binop L.equal R.equal
- let hash = unop L.hash R.hash
- let compare = binop L.compare R.compare
let show = unop L.show R.show
let pretty () = unop (L.pretty ()) (R.pretty ())
let printXml f = unop (L.printXml f) (R.printXml f)
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index bac481e8da..f6632610ea 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -43,6 +43,7 @@ end
module LS = SetDomain.ToppedSet (Lval.CilLval) (struct let topname = "All" end)
module TS = SetDomain.ToppedSet (CilType.Typ) (struct let topname = "All" end)
module ES = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Exp) (struct let topname = "All" end))
+module VS = SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All" end)
module VI = Lattice.Flat (Basetype.Variables) (struct
let top_name = "Unknown line"
@@ -116,6 +117,9 @@ type _ t =
| IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *)
| IsMultiple: varinfo -> MustBool.t t (* Is no other copy of this local variable reachable via pointers? *)
| EvalThread: exp -> ConcDomain.ThreadSet.t t
+ | EvalJumpBuf: exp -> JmpBufDomain.JmpBufSet.t t
+ | ActiveJumpBuf: JmpBufDomain.ActiveLongjmps.t t
+ | ValidLongJmp: JmpBufDomain.JmpBufSet.t t
| CreatedThreads: ConcDomain.ThreadSet.t t
| MustJoinedThreads: ConcDomain.MustThreadSet.t t
| MustProtectedVars: mustprotectedvars -> LS.t t
@@ -125,6 +129,7 @@ type _ t =
| IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *)
| MayAccessed: AccessDomain.EventSet.t t
| MayBeTainted: LS.t t
+ | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t
type 'a result = 'a
@@ -172,6 +177,9 @@ struct
| PartAccess _ -> Obj.magic (module Unit: Lattice.S) (* Never used, MCP handles PartAccess specially. Must still return module (instead of failwith) here, but the module is never used. *)
| IsMultiple _ -> (module MustBool) (* see https://github.com/goblint/analyzer/pull/310#discussion_r700056687 on why this needs to be MustBool *)
| EvalThread _ -> (module ConcDomain.ThreadSet)
+ | EvalJumpBuf _ -> (module JmpBufDomain.JmpBufSet)
+ | ActiveJumpBuf -> (module JmpBufDomain.ActiveLongjmps)
+ | ValidLongJmp -> (module JmpBufDomain.JmpBufSet)
| CreatedThreads -> (module ConcDomain.ThreadSet)
| MustJoinedThreads -> (module ConcDomain.MustThreadSet)
| MustProtectedVars _ -> (module LS)
@@ -181,6 +189,7 @@ struct
| IterSysVars _ -> (module Unit)
| MayAccessed -> (module AccessDomain.EventSet)
| MayBeTainted -> (module LS)
+ | MayBeModifiedSinceSetjmp _ -> (module VS)
(** Get bottom result for query. *)
let bot (type a) (q: a t): a result =
@@ -227,6 +236,9 @@ struct
| PartAccess _ -> failwith "Queries.Result.top: PartAccess" (* Never used, MCP handles PartAccess specially. *)
| IsMultiple _ -> MustBool.top ()
| EvalThread _ -> ConcDomain.ThreadSet.top ()
+ | EvalJumpBuf _ -> JmpBufDomain.JmpBufSet.top ()
+ | ActiveJumpBuf -> JmpBufDomain.ActiveLongjmps.top ()
+ | ValidLongJmp -> JmpBufDomain.JmpBufSet.top ()
| CreatedThreads -> ConcDomain.ThreadSet.top ()
| MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
| MustProtectedVars _ -> LS.top ()
@@ -236,6 +248,7 @@ struct
| IterSysVars _ -> Unit.top ()
| MayAccessed -> AccessDomain.EventSet.top ()
| MayBeTainted -> LS.top ()
+ | MayBeModifiedSinceSetjmp _ -> VS.top ()
end
(* The type any_query can't be directly defined in Any as t,
@@ -288,6 +301,10 @@ struct
| Any (PathQuery _) -> 42
| Any DYojson -> 43
| Any (EvalValueYojson _) -> 44
+ | Any (EvalJumpBuf _) -> 45
+ | Any ActiveJumpBuf -> 46
+ | Any ValidLongJmp -> 47
+ | Any (MayBeModifiedSinceSetjmp _) -> 48
let rec compare a b =
let r = Stdlib.compare (order a) (order b) in
@@ -323,11 +340,13 @@ struct
| Any (IsHeapVar v1), Any (IsHeapVar v2) -> CilType.Varinfo.compare v1 v2
| Any (IsMultiple v1), Any (IsMultiple v2) -> CilType.Varinfo.compare v1 v2
| Any (EvalThread e1), Any (EvalThread e2) -> CilType.Exp.compare e1 e2
+ | Any (EvalJumpBuf e1), Any (EvalJumpBuf e2) -> CilType.Exp.compare e1 e2
| Any (WarnGlobal vi1), Any (WarnGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
| Any (Invariant i1), Any (Invariant i2) -> compare_invariant_context i1 i2
| Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
| Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
| Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2
+ | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2
(* only argumentless queries should remain *)
| _, _ -> Stdlib.compare (order a) (order b)
@@ -357,10 +376,15 @@ struct
| Any (IsHeapVar v) -> CilType.Varinfo.hash v
| Any (IsMultiple v) -> CilType.Varinfo.hash v
| Any (EvalThread e) -> CilType.Exp.hash e
+ | Any (EvalJumpBuf e) -> CilType.Exp.hash e
| Any (WarnGlobal vi) -> Hashtbl.hash vi
| Any (Invariant i) -> hash_invariant_context i
| Any (InvariantGlobal vi) -> Hashtbl.hash vi
| Any (MustProtectedVars m) -> hash_mustprotectedvars m
+ | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e
+ (* IterSysVars: *)
+ (* - argument is a function and functions cannot be compared in any meaningful way. *)
+ (* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *)
(* only argumentless queries should remain *)
| _ -> 0
@@ -397,6 +421,9 @@ struct
| Any (IsHeapVar v) -> Pretty.dprintf "IsHeapVar %a" CilType.Varinfo.pretty v
| Any (IsMultiple v) -> Pretty.dprintf "IsMultiple %a" CilType.Varinfo.pretty v
| Any (EvalThread e) -> Pretty.dprintf "EvalThread %a" CilType.Exp.pretty e
+ | Any (EvalJumpBuf e) -> Pretty.dprintf "EvalJumpBuf %a" CilType.Exp.pretty e
+ | Any ActiveJumpBuf -> Pretty.dprintf "ActiveJumpBuf"
+ | Any ValidLongJmp -> Pretty.dprintf "ValidLongJmp"
| Any CreatedThreads -> Pretty.dprintf "CreatedThreads"
| Any MustJoinedThreads -> Pretty.dprintf "MustJoinedThreads"
| Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _"
@@ -407,6 +434,7 @@ struct
| Any MayAccessed -> Pretty.dprintf "MayAccessed"
| Any MayBeTainted -> Pretty.dprintf "MayBeTainted"
| Any DYojson -> Pretty.dprintf "DYojson"
+ | Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf
end
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index d834a6928a..9eead26aa4 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -396,11 +396,16 @@ sig
val enter : (D.t, G.t, C.t, V.t) ctx -> lval option -> fundec -> exp list -> (D.t * D.t) list
val combine : (D.t, G.t, C.t, V.t) ctx -> lval option -> exp -> fundec -> exp list -> C.t option -> D.t -> Queries.ask -> D.t
+ (* Paths as sets: I know this is ugly! *)
+ val paths_as_set : (D.t, G.t, C.t, V.t) ctx -> D.t list
+
(** Returns initial state for created thread. *)
val threadenter : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t list
(** Updates the local state of the creator thread using initial state of created thread. *)
val threadspawn : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
+
+ val event : (D.t, G.t, C.t, V.t) ctx -> Events.t -> (D.t, G.t, C.t, V.t) ctx -> D.t
end
module type MCPA =
@@ -413,7 +418,6 @@ end
module type MCPSpec =
sig
include Spec
- val event : (D.t, G.t, C.t, V.t) ctx -> Events.t -> (D.t, G.t, C.t, V.t) ctx -> D.t
module A: MCPA
val access: (D.t, G.t, C.t, V.t) ctx -> Queries.access -> A.t
@@ -606,6 +610,8 @@ struct
let context fd x = x
(* Everything is context sensitive --- override in MCP and maybe elsewhere*)
+ let paths_as_set ctx = [ctx.local]
+
module A = UnitA
let access _ _ = ()
end
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index 28ca8fab1b..2792d1b92e 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -525,7 +525,7 @@ struct
in
let shape = match n with
| Statement {skind=If (_,_,_,_,_); _} -> ["shape=diamond"]
- | Statement _ -> [] (* use default shape *)
+ | Statement _ -> [] (* use default shape *)
| Function _
| FunctionEntry _ -> ["shape=box"]
in
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 5431dbadb1..602a5ddf5e 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -8,6 +8,7 @@ open GobConfig
module M = Messages
+
(** Lifts a [Spec] so that the domain is [Hashcons]d *)
module HashconsLifter (S:Spec)
: Spec with module D = Lattice.HConsed (S.D)
@@ -80,6 +81,12 @@ struct
let threadspawn ctx lval f args fctx =
D.lift @@ S.threadspawn (conv ctx) lval f args (conv fctx)
+
+ let paths_as_set ctx =
+ List.map (fun x -> D.lift x) @@ S.paths_as_set (conv ctx)
+
+ let event ctx e octx =
+ D.lift @@ S.event (conv ctx) e (conv octx)
end
(** Lifts a [Spec] so that the context is [Hashcons]d. *)
@@ -156,6 +163,9 @@ struct
let threadspawn ctx lval f args fctx =
S.threadspawn (conv ctx) lval f args (conv fctx)
+
+ let paths_as_set ctx = S.paths_as_set (conv ctx)
+ let event ctx e octx = S.event (conv ctx) e (conv octx)
end
(* see option ana.opt.equal *)
@@ -242,6 +252,13 @@ struct
| `Lifted x -> `Lifted (Int64.add x 1L)
| x -> x
+ let paths_as_set ctx =
+ let liftmap = List.map (fun x -> (x, snd ctx.local)) in
+ lift_fun ctx liftmap S.paths_as_set (Fun.id)
+
+ let event ctx e octx =
+ lift_fun ctx (lift ctx) S.event ((|>) (conv octx) % (|>) e)
+
let enter ctx r f args =
let (d,l) = ctx.local in
if leq0 l then
@@ -350,6 +367,8 @@ struct
let skip ctx = lift_fun ctx S.skip identity
let special ctx r f args = lift_fun ctx S.special ((|>) args % (|>) f % (|>) r)
+ let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e)
+
let threadenter ctx lval f args = S.threadenter (conv ctx) lval f args |> List.map (fun d -> (d, snd ctx.local))
let threadspawn ctx lval f args fctx = lift_fun ctx S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
@@ -368,6 +387,10 @@ struct
S.enter (conv ctx) r f args
|> List.map (fun (c,v) -> (c,m), d' v) (* c: caller, v: callee *)
+ let paths_as_set ctx =
+ let m = snd ctx.local in
+ S.paths_as_set (conv ctx) |> List.map (fun v -> (v,m))
+
let combine ctx r fe f args fc es f_ask = lift_fun ctx S.combine (fun p -> p r fe f args fc (fst es) f_ask)
end
@@ -416,6 +439,10 @@ struct
let liftmap = List.map (fun (x,y) -> D.lift x, D.lift y) in
lift_fun ctx liftmap S.enter ((|>) args % (|>) f % (|>) r) []
+ let paths_as_set ctx =
+ let liftmap = List.map (fun x -> D.lift x) in
+ lift_fun ctx liftmap S.paths_as_set (Fun.id) []
+
let query ctx (type a) (q: a Queries.t): a Queries.result =
lift_fun ctx identity S.query (fun (x) -> x q) (Queries.Result.bot q)
let assign ctx lv e = lift_fun ctx D.lift S.assign ((|>) e % (|>) lv) `Bot
@@ -430,6 +457,8 @@ struct
let threadenter ctx lval f args = lift_fun ctx (List.map D.lift) S.threadenter ((|>) args % (|>) f % (|>) lval) []
let threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
+
+ let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
end
module type Increment =
@@ -618,20 +647,37 @@ struct
let tf_normal_call ctx lv e (f:fundec) args getl sidel getg sideg =
let combine (cd, fc, fd) =
if M.tracing then M.traceli "combine" "local: %a\n" S.D.pretty cd;
- (* Extra sync in case function has multiple returns.
- Each `Return sync is done before joining, so joined value may be unsound.
- Since sync is normally done before tf (in common_ctx), simulate it here for fd. *)
- (* TODO: don't do this extra sync here *)
- let rec sync_ctx = { ctx with
- ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q);
- local = fd;
- prev_node = Function f
- }
+ let rec cd_ctx =
+ { ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query cd_ctx q);
+ local = cd;
+ }
+ in
+ let fd_ctx =
+ (* Inner scope to prevent unsynced fd_ctx from being used. *)
+ (* Extra sync in case function has multiple returns.
+ Each `Return sync is done before joining, so joined value may be unsound.
+ Since sync is normally done before tf (in common_ctx), simulate it here for fd. *)
+ (* TODO: don't do this extra sync here *)
+ let rec sync_ctx =
+ { ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q);
+ local = fd;
+ prev_node = Function f;
+ }
+ in
+ (* TODO: more accurate ctx? *)
+ let synced = sync sync_ctx in
+ let rec fd_ctx =
+ { sync_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query fd_ctx q);
+ local = synced;
+ }
+ in
+ fd_ctx
in
- (* TODO: more accurate ctx? *)
- let fd = sync sync_ctx in
if M.tracing then M.trace "combine" "function: %a\n" S.D.pretty fd;
- let r = S.combine {ctx with local = cd} lv e f args fc fd (Analyses.ask_of_ctx sync_ctx) in
+ let r = S.combine cd_ctx lv e f args fc fd_ctx.local (Analyses.ask_of_ctx fd_ctx) in
if M.tracing then M.traceu "combine" "combined local: %a\n" S.D.pretty r;
r
in
@@ -639,7 +685,8 @@ struct
let paths = List.map (fun (c,v) -> (c, S.context f v, v)) paths in
List.iter (fun (c,fc,v) -> if not (S.D.is_bot v) then sidel (FunctionEntry f, fc) v) paths;
let paths = List.map (fun (c,fc,v) -> (c, fc, if S.D.is_bot v then v else getl (Function f, fc))) paths in
- let paths = List.filter (fun (c,fc,v) -> not (D.is_bot v)) paths in
+ (* Don't filter bot paths, otherwise LongjmpLifter is not called. *)
+ (* let paths = List.filter (fun (c,fc,v) -> not (D.is_bot v)) paths in *)
let paths = List.map (Tuple3.map2 Option.some) paths in
if M.tracing then M.traceli "combine" "combining\n";
let paths = List.map combine paths in
@@ -1162,6 +1209,10 @@ struct
let skip ctx = map ctx Spec.skip identity
let special ctx l f a = map ctx Spec.special (fun h -> h l f a)
+ let event ctx e octx =
+ let fd1 = D.choose octx.local in
+ map ctx Spec.event (fun h -> h e (conv octx fd1))
+
let threadenter ctx lval f args =
let g xs ys = (List.map (fun y -> D.singleton y) ys) @ xs in
fold' ctx Spec.threadenter (fun h -> h lval f args) g []
@@ -1181,6 +1232,11 @@ struct
let g xs ys = (List.map (fun (x,y) -> D.singleton x, D.singleton y) ys) @ xs in
fold' ctx Spec.enter (fun h -> h l f a) g []
+ let paths_as_set ctx =
+ (* Path-sensitivity is only here, not below! *)
+ let elems = D.elements ctx.local in
+ List.map (D.singleton) elems
+
let combine ctx l fe f a fc d f_ask =
assert (D.cardinal ctx.local = 1);
let cd = D.choose ctx.local in
@@ -1316,6 +1372,7 @@ struct
let assign ctx = S.assign (conv ctx)
let vdecl ctx = S.vdecl (conv ctx)
let enter ctx = S.enter (conv ctx)
+ let paths_as_set ctx = S.paths_as_set (conv ctx)
let body ctx = S.body (conv ctx)
let return ctx = S.return (conv ctx)
let combine ctx = S.combine (conv ctx)
@@ -1325,6 +1382,240 @@ struct
let sync ctx = S.sync (conv ctx)
let skip ctx = S.skip (conv ctx)
let asm ctx = S.asm (conv ctx)
+ let event ctx e octx = S.event (conv ctx) e (conv octx)
+end
+
+module LongjmpLifter (S: Spec): Spec =
+struct
+ include S
+
+ let name () = "Longjmp (" ^ S.name () ^ ")"
+
+ module V =
+ struct
+ include Printable.Either (S.V) (Printable.Either (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C)))
+ let s x = `Left x
+ let longjmpto x = `Right (`Left x)
+ let longjmpret x = `Right (`Right x)
+ let is_write_only = function
+ | `Left x -> S.V.is_write_only x
+ | `Right _ -> false
+ end
+
+ module G =
+ struct
+ include Lattice.Lift2 (S.G) (S.D) (Printable.DefaultNames)
+
+ let s = function
+ | `Bot -> S.G.bot ()
+ | `Lifted1 x -> x
+ | _ -> failwith "LongjmpLifter.s"
+ let local = function
+ | `Bot -> S.D.bot ()
+ | `Lifted2 x -> x
+ | _ -> failwith "LongjmpLifter.local"
+ let create_s s = `Lifted1 s
+ let create_local local = `Lifted2 local
+
+ let printXml f = function
+ | `Lifted1 x -> S.G.printXml f x
+ | `Lifted2 x -> BatPrintf.fprintf f "%a" S.D.printXml x
+ | x -> BatPrintf.fprintf f "%a" printXml x
+ end
+
+ let conv (ctx: (_, G.t, _, V.t) ctx): (_, S.G.t, _, S.V.t) ctx =
+ { ctx with
+ global = (fun v -> G.s (ctx.global (V.s v)));
+ sideg = (fun v g -> ctx.sideg (V.s v) (G.create_s g));
+ }
+
+ let query ctx (type a) (q: a Queries.t): a Queries.result =
+ match q with
+ | WarnGlobal g ->
+ let g: V.t = Obj.obj g in
+ begin match g with
+ | `Left g ->
+ S.query (conv ctx) (WarnGlobal (Obj.repr g))
+ | `Right g ->
+ Queries.Result.top q
+ end
+ | InvariantGlobal g ->
+ let g: V.t = Obj.obj g in
+ begin match g with
+ | `Left g ->
+ S.query (conv ctx) (InvariantGlobal (Obj.repr g))
+ | `Right g ->
+ Queries.Result.top q
+ end
+ | IterSysVars (vq, vf) ->
+ (* vars for S *)
+ let vf' x = vf (Obj.repr (V.s (Obj.obj x))) in
+ S.query (conv ctx) (IterSysVars (vq, vf'));
+ (* TODO: vars? *)
+ | _ ->
+ S.query (conv ctx) q
+
+
+ let branch ctx = S.branch (conv ctx)
+ let assign ctx = S.assign (conv ctx)
+ let vdecl ctx = S.vdecl (conv ctx)
+ let enter ctx = S.enter (conv ctx)
+ let paths_as_set ctx = S.paths_as_set (conv ctx)
+ let body ctx = S.body (conv ctx)
+ let return ctx = S.return (conv ctx)
+
+ let combine ctx lv e f args fc fd f_ask =
+ let conv_ctx = conv ctx in
+ let current_fundec = Node.find_fundec ctx.node in
+ let handle_longjmp (cd, fc, longfd) =
+ (* This is called per-path. *)
+ let rec cd_ctx =
+ { conv_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query cd_ctx q);
+ local = cd;
+ }
+ in
+ let longfd_ctx =
+ (* Inner scope to prevent unsynced longfd_ctx from being used. *)
+ (* Extra sync like with normal combine. *)
+ let rec sync_ctx =
+ { conv_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q);
+ local = longfd;
+ prev_node = Function f;
+ }
+ in
+ let synced = S.sync sync_ctx `Join in
+ let rec longfd_ctx =
+ { sync_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query longfd_ctx q);
+ local = synced;
+ }
+ in
+ longfd_ctx
+ in
+ let combined = lazy ( (* does not depend on target, do at most once *)
+ (* Globals are non-problematic here, as they are always carried around without any issues! *)
+ (* A combine call is mostly needed to ensure locals have appropriate values. *)
+ (* Using f from called function on purpose here! Needed? *)
+ S.combine cd_ctx None e f args fc longfd_ctx.local (Analyses.ask_of_ctx longfd_ctx) (* no lval because longjmp return skips return value assignment *)
+ )
+ in
+ let returned = lazy ( (* does not depend on target, do at most once *)
+ let rec combined_ctx =
+ { cd_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query combined_ctx q);
+ local = Lazy.force combined;
+ }
+ in
+ S.return combined_ctx None current_fundec
+ )
+ in
+ let (active_targets, _) = longfd_ctx.ask ActiveJumpBuf in
+ let valid_targets = cd_ctx.ask ValidLongJmp in
+ let handle_target target = match target with
+ | JmpBufDomain.BufferEntryOrTop.AllTargets -> () (* The warning is already emitted at the point where the longjmp happens *)
+ | Target (target_node, target_context) ->
+ let target_fundec = Node.find_fundec target_node in
+ if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (ctx.control_context ()) then (
+ if M.tracing then Messages.tracel "longjmp" "Fun: Potentially from same context, side-effect to %a\n" Node.pretty target_node;
+ ctx.sideg (V.longjmpto (target_node, ctx.context ())) (G.create_local (Lazy.force combined))
+ (* No need to propagate this outwards here, the set of valid longjumps is part of the context, we can never have the same context setting the longjmp multiple times *)
+ )
+ (* Appropriate setjmp is not in current function & current context *)
+ else if JmpBufDomain.JmpBufSet.mem target valid_targets then
+ ctx.sideg (V.longjmpret (current_fundec, ctx.context ())) (G.create_local (Lazy.force returned))
+ else
+ (* It actually is not handled here but was propagated here spuriously, we already warned at the location where this issue is caused *)
+ (* As the validlongjumps inside the callee is a a superset of the ones inside the caller *)
+ ()
+ in
+ JmpBufDomain.JmpBufSet.iter handle_target active_targets
+ in
+ if M.tracing then M.tracel "longjmp" "longfd getg %a\n" CilType.Fundec.pretty f;
+ let longfd = G.local (ctx.global (V.longjmpret (f, Option.get fc))) in
+ if M.tracing then M.tracel "longjmp" "longfd %a\n" D.pretty longfd;
+ if not (D.is_bot longfd) then
+ handle_longjmp (ctx.local, fc, longfd);
+ S.combine (conv_ctx) lv e f args fc fd f_ask
+
+ let special ctx lv f args =
+ let conv_ctx = conv ctx in
+ match (LibraryFunctions.find f).special args with
+ | Setjmp {env} ->
+ (* Handling of returning for the first time *)
+ let normal_return = S.special conv_ctx lv f args in
+ let jmp_return = G.local (ctx.global (V.longjmpto (ctx.prev_node, ctx.context ()))) in
+ if S.D.is_bot jmp_return then
+ normal_return
+ else (
+ let rec jmp_ctx =
+ { conv_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query jmp_ctx q);
+ local = jmp_return;
+ }
+ in
+ let longjmped = S.event jmp_ctx (Events.Longjmped {lval=lv}) jmp_ctx in
+ S.D.join normal_return longjmped
+ )
+ | Longjmp {env; value} ->
+ let current_fundec = Node.find_fundec ctx.node in
+ let handle_path path = (
+ let rec path_ctx =
+ { conv_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query path_ctx q);
+ local = path;
+ }
+ in
+ let specialed = lazy ( (* does not depend on target, do at most once *)
+ S.special path_ctx lv f args
+ )
+ in
+ let returned = lazy ( (* does not depend on target, do at most once *)
+ let rec specialed_ctx =
+ { path_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query specialed_ctx q);
+ local = Lazy.force specialed;
+ }
+ in
+ S.return specialed_ctx None current_fundec
+ )
+ in
+ (* Eval `env` again to avoid having to construct bespoke ctx to ask *)
+ let targets = path_ctx.ask (EvalJumpBuf env) in
+ let valid_targets = path_ctx.ask ValidLongJmp in
+ if M.tracing then Messages.tracel "longjmp" "Jumping to %a\n" JmpBufDomain.JmpBufSet.pretty targets;
+ let handle_target target = match target with
+ | JmpBufDomain.BufferEntryOrTop.AllTargets ->
+ M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env
+ | Target (target_node, target_context) ->
+ let target_fundec = Node.find_fundec target_node in
+ if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (ctx.control_context ()) then (
+ if M.tracing then Messages.tracel "longjmp" "Potentially from same context, side-effect to %a\n" Node.pretty target_node;
+ ctx.sideg (V.longjmpto (target_node, ctx.context ())) (G.create_local (Lazy.force specialed))
+ )
+ else if JmpBufDomain.JmpBufSet.mem target valid_targets then (
+ if M.tracing then Messages.tracel "longjmp" "Longjmp to somewhere else, side-effect to %i\n" (S.C.hash (ctx.context ()));
+ ctx.sideg (V.longjmpret (current_fundec, ctx.context ())) (G.create_local (Lazy.force returned))
+ )
+ else
+ M.warn ~category:(Behavior (Undefined Other)) "Longjmp to potentially invalid target! (Target %a in Function %a which may have already returned or is in a different thread)" Node.pretty target_node CilType.Fundec.pretty target_fundec
+ in
+ if JmpBufDomain.JmpBufSet.is_empty targets then
+ M.warn ~category:(Behavior (Undefined Other)) "Longjmp to potentially invalid target (%a is bot?!)" d_exp env
+ else
+ JmpBufDomain.JmpBufSet.iter handle_target targets
+ )
+ in
+ List.iter handle_path (S.paths_as_set conv_ctx);
+ S.D.bot ()
+ | _ -> S.special conv_ctx lv f args
+ let threadenter ctx = S.threadenter (conv ctx)
+ let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
+ let sync ctx = S.sync (conv ctx)
+ let skip ctx = S.skip (conv ctx)
+ let asm ctx = S.asm (conv ctx)
+ let event ctx e octx = S.event (conv ctx) e (conv octx)
end
module CompareGlobSys (SpecSys: SpecSys) =
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 2d18814ad2..656f8883bb 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -33,6 +33,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
(* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
|> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
+ |> lift true (module LongjmpLifter)
) in
GobConfig.building_spec := false;
ControlSpecC.control_spec_c := (module S1.C);
diff --git a/src/framework/node.ml b/src/framework/node.ml
index 36f1722615..451c2d6db3 100644
--- a/src/framework/node.ml
+++ b/src/framework/node.ml
@@ -54,7 +54,7 @@ let show_cfg = function
let find_fundec (node: t) =
match node with
| Statement stmt -> Cilfacade.find_stmt_fundec stmt
- | Function fd -> fd
+ | Function fd
| FunctionEntry fd -> fd
(** @raise Not_found *)
@@ -70,4 +70,3 @@ let of_id s =
| "ret" -> Function fundec
| "fun" -> FunctionEntry fundec
| _ -> raise Not_found
-
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 5387c11b57..3f0c7dd779 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -18,6 +18,13 @@ let isFloatType t =
| TFloat _ -> true
| _ -> false
+let rec isVLAType t =
+ match Cil.unrollType t with
+ | TArray (et, len, _) ->
+ let variable_len = GobOption.exists (Fun.negate Cil.isConstant) len in
+ variable_len || isVLAType et
+ | _ -> false
+
let init_options () =
Mergecil.merge_inlines := get_bool "cil.merge.inlines";
Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index c231559173..057720f776 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -332,7 +332,7 @@
"default": [
"expRelation", "base", "threadid", "threadflag", "threadreturn",
"escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
- "assert"
+ "assert","activeLongjmp","activeSetjmp","taintPartialContexts","modifiedSinceLongjmp","poisonVariables","expsplit","vla"
]
},
"path_sens": {
@@ -340,7 +340,7 @@
"description": "List of path-sensitive analyses",
"type": "array",
"items": { "type": "string" },
- "default": [ "mutex", "malloc_null", "uninit", "expsplit" ]
+ "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp" ]
},
"ctx_insens": {
"title": "ana.ctx_insens",
@@ -349,6 +349,21 @@
"items": { "type": "string" },
"default": [ "stack_loc", "stack_trace_set" ]
},
+ "setjmp" : {
+ "title": "ana.setjmp",
+ "description": "Setjmp/Longjmp analysis",
+ "type": "object",
+ "properties": {
+ "split": {
+ "title": "ana.setjmp.split",
+ "description": "Split returns of setjmp",
+ "type": "string",
+ "enum": ["none", "coarse", "precise"],
+ "default": "precise"
+ }
+ },
+ "additionalProperties": false
+ },
"int": {
"title": "ana.int",
"type": "object",
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index 3c225c3509..04b1af62f6 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -152,6 +152,10 @@ struct
let lift' d ts = (d, ts)
+ let paths_as_set ctx =
+ let liftmap l ts = List.map (fun x -> (x, ts)) l in
+ lift_fun ctx liftmap S.paths_as_set (Fun.id)
+
let sync ctx reason = lift_fun ctx lift' S.sync ((|>) reason)
let enter ctx r f args =
@@ -172,4 +176,5 @@ struct
let threadenter ctx lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) S.threadenter ((|>) args % (|>) f % (|>) lval)
let threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+ let event ctx e octx = lift_fun ctx lift' S.event ((|>) (conv octx) % (|>) e)
end
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 838941c50f..2e2e146659 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -157,6 +157,19 @@ struct
let d = Dom.fold_keys h (fst ctx.local) (Dom.empty (), Sync.bot ()) in
if Dom.is_bot (fst d) then raise Deadcode else d
+ (* TODO???? *)
+ let map_event ctx e =
+ (* we now use Sync for every tf such that threadspawn after tf could look up state before tf *)
+ let h x (xs, sync) =
+ try
+ let x' = Spec.event (conv ctx x) e (conv ctx x) in
+ (Dom.add x' (step_ctx_edge ctx x) xs, Sync.add x' (SyncSet.singleton x) sync)
+ with Deadcode -> (xs, sync)
+ in
+ let d = Dom.fold_keys h (fst ctx.local) (Dom.empty (), Sync.bot ()) in
+ if Dom.is_bot (fst d) then raise Deadcode else d
+
+
let fold' ctx f g h a =
let k x a =
try h a x @@ g @@ f @@ conv ctx x
@@ -179,6 +192,12 @@ struct
let asm ctx = map ctx Spec.asm identity
let skip ctx = map ctx Spec.skip identity
let special ctx l f a = map ctx Spec.special (fun h -> h l f a)
+ let event ctx e octx = map_event ctx e (* TODO: ???? *)
+
+ let paths_as_set ctx =
+ let (a,b) = ctx.local in
+ let r = Dom.bindings a in
+ List.map (fun (x,v) -> (Dom.singleton x v, b)) r
let threadenter ctx lval f args =
let g xs x' ys =
@@ -259,7 +278,7 @@ struct
in
fold' ctx Spec.enter (fun h -> h l f a) g []
- let combine ctx l fe f a fc d f_ask =
+ let combine ctx l fe f a fc d f_ask =
assert (Dom.cardinal (fst ctx.local) = 1);
let cd = Dom.choose_key (fst ctx.local) in
let k x (y, sync) =
diff --git a/tests/incremental/13-restart-write/05-race-call-remove.c b/tests/incremental/13-restart-write/05-race-call-remove.c
index 599b753320..c07962ad78 100644
--- a/tests/incremental/13-restart-write/05-race-call-remove.c
+++ b/tests/incremental/13-restart-write/05-race-call-remove.c
@@ -16,4 +16,4 @@ int main() {
pthread_create(&id, NULL, t_fun, NULL);
foo();
return 0;
-}
\ No newline at end of file
+}
diff --git a/tests/regression/11-heap/15-malloc_unique_addresses_struct.c b/tests/regression/11-heap/15-malloc_unique_addresses_struct.c
new file mode 100644
index 0000000000..1f49c53dc2
--- /dev/null
+++ b/tests/regression/11-heap/15-malloc_unique_addresses_struct.c
@@ -0,0 +1,26 @@
+// PARAM: --set ana.malloc.unique_address_count 1
+
+#include
+#include
+#include
+
+struct s {
+ int x;
+ int y;
+};
+
+int main() {
+ struct s *ptr = malloc(sizeof(struct s));
+ int p;
+
+ ptr->x = 0;
+ ptr->y = 1;
+
+ __goblint_check(ptr->x == 0);
+ __goblint_check(ptr->y == 1);
+
+ ptr->x = 1;
+ ptr->y = 0;
+ __goblint_check(ptr->x == 1);
+ __goblint_check(ptr->y == 0);
+}
diff --git a/tests/regression/68-longjmp/01-setjmp-return.c b/tests/regression/68-longjmp/01-setjmp-return.c
new file mode 100644
index 0000000000..3a3eb3137c
--- /dev/null
+++ b/tests/regression/68-longjmp/01-setjmp-return.c
@@ -0,0 +1,31 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never
+#include
+#include
+#include
+
+int main(void)
+{
+ jmp_buf jmp_buf;
+
+ __goblint_check(1);
+ switch (setjmp(jmp_buf))
+ {
+ case 0:
+ __goblint_check(1);
+ longjmp(jmp_buf, 1);
+ __goblint_check(0); // NOWARN
+ break;
+ case 1:
+ __goblint_check(1);
+ break;
+ case 2:
+ __goblint_check(0); // NOWARN
+ break;
+ default:
+ __goblint_check(0); // NOWARN
+ break;
+ }
+ __goblint_check(1);
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/02-setjmp-global.c b/tests/regression/68-longjmp/02-setjmp-global.c
new file mode 100644
index 0000000000..c5e256df9a
--- /dev/null
+++ b/tests/regression/68-longjmp/02-setjmp-global.c
@@ -0,0 +1,34 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never
+#include
+#include
+
+int global = 0;
+jmp_buf jmp_buffer;
+
+int main(void)
+{
+
+ __goblint_check(1);
+ setjmp(jmp_buffer);
+ switch (global)
+ {
+ case 0:
+ __goblint_check(1);
+ global = 1;
+ longjmp(jmp_buffer, 1);
+ __goblint_check(0); // NOWARN
+ break;
+ case 1:
+ __goblint_check(1);
+ break;
+ case 2:
+ __goblint_check(0); // NOWARN
+ break;
+ default:
+ __goblint_check(0); // NOWARN
+ break;
+ }
+ __goblint_check(1);
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/03-setjmp-local.c b/tests/regression/68-longjmp/03-setjmp-local.c
new file mode 100644
index 0000000000..8cc9676b55
--- /dev/null
+++ b/tests/regression/68-longjmp/03-setjmp-local.c
@@ -0,0 +1,34 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never --disable exp.volatiles_are_top
+#include
+#include
+
+
+int main(void)
+{
+ jmp_buf jmp_buf;
+ volatile int local = 0;
+
+ __goblint_check(1);
+ setjmp(jmp_buf);
+ switch (local)
+ {
+ case 0:
+ __goblint_check(1);
+ local = 1;
+ longjmp(jmp_buf, 1);
+ __goblint_check(0); // NOWARN
+ break;
+ case 1:
+ __goblint_check(1);
+ break;
+ case 2:
+ __goblint_check(0); // NOWARN
+ break;
+ default:
+ __goblint_check(0); // NOWARN
+ break;
+ }
+ __goblint_check(1);
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/04-counting-local.c b/tests/regression/68-longjmp/04-counting-local.c
new file mode 100644
index 0000000000..691985a61a
--- /dev/null
+++ b/tests/regression/68-longjmp/04-counting-local.c
@@ -0,0 +1,25 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --disable exp.volatiles_are_top --set solvers.td3.side_widen never
+#include
+#include
+
+jmp_buf my_jump_buffer;
+
+void foo(int count)
+{
+ __goblint_check(count >= 0 && count <= 5);
+ longjmp(my_jump_buffer, 1);
+ __goblint_check(0); // NOWARN
+}
+
+int main(void)
+{
+ volatile int count = 0;
+ setjmp(my_jump_buffer);
+ __goblint_check(count == 0); // UNKNOWN!
+ if (count < 5) {
+ count++;
+ foo(count);
+ __goblint_check(0); // NOWARN
+ }
+ __goblint_check(count == 5);
+}
diff --git a/tests/regression/68-longjmp/05-heap-counting-return-one-method.c b/tests/regression/68-longjmp/05-heap-counting-return-one-method.c
new file mode 100644
index 0000000000..1b40c3c31d
--- /dev/null
+++ b/tests/regression/68-longjmp/05-heap-counting-return-one-method.c
@@ -0,0 +1,18 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never --enable exp.earlyglobs --set ana.setjmp.split none --disable exp.volatiles_are_top
+#include
+#include
+#include
+
+int main(void)
+{
+ jmp_buf* my_jump_buffer = malloc(sizeof(jmp_buf));
+
+ volatile int count = setjmp(*my_jump_buffer);
+ __goblint_check(count == 0); // UNKNOWN!
+ if (count < 5) {
+ __goblint_check(count >= 0 & count < 5);
+ longjmp(*my_jump_buffer, count + 1);
+ __goblint_check(0); // NOWARN
+ }
+ __goblint_check(count == 5);
+}
diff --git a/tests/regression/68-longjmp/06-sigsetjmp-return.c b/tests/regression/68-longjmp/06-sigsetjmp-return.c
new file mode 100644
index 0000000000..33e5253a3a
--- /dev/null
+++ b/tests/regression/68-longjmp/06-sigsetjmp-return.c
@@ -0,0 +1,30 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never
+#include
+#include
+
+int main(void)
+{
+ jmp_buf jmp_buf;
+
+ __goblint_check(1);
+ switch (sigsetjmp(jmp_buf,0))
+ {
+ case 0:
+ __goblint_check(1);
+ longjmp(jmp_buf, 1);
+ __goblint_check(0); // NOWARN
+ break;
+ case 1:
+ __goblint_check(1);
+ break;
+ case 2:
+ __goblint_check(0); // NOWARN
+ break;
+ default:
+ __goblint_check(0); // NOWARN
+ break;
+ }
+ __goblint_check(1);
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/07-returns.c b/tests/regression/68-longjmp/07-returns.c
new file mode 100644
index 0000000000..b962662f34
--- /dev/null
+++ b/tests/regression/68-longjmp/07-returns.c
@@ -0,0 +1,28 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --disable exp.volatiles_are_top --set solvers.td3.side_widen never
+#include
+#include
+
+jmp_buf my_jump_buffer;
+
+int foo(int count)
+{
+ __goblint_check(count >= 0 && count <= 5);
+ longjmp(my_jump_buffer, -10);
+ __goblint_check(0); // NOWARN
+ return 8;
+}
+
+int main(void)
+{
+ volatile int count = 0;
+ int x = setjmp(my_jump_buffer);
+ if( x == -10) {
+ __goblint_check(1);
+ return -1;
+ }
+ if( x > 0) {
+ __goblint_check(0); //NOWARN
+ }
+
+ foo(count);
+}
diff --git a/tests/regression/68-longjmp/11-counting-return.c b/tests/regression/68-longjmp/11-counting-return.c
new file mode 100644
index 0000000000..682b402e01
--- /dev/null
+++ b/tests/regression/68-longjmp/11-counting-return.c
@@ -0,0 +1,23 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never --set ana.setjmp.split none
+#include
+#include
+
+jmp_buf my_jump_buffer;
+
+void foo(int count)
+{
+ __goblint_check(count >= 0 && count < 5);
+ longjmp(my_jump_buffer, count + 1);
+ __goblint_check(0); // NOWARN
+}
+
+int main(void)
+{
+ int count = setjmp(my_jump_buffer);
+ __goblint_check(count == 0); // UNKNOWN!
+ if (count < 5) {
+ foo(count);
+ __goblint_check(0); // NOWARN
+ }
+ __goblint_check(count == 5);
+}
diff --git a/tests/regression/68-longjmp/12-counting-global.c b/tests/regression/68-longjmp/12-counting-global.c
new file mode 100644
index 0000000000..8b8847870f
--- /dev/null
+++ b/tests/regression/68-longjmp/12-counting-global.c
@@ -0,0 +1,25 @@
+//PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never
+#include
+#include
+
+jmp_buf my_jump_buffer;
+int count = 0;
+
+void foo()
+{
+ __goblint_check(count >= 0 && count < 5);
+ count++;
+ longjmp(my_jump_buffer, 1);
+ __goblint_check(0); // NOWARN
+}
+
+int main(void)
+{
+ setjmp(my_jump_buffer);
+ __goblint_check(count == 0); // UNKNOWN!
+ if (count < 5) {
+ foo();
+ __goblint_check(0); // NOWARN
+ }
+ __goblint_check(count == 5);
+}
diff --git a/tests/regression/68-longjmp/13-counting-local.c b/tests/regression/68-longjmp/13-counting-local.c
new file mode 100644
index 0000000000..4751138286
--- /dev/null
+++ b/tests/regression/68-longjmp/13-counting-local.c
@@ -0,0 +1,25 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never --disable exp.volatiles_are_top
+#include
+#include
+
+jmp_buf my_jump_buffer;
+
+void foo(int count)
+{
+ __goblint_check(count >= 0 && count <= 5);
+ longjmp(my_jump_buffer, 1);
+ __goblint_check(0); // NOWARN
+}
+
+int main(void)
+{
+ volatile int count = 0;
+ setjmp(my_jump_buffer);
+ __goblint_check(count == 0); // UNKNOWN!
+ if (count < 5) {
+ count++;
+ foo(count);
+ __goblint_check(0); // NOWARN
+ }
+ __goblint_check(count == 5);
+}
diff --git a/tests/regression/68-longjmp/14-counting-return-one-method.c b/tests/regression/68-longjmp/14-counting-return-one-method.c
new file mode 100644
index 0000000000..651c9f85e1
--- /dev/null
+++ b/tests/regression/68-longjmp/14-counting-return-one-method.c
@@ -0,0 +1,17 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never --set ana.setjmp.split none
+#include
+#include
+
+jmp_buf my_jump_buffer;
+
+int main(void)
+{
+ int count = setjmp(my_jump_buffer);
+ __goblint_check(count == 0); // UNKNOWN!
+ if (count < 5) {
+ __goblint_check(count >= 0 && count < 5);
+ longjmp(my_jump_buffer, count + 1);
+ __goblint_check(0); // NOWARN
+ }
+ __goblint_check(count == 5);
+}
diff --git a/tests/regression/68-longjmp/15-counting-global-one-method.c b/tests/regression/68-longjmp/15-counting-global-one-method.c
new file mode 100644
index 0000000000..7b476afc15
--- /dev/null
+++ b/tests/regression/68-longjmp/15-counting-global-one-method.c
@@ -0,0 +1,19 @@
+//PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never
+#include
+#include
+
+jmp_buf my_jump_buffer;
+int count = 0;
+
+int main(void)
+{
+ setjmp(my_jump_buffer);
+ __goblint_check(count == 0); // UNKNOWN!
+ if (count < 5) {
+ __goblint_check(count >= 0 && count < 5);
+ count++;
+ longjmp(my_jump_buffer, 1);
+ __goblint_check(0); // NOWARN
+ }
+ __goblint_check(count == 5);
+}
diff --git a/tests/regression/68-longjmp/16-counting-local-one-method.c b/tests/regression/68-longjmp/16-counting-local-one-method.c
new file mode 100644
index 0000000000..51ca3b8ab0
--- /dev/null
+++ b/tests/regression/68-longjmp/16-counting-local-one-method.c
@@ -0,0 +1,19 @@
+//PARAM: --enable ana.int.interval --enable ana.int.enums --set solvers.td3.side_widen never --disable exp.volatiles_are_top
+#include
+#include
+
+jmp_buf my_jump_buffer;
+
+int main(void)
+{
+ volatile int count = 0;
+ setjmp(my_jump_buffer);
+ __goblint_check(count == 0); // UNKNOWN!
+ if (count < 5) {
+ count++;
+ __goblint_check(count >= 0 && count <= 5);
+ longjmp(my_jump_buffer, 1);
+ __goblint_check(0); // NOWARN
+ }
+ __goblint_check(count == 5);
+}
diff --git a/tests/regression/68-longjmp/17-loop.c b/tests/regression/68-longjmp/17-loop.c
new file mode 100644
index 0000000000..a0d7836f4c
--- /dev/null
+++ b/tests/regression/68-longjmp/17-loop.c
@@ -0,0 +1,30 @@
+//PARAM: --set ana.setjmp.split coarse
+#include
+#include
+#include
+#include
+
+void jmpfunction(jmp_buf env_buf) {
+ longjmp(env_buf, 2);
+}
+
+int main () {
+ int val;
+ jmp_buf env_buffer;
+
+ /* save calling environment for longjmp */
+ val = setjmp( env_buffer ); // NOWARN
+
+ if( val != 0 ) { // NOWARN
+ printf("Returned from a longjmp() with value = %i\n", val);
+ longjmp(env_buffer, val+1);
+ exit(0);
+ }
+
+ printf("Jump function call\n");
+ jmpfunction( env_buffer );
+
+ __goblint_check(0); // NOWARN
+
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/18-simple-else.c b/tests/regression/68-longjmp/18-simple-else.c
new file mode 100644
index 0000000000..af1fdb97ad
--- /dev/null
+++ b/tests/regression/68-longjmp/18-simple-else.c
@@ -0,0 +1,40 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set ana.setjmp.split none
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int fun() {
+ global = 2;
+ longjmp(env_buffer, 2);
+}
+
+
+int main () {
+ int val;
+ jmp_buf env_buffer2;
+
+ __goblint_check(global == 0);
+
+ /* save calling environment for longjmp */
+ val = setjmp( env_buffer );
+
+ __goblint_check(global == 0); //UNKNOWN!
+ __goblint_check(global == 2); //UNKNOWN!
+ __goblint_check(global == 8); //FAIL!
+
+ if( val != 0 ) {
+ printf("Returned from a longjmp() with value = %i\n", val);
+ __goblint_check(val == 2);
+ __goblint_check(global == 2); //TODO (requires path-sensitivity distinguishing between returns) -> see test 44
+ exit(0);
+ }
+
+ fun();
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/19-simpler.c b/tests/regression/68-longjmp/19-simpler.c
new file mode 100644
index 0000000000..b928ce08d0
--- /dev/null
+++ b/tests/regression/68-longjmp/19-simpler.c
@@ -0,0 +1,24 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int fun() {
+ longjmp(env_buffer, 2);
+}
+
+
+int main () {
+ int val;
+
+ __goblint_check(global == 0);
+ setjmp( env_buffer );
+ fun();
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/20-simpler-multifun.c b/tests/regression/68-longjmp/20-simpler-multifun.c
new file mode 100644
index 0000000000..0213cd015d
--- /dev/null
+++ b/tests/regression/68-longjmp/20-simpler-multifun.c
@@ -0,0 +1,30 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+void foo() {
+ int local = 7;
+ longjmp(env_buffer, 2);
+}
+
+
+int fun() {
+ foo();
+}
+
+
+int main () {
+ int val;
+
+ __goblint_check(global == 0);
+ setjmp( env_buffer );
+ fun();
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/21-multifun.c b/tests/regression/68-longjmp/21-multifun.c
new file mode 100644
index 0000000000..3d593c2a8f
--- /dev/null
+++ b/tests/regression/68-longjmp/21-multifun.c
@@ -0,0 +1,33 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+void foo() {
+ int local = 7;
+ longjmp(env_buffer, 2);
+}
+
+
+int fun() {
+ global = 42;
+ foo();
+}
+
+
+int main () {
+ int val;
+
+ __goblint_check(global == 0);
+ if(0 == setjmp( env_buffer )) {
+ fun();
+ } else {
+ __goblint_check(global == 42);
+ }
+
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/22-multifun-arg.c b/tests/regression/68-longjmp/22-multifun-arg.c
new file mode 100644
index 0000000000..a6b4b71c2b
--- /dev/null
+++ b/tests/regression/68-longjmp/22-multifun-arg.c
@@ -0,0 +1,37 @@
+// PARAM: --enable ana.int.interval --disable exp.volatiles_are_top --enable ana.int.enums --set solvers.td3.side_widen never
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+void foo() {
+ int local = 7;
+ longjmp(env_buffer, 2);
+}
+
+
+int fun(int* ptr) {
+ global = 42;
+ *ptr = 1;
+ foo();
+}
+
+
+int main () {
+ volatile int val = 0;
+
+ __goblint_check(global == 0);
+ int x = setjmp( env_buffer);
+ if(0 == x) {
+ fun(&val);
+ } else {
+ __goblint_check(x == 2);
+ __goblint_check(val == 1);
+ __goblint_check(global == 42);
+ }
+
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/23-arguments.c b/tests/regression/68-longjmp/23-arguments.c
new file mode 100644
index 0000000000..f135011c83
--- /dev/null
+++ b/tests/regression/68-longjmp/23-arguments.c
@@ -0,0 +1,35 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int fun() {
+ int top;
+
+ if(top == 1) {
+ longjmp(env_buffer, 2); //NOWARN
+ } else if (top == 2) {
+ longjmp(env_buffer, 0); //WARN
+ } else {
+ longjmp(env_buffer, top); //WARN
+ }
+}
+
+
+int main () {
+ int val;
+
+ __goblint_check(global == 0);
+ if(setjmp( env_buffer )) {
+ return 8;
+ }
+
+ fun();
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/24-too-late.c b/tests/regression/68-longjmp/24-too-late.c
new file mode 100644
index 0000000000..4c5062853f
--- /dev/null
+++ b/tests/regression/68-longjmp/24-too-late.c
@@ -0,0 +1,31 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int fun() {
+ int top;
+ longjmp(env_buffer, 2); //WARN
+}
+
+int bar() {
+ if(setjmp( env_buffer )) {
+ return 8;
+ }
+}
+
+
+int main () {
+ int val;
+
+ __goblint_check(global == 0);
+ bar();
+ fun();
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/25-rec.c b/tests/regression/68-longjmp/25-rec.c
new file mode 100644
index 0000000000..8c1f7b06a8
--- /dev/null
+++ b/tests/regression/68-longjmp/25-rec.c
@@ -0,0 +1,41 @@
+// PARAM: --enable ana.int.interval --enable exp.earlyglobs
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int fun() {
+ int top;
+ longjmp(env_buffer, 2); //WARN
+}
+
+int bar() {
+ int top,top2;
+
+ if(top) {
+ if(setjmp( env_buffer )) {
+ return 8;
+ }
+ }
+
+ if(top2) {
+ fun();
+ }
+}
+
+
+int main () {
+ int val;
+
+ __goblint_check(global == 0);
+ bar();
+
+ // In this second invocation of bar() the jumpbuffer could still contain the old value set during the first invocation, making the longjmp in fun()
+ // an illegal longjmp :/
+ bar();
+
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/26-non-term.c b/tests/regression/68-longjmp/26-non-term.c
new file mode 100644
index 0000000000..26d70471d9
--- /dev/null
+++ b/tests/regression/68-longjmp/26-non-term.c
@@ -0,0 +1,27 @@
+// SKIP PARAM: --enable ana.int.interval --enable exp.earlyglobs
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+// This will cause the analysis to not terminate as the set of
+// active setjumps will grow without bounds as the set of active
+// setjumps also forms part of the context.
+void bar() {
+ if(global == 0) {
+ if(setjmp( env_buffer )) {
+ return 8;
+ }
+ }
+
+ bar();
+}
+
+
+int main () {
+ bar();
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/27-other.c b/tests/regression/68-longjmp/27-other.c
new file mode 100644
index 0000000000..a19cc7c9b2
--- /dev/null
+++ b/tests/regression/68-longjmp/27-other.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.int.interval --enable exp.earlyglobs
+#include
+#include
+#include
+#include
+
+int main(void)
+{
+ jmp_buf buf;
+ int top;
+
+ if(top) {
+ if(setjmp(buf)) {
+ __goblint_check(1);
+ return 8;
+ }
+ }
+
+ longjmp(buf, 1); //WARN
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/28-svcomp.c b/tests/regression/68-longjmp/28-svcomp.c
new file mode 100644
index 0000000000..16856fb322
--- /dev/null
+++ b/tests/regression/68-longjmp/28-svcomp.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.int.interval --enable exp.earlyglobs --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"
+#include
+#include
+#include
+#include
+
+int main(void)
+{
+ jmp_buf buf;
+ int top;
+
+ if(top) {
+ if(setjmp(buf)) {
+ __goblint_check(1);
+ return 8;
+ }
+ }
+
+ longjmp(buf, 1); //WARN
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/29-rec2.c b/tests/regression/68-longjmp/29-rec2.c
new file mode 100644
index 0000000000..1bc9a5a012
--- /dev/null
+++ b/tests/regression/68-longjmp/29-rec2.c
@@ -0,0 +1,39 @@
+//PARAM: --enable ana.int.interval --enable exp.earlyglobs
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+
+void handler(int v) {
+ if(setjmp( env_buffer )) {
+ return 8;
+ }
+
+
+ if(v == 0) {
+ handler(1);
+ } else {
+ fun();
+ }
+
+ // If v == 0 then env_buffer was set in the recursive call to handler
+ // meaning that jumping here again is not valid.
+ fun();
+}
+
+
+int fun() {
+ int top;
+ longjmp(env_buffer, 2); //WARN
+}
+
+int main () {
+ int val;
+
+ handler(global);
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/30-nonuniquetid.c b/tests/regression/68-longjmp/30-nonuniquetid.c
new file mode 100644
index 0000000000..4e586130ff
--- /dev/null
+++ b/tests/regression/68-longjmp/30-nonuniquetid.c
@@ -0,0 +1,42 @@
+#include
+#include
+#include
+
+jmp_buf buf;
+jmp_buf buf1;
+pthread_mutex_t m;
+
+void *t_benign(void *arg) {
+ if(setjmp(buf1)) {
+ return NULL;
+ }
+
+ longjmp(buf1, 1); //NOWARN
+}
+
+void *t_fun(void *arg) {
+ pthread_mutex_lock(&m);
+ if(setjmp(buf)) {
+ return NULL;
+ }
+ pthread_mutex_unlock(&m);
+
+ pthread_mutex_lock(&m);
+ longjmp(buf, 1); //WARN
+ pthread_mutex_unlock(&m);
+}
+
+int main(void) {
+ int t;
+
+ pthread_t id;
+ pthread_create(&id, NULL, t_benign, NULL);
+
+ pthread_t id2[10];
+ for(int i =0; i < 10;i++) {
+ // As we have both a unique & a non-unique thread here, we automatically warn as appropriate
+ pthread_create(&id2[i], NULL, t_fun, NULL);
+ }
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/31-mixedjmpbufs.c b/tests/regression/68-longjmp/31-mixedjmpbufs.c
new file mode 100644
index 0000000000..470526fe19
--- /dev/null
+++ b/tests/regression/68-longjmp/31-mixedjmpbufs.c
@@ -0,0 +1,47 @@
+#include
+#include
+#include
+#include
+
+jmp_buf error0;
+jmp_buf error1;
+
+
+int blorg(int x) {
+ if(x > 8) {
+ longjmp(error1, 1); // WARN (modified since setjmp)
+ }
+
+ return x;
+}
+
+int blub(int x,int y) {
+ if(x == 0) {
+ longjmp(error0, 1); // WARN (modified since setjmp)
+ }
+
+ return blorg(x-27+3);
+}
+
+
+
+int main(void) {
+
+ if(setjmp(error0)) {
+ printf("error0 occured");
+ return -1;
+ }
+
+ if(setjmp(error1)) {
+ printf("error1 occured");
+ return -2;
+ }
+
+ int x, y;
+ scanf("%d", &x);
+ scanf("%d", &y);
+ int x = blub(x, y); // NOWARN
+ printf("%d", x);
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/32-libpng.c b/tests/regression/68-longjmp/32-libpng.c
new file mode 100644
index 0000000000..e2b8e6019c
--- /dev/null
+++ b/tests/regression/68-longjmp/32-libpng.c
@@ -0,0 +1,76 @@
+#include
+#include
+#include
+
+typedef void ( *png_longjmp_ptr) (jmp_buf, int);
+struct png_struct_def
+{
+ jmp_buf jmp_buf_local;
+ png_longjmp_ptr longjmp_fn;
+ jmp_buf *jmp_buf_ptr;
+ size_t jmp_buf_size;
+};
+
+typedef struct png_struct_def png_struct;
+typedef png_struct * __restrict png_structrp;
+
+jmp_buf* png_set_longjmp_fn(png_structrp png_ptr, png_longjmp_ptr longjmp_fn, size_t jmp_buf_size)
+{
+
+ if (png_ptr ==((void *)0) )
+ return ((void *)0);
+
+ if (png_ptr->jmp_buf_ptr == ((void *)0))
+ {
+ png_ptr->jmp_buf_size = 0;
+
+ if (jmp_buf_size <= (sizeof png_ptr->jmp_buf_local))
+ png_ptr->jmp_buf_ptr = &png_ptr->jmp_buf_local;
+
+ else
+ {
+ png_ptr->jmp_buf_ptr = malloc (jmp_buf_size);
+
+ if (png_ptr->jmp_buf_ptr ==((void *)0))
+ return ((void *)0);
+
+ png_ptr->jmp_buf_size = jmp_buf_size;
+ }
+ }
+
+ else
+ {
+ size_t size = png_ptr->jmp_buf_size;
+
+ if (size == 0)
+ {
+ size = (sizeof png_ptr->jmp_buf_local);
+ if (png_ptr->jmp_buf_ptr != &png_ptr->jmp_buf_local)
+ {
+ }
+ }
+
+ if (size != jmp_buf_size)
+ {
+ return ((void *)0);
+ }
+ }
+
+ png_ptr->longjmp_fn = longjmp_fn;
+ return png_ptr->jmp_buf_ptr;
+}
+
+
+int main(void) {
+ png_struct *read_ptr = malloc(sizeof(png_struct));
+ int local = 5;
+
+ if (setjmp ((*png_set_longjmp_fn((read_ptr), longjmp, (sizeof (jmp_buf)))))) {
+ int z = local; //WARN
+ return 48;
+
+ } else {
+ local = 8;
+ read_ptr->longjmp_fn(*read_ptr->jmp_buf_ptr, 1);
+ }
+}
diff --git a/tests/regression/68-longjmp/33-munge.c b/tests/regression/68-longjmp/33-munge.c
new file mode 100644
index 0000000000..65972b4704
--- /dev/null
+++ b/tests/regression/68-longjmp/33-munge.c
@@ -0,0 +1,55 @@
+// PARAMS: --disable exp.volatiles_are_top
+#include
+#include
+#include
+
+jmp_buf buf;
+jmp_buf buf1;
+pthread_mutex_t m;
+int g;
+
+void blub(int *x) {
+ *x = 17;
+}
+
+void blarg() {
+ int x = 28;
+ blub(&x);
+}
+
+void *t_benign(void *arg) {
+ volatile int vol = 2;
+ int t = 42, top;
+
+ if(setjmp(buf1)) {
+ t = t+1; //WARN
+ return NULL;
+ }
+
+ t = 19;
+
+ if(setjmp(buf)) {
+ t = t+1; //NOWARN
+ return NULL;
+ }
+
+ blarg();
+ vol++;
+ g = 17;
+
+ if(top) {
+ longjmp(buf1, 1); //WARN
+ } else{
+ longjmp(buf, 1); //NOWARN
+ }
+}
+
+
+int main(void) {
+ int t;
+
+ pthread_t id;
+ pthread_create(&id, NULL, t_benign, NULL);
+
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/34-wrapper.c b/tests/regression/68-longjmp/34-wrapper.c
new file mode 100644
index 0000000000..bf07e1333e
--- /dev/null
+++ b/tests/regression/68-longjmp/34-wrapper.c
@@ -0,0 +1,84 @@
+//PARAM: --set ana.malloc.wrappers[+] my_dirty_little_malloc
+#include
+#include
+#include
+
+typedef void ( *png_longjmp_ptr) (jmp_buf, int);
+struct png_struct_def
+{
+ jmp_buf jmp_buf_local;
+ png_longjmp_ptr longjmp_fn;
+ jmp_buf *jmp_buf_ptr;
+ size_t jmp_buf_size;
+};
+
+typedef struct png_struct_def png_struct;
+typedef png_struct * __restrict png_structrp;
+
+void* my_dirty_little_malloc(size_t size) {
+ return malloc(size);
+}
+
+
+jmp_buf* png_set_longjmp_fn(png_structrp png_ptr, png_longjmp_ptr longjmp_fn, size_t jmp_buf_size)
+{
+
+ if (png_ptr ==((void *)0) )
+ return ((void *)0);
+
+ if (png_ptr->jmp_buf_ptr == ((void *)0))
+ {
+ png_ptr->jmp_buf_size = 0;
+
+ if (jmp_buf_size <= (sizeof png_ptr->jmp_buf_local))
+ png_ptr->jmp_buf_ptr = &png_ptr->jmp_buf_local;
+
+ else
+ {
+ png_ptr->jmp_buf_ptr = my_dirty_little_malloc (jmp_buf_size);
+
+ if (png_ptr->jmp_buf_ptr ==((void *)0))
+ return ((void *)0);
+
+ png_ptr->jmp_buf_size = jmp_buf_size;
+ }
+ }
+
+ else
+ {
+ size_t size = png_ptr->jmp_buf_size;
+
+ if (size == 0)
+ {
+ size = (sizeof png_ptr->jmp_buf_local);
+ if (png_ptr->jmp_buf_ptr != &png_ptr->jmp_buf_local)
+ {
+ }
+ }
+
+ if (size != jmp_buf_size)
+ {
+ return ((void *)0);
+ }
+ }
+
+ png_ptr->longjmp_fn = longjmp_fn;
+ return png_ptr->jmp_buf_ptr;
+}
+
+
+int main(void) {
+ png_struct *read_ptr = my_dirty_little_malloc(sizeof(png_struct));
+ int *soup = my_dirty_little_malloc(sizeof(int));
+ *soup = 8;
+ int local = 5;
+
+ if (setjmp ((*png_set_longjmp_fn((read_ptr), longjmp, (sizeof (jmp_buf)))))) {
+ int z = local; //WARN
+ return 48;
+
+ } else {
+ local = 8;
+ read_ptr->longjmp_fn(*read_ptr->jmp_buf_ptr, 1);
+ }
+}
diff --git a/tests/regression/68-longjmp/35-null.c b/tests/regression/68-longjmp/35-null.c
new file mode 100644
index 0000000000..3e4f50d4bd
--- /dev/null
+++ b/tests/regression/68-longjmp/35-null.c
@@ -0,0 +1,93 @@
+//PARAM: --set ana.malloc.wrappers[+] my_dirty_little_malloc --disable sem.unknown_function.spawn
+#include
+#include
+#include
+
+typedef void ( *png_longjmp_ptr) (jmp_buf, int);
+struct png_struct_def
+{
+ jmp_buf jmp_buf_local;
+ png_longjmp_ptr longjmp_fn;
+ jmp_buf *jmp_buf_ptr;
+ size_t jmp_buf_size;
+};
+
+typedef struct png_struct_def png_struct;
+typedef png_struct * __restrict png_structrp;
+
+void* my_dirty_little_malloc(size_t size) {
+ return malloc(size);
+}
+
+extern void* munge(png_structrp png_ptr);
+
+jmp_buf* png_set_longjmp_fn(png_structrp png_ptr, png_longjmp_ptr longjmp_fn, size_t jmp_buf_size)
+{
+
+ if (png_ptr ==((void *)0) )
+ return ((void *)0);
+
+ if (png_ptr->jmp_buf_ptr == ((void *)0))
+ {
+ png_ptr->jmp_buf_size = 0;
+
+ if (jmp_buf_size <= (sizeof png_ptr->jmp_buf_local))
+ png_ptr->jmp_buf_ptr = &png_ptr->jmp_buf_local;
+
+ else
+ {
+ png_ptr->jmp_buf_ptr = my_dirty_little_malloc (jmp_buf_size);
+
+ if (png_ptr->jmp_buf_ptr ==((void *)0))
+ return ((void *)0);
+
+ png_ptr->jmp_buf_size = jmp_buf_size;
+ }
+ }
+
+ else
+ {
+ size_t size = png_ptr->jmp_buf_size;
+
+ if (size == 0)
+ {
+ size = (sizeof png_ptr->jmp_buf_local);
+ if (png_ptr->jmp_buf_ptr != &png_ptr->jmp_buf_local)
+ {
+ }
+ }
+
+ if (size != jmp_buf_size)
+ {
+ return ((void *)0);
+ }
+ }
+
+ png_ptr->longjmp_fn = longjmp_fn;
+ return png_ptr->jmp_buf_ptr;
+}
+
+
+int main(void) {
+ png_struct *read_ptr = my_dirty_little_malloc(sizeof(png_struct));
+ int *soup = my_dirty_little_malloc(sizeof(int));
+ *soup = 8;
+ int local = 5;
+
+ struct __jmp_buf_tag *buf[1] = malloc(sizeof(jmp_buf));
+
+ if (setjmp ((*png_set_longjmp_fn((read_ptr), longjmp, (sizeof (jmp_buf)))))) {
+ int z = local; //WARN
+ return 48;
+
+ } else {
+ local = 8;
+
+ int top;
+ if(top) {
+ read_ptr->jmp_buf_ptr = ((void *)0);
+ }
+ munge(read_ptr);
+ read_ptr->longjmp_fn(*read_ptr->jmp_buf_ptr, 1);
+ }
+}
diff --git a/tests/regression/68-longjmp/36-poison.c b/tests/regression/68-longjmp/36-poison.c
new file mode 100644
index 0000000000..0a2959bb92
--- /dev/null
+++ b/tests/regression/68-longjmp/36-poison.c
@@ -0,0 +1,51 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int myRandom() {
+ // Chosen by fair dice roll.
+ return 42;
+}
+
+int funjmp() {
+ longjmp(env_buffer, 2);
+}
+
+int fun(int param) {
+ param = param +1; //NOWARN
+ if(param == 2) {
+ funjmp();
+ }
+}
+
+int main () {
+ int val;
+ int x;
+ int top;
+
+ __goblint_check(global == 0);
+ if(setjmp( env_buffer )) {
+ x = val; //WARN
+
+ if(top) {
+ val = 8;
+ } else {
+ val = myRandom();
+ }
+
+ x = val; //NOWARN
+ fun(5);
+ return;
+ };
+
+ val = 8;
+ fun(1);
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/37-more.c b/tests/regression/68-longjmp/37-more.c
new file mode 100644
index 0000000000..d82a8908af
--- /dev/null
+++ b/tests/regression/68-longjmp/37-more.c
@@ -0,0 +1,86 @@
+//PARAM:
+#include
+#include
+#include
+
+typedef void ( *png_longjmp_ptr) (jmp_buf, int);
+struct png_struct_def
+{
+ jmp_buf jmp_buf_local;
+ png_longjmp_ptr longjmp_fn;
+ jmp_buf *jmp_buf_ptr;
+ size_t jmp_buf_size;
+};
+
+typedef struct png_struct_def png_struct;
+typedef png_struct * __restrict png_structrp;
+
+jmp_buf* png_set_longjmp_fn(png_structrp png_ptr, png_longjmp_ptr longjmp_fn, size_t jmp_buf_size)
+{
+
+ if (png_ptr ==((void *)0))
+ return ((void *)0);
+
+ if (png_ptr->jmp_buf_ptr == ((void *)0))
+ {
+ png_ptr->jmp_buf_size = 0;
+
+ if (jmp_buf_size <= (sizeof png_ptr->jmp_buf_local))
+ png_ptr->jmp_buf_ptr = &png_ptr->jmp_buf_local;
+
+ else
+ {
+ png_ptr->jmp_buf_ptr = malloc(jmp_buf_size);
+
+ if (png_ptr->jmp_buf_ptr ==((void *)0))
+ return ((void *)0);
+
+ png_ptr->jmp_buf_size = jmp_buf_size;
+ }
+ }
+
+ else
+ {
+ size_t size = png_ptr->jmp_buf_size;
+
+ if (size == 0)
+ {
+ size = (sizeof png_ptr->jmp_buf_local);
+ if (png_ptr->jmp_buf_ptr != &png_ptr->jmp_buf_local)
+ {
+ }
+ }
+
+ if (size != jmp_buf_size)
+ {
+ return ((void *)0);
+ }
+ }
+
+ png_ptr->longjmp_fn = longjmp_fn;
+ return png_ptr->jmp_buf_ptr;
+}
+
+
+int main(void) {
+ png_struct *read_ptr;
+
+ // They really do this crap!
+ png_struct create_struct;
+ memset(&create_struct, 0, (sizeof create_struct));
+
+ read_ptr = malloc(sizeof(png_struct));
+ *read_ptr = create_struct;
+
+ int local = 5;
+
+ if (setjmp ((*png_set_longjmp_fn((read_ptr), longjmp, (sizeof (jmp_buf)))))) {
+ int z = local; //WARN
+ return 48;
+
+ } else {
+ local = 8;
+
+ read_ptr->longjmp_fn(*read_ptr->jmp_buf_ptr, 1);
+ }
+}
diff --git a/tests/regression/68-longjmp/38-more-trimmed.c b/tests/regression/68-longjmp/38-more-trimmed.c
new file mode 100644
index 0000000000..54805c9edf
--- /dev/null
+++ b/tests/regression/68-longjmp/38-more-trimmed.c
@@ -0,0 +1,48 @@
+// PARAM: --set ana.malloc.unique_address_count 1
+#include
+#include
+#include
+
+typedef void ( *png_longjmp_ptr) (jmp_buf, int);
+struct png_struct_def
+{
+ jmp_buf jmp_buf_local;
+ png_longjmp_ptr longjmp_fn;
+ jmp_buf *jmp_buf_ptr;
+ size_t jmp_buf_size;
+};
+
+typedef struct png_struct_def png_struct;
+typedef png_struct * __restrict png_structrp;
+
+jmp_buf* png_set_longjmp_fn(png_structrp png_ptr, png_longjmp_ptr longjmp_fn, size_t jmp_buf_size)
+{
+ png_ptr->jmp_buf_size = 0;
+ png_ptr->jmp_buf_ptr = &png_ptr->jmp_buf_local;
+ png_ptr->longjmp_fn = longjmp_fn;
+ return png_ptr->jmp_buf_ptr;
+}
+
+
+int main(void) {
+ png_struct *read_ptr;
+
+ // They really do this crap!
+ png_struct create_struct;
+ memset(&create_struct, 0, (sizeof create_struct));
+
+ read_ptr = malloc(sizeof(png_struct));
+ *read_ptr = create_struct;
+
+ int local = 5;
+
+ if (setjmp ((*png_set_longjmp_fn((read_ptr), longjmp, (sizeof (jmp_buf)))))) {
+ int z = local; //WARN
+ return 48;
+
+ } else {
+ local = 8;
+
+ read_ptr->longjmp_fn(*read_ptr->jmp_buf_ptr, 1);
+ }
+}
diff --git a/tests/regression/68-longjmp/39-poison-return.c b/tests/regression/68-longjmp/39-poison-return.c
new file mode 100644
index 0000000000..09e8883664
--- /dev/null
+++ b/tests/regression/68-longjmp/39-poison-return.c
@@ -0,0 +1,32 @@
+// PARAM:
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+
+int wrap () {
+ int val;
+ int x;
+ int top;
+
+ val = val + 2; //NOWARN
+
+ if(setjmp( env_buffer )) {
+ x = val; //WARN
+ return 3;
+ };
+
+ val = 8;
+ longjmp(env_buffer, 2);
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
+
+int main() {
+ wrap();
+ int y = 8;
+ wrap();
+}
diff --git a/tests/regression/68-longjmp/40-complicated-poison.c b/tests/regression/68-longjmp/40-complicated-poison.c
new file mode 100644
index 0000000000..2b3eb89d96
--- /dev/null
+++ b/tests/regression/68-longjmp/40-complicated-poison.c
@@ -0,0 +1,65 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int myRandom() {
+ // Chosen by fair dice roll.
+ return 42;
+}
+
+int funjmp() {
+ longjmp(env_buffer, 2);
+}
+
+int fun(int param) {
+ param = param +1; //NOWARN
+ if(param == 2) {
+ funjmp();
+ }
+}
+
+int eight() {
+ return 8;
+}
+
+int main () {
+ int val;
+ int x;
+ int top;
+ int* ptr = &val;
+ int* ptr2 = &val;
+ int** ptrptr = &ptr;
+ int arr[10] = {0,0,0,0,0,0,0,0,0,0};
+ int* ptr3;
+
+ __goblint_check(global == 0);
+ if(setjmp( env_buffer )) {
+ x = val; //WARN
+ x = *ptr; //WARN
+ ptr3 = ptr2; //WARN
+ x = *ptr2; //WARN
+ x = **ptrptr; //WARN
+ x = arr[**ptrptr]; //WARN
+
+ *ptr = 5; //NOWARN
+ x = *ptr; //NOWARN
+ *ptr2 = 9; //WARN (ptr2 still has indeterminate value)
+ *ptr2 = eight(); //WARN (ptr2 still has indeterminate value)
+
+ x = val; //NOWARN
+ fun(5);
+ return 3;
+ };
+
+ val = 8;
+ ptr2 = &x;
+ fun(1);
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/41-poison-rec.c b/tests/regression/68-longjmp/41-poison-rec.c
new file mode 100644
index 0000000000..c5ff941298
--- /dev/null
+++ b/tests/regression/68-longjmp/41-poison-rec.c
@@ -0,0 +1,33 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int fun(int param) {
+ char keyword[81] = "example";
+
+ if(param != 2) {
+ char c = keyword[0]; //NOWARN
+ return 1;
+ }
+
+ if(setjmp( env_buffer )) {
+ fun(4);
+
+ char c = keyword[0]; //WARN
+ return 3;
+ };
+
+ keyword[0] = 'a';
+
+ longjmp(env_buffer, 2);
+}
+
+int main () {
+ fun(2);
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/42-poison-reduced.c b/tests/regression/68-longjmp/42-poison-reduced.c
new file mode 100644
index 0000000000..a3ef050b35
--- /dev/null
+++ b/tests/regression/68-longjmp/42-poison-reduced.c
@@ -0,0 +1,37 @@
+// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --enable dbg.verbose --disable exp.volatiles_are_top --enable ana.int.interval
+#include
+jmp_buf env_buffer;
+struct c {
+ char *g;
+};
+
+int u(struct c * t) {
+ if (*t->g) {
+ return 2;
+ } else {
+ return 3;
+ }
+}
+
+void set_g_to_keyword(struct c* t) {
+ char keyword[20];
+ keyword[0] = 'a';
+ t->g = keyword;
+}
+
+main() {
+ struct c* ab = malloc(sizeof(struct c));
+ int x;
+
+ if(setjmp(env_buffer)) {
+ __goblint_check(x == 2);
+ set_g_to_keyword(ab);
+ }
+ else {
+ set_g_to_keyword(ab);
+ x = 1;
+ u(ab);
+ x = 2;
+ longjmp(env_buffer, 1);
+ }
+}
diff --git a/tests/regression/68-longjmp/43-poison-addr.c b/tests/regression/68-longjmp/43-poison-addr.c
new file mode 100644
index 0000000000..6d1c0b455d
--- /dev/null
+++ b/tests/regression/68-longjmp/43-poison-addr.c
@@ -0,0 +1,37 @@
+// PARAM:
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+
+void makeFive(int* ptr) {
+ *ptr = 5;
+}
+
+int wrap () {
+ int val;
+ int x;
+ int top;
+
+ val = val + 2; //NOWARN
+
+ if(setjmp( env_buffer )) {
+ makeFive(&val); //NOWARN
+ x = val; //NOWARN
+ return 3;
+ };
+
+ val = 8;
+ longjmp(env_buffer, 2);
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
+
+int main() {
+ wrap();
+ int y = 8;
+ wrap();
+}
diff --git a/tests/regression/68-longjmp/44-simple-else-path.c b/tests/regression/68-longjmp/44-simple-else-path.c
new file mode 100644
index 0000000000..9215eb79d8
--- /dev/null
+++ b/tests/regression/68-longjmp/44-simple-else-path.c
@@ -0,0 +1,38 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set ana.activated[+] expsplit
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int fun() {
+ global = 2;
+ longjmp(env_buffer, 2);
+}
+
+
+int main () {
+ int val;
+ jmp_buf env_buffer2;
+
+ __goblint_check(global == 0);
+
+ /* save calling environment for longjmp */
+ val = setjmp( env_buffer );
+
+
+ if( val != 0 ) {
+ printf("Returned from a longjmp() with value = %i\n", val);
+ __goblint_check(val == 2);
+ __goblint_check(global == 2);
+ exit(0);
+ }
+
+ __goblint_check(global == 0);
+ fun();
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/45-variably-modified.c b/tests/regression/68-longjmp/45-variably-modified.c
new file mode 100644
index 0000000000..5bb2ebea85
--- /dev/null
+++ b/tests/regression/68-longjmp/45-variably-modified.c
@@ -0,0 +1,54 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set ana.activated[+] expsplit --disable warn.deadcode
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int fun() {
+ if(setjmp(env_buffer)) { //NOWARN
+ return 0;
+ }
+
+
+ global = 2;
+ longjmp(env_buffer, 2);
+}
+
+
+int main () {
+ int val;
+ jmp_buf env_buffer2;
+
+ __goblint_check(global == 0);
+
+ if(setjmp(env_buffer)) { //NOWARN
+ return 0;
+ }
+
+ int n;
+
+ {
+ // Array of variably modified type
+ int a[n];
+
+ if(setjmp(env_buffer)) { // WARN
+ return 0;
+ }
+ }
+
+ {
+ // Array of variably modified type
+ int b[2][n];
+
+ if(setjmp(env_buffer)) { // WARN
+ return 0;
+ }
+ }
+
+ fun();
+
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/46-copied.c b/tests/regression/68-longjmp/46-copied.c
new file mode 100644
index 0000000000..d7ec9de0da
--- /dev/null
+++ b/tests/regression/68-longjmp/46-copied.c
@@ -0,0 +1,28 @@
+// PARAM: --enable ana.int.interval --enable ana.int.enums --set ana.activated[+] expsplit --disable warn.deadcode
+#include
+#include
+#include
+// #include
+
+struct buf_struct {
+ jmp_buf buf;
+};
+
+struct buf_struct env_buffer;
+struct buf_struct buffer2;
+int global = 0;
+
+int main () {
+ int val;
+ __goblint_check(global == 0);
+
+ if(setjmp(env_buffer.buf)) { //NOWARN
+ return 0;
+ }
+
+ buffer2 = env_buffer;
+
+ longjmp(buffer2.buf,42); //WARN
+
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/47-more-reduced.c b/tests/regression/68-longjmp/47-more-reduced.c
new file mode 100644
index 0000000000..ff85a229e5
--- /dev/null
+++ b/tests/regression/68-longjmp/47-more-reduced.c
@@ -0,0 +1,38 @@
+// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --enable dbg.verbose --disable exp.volatiles_are_top --enable ana.int.interval
+#include
+jmp_buf env_buffer;
+
+struct c {
+ char *g;
+} s;
+
+int g;
+
+set_key(struct c* t) {
+ char keyword[20];
+ keyword[0] = 'a';
+ t->g = keyword;
+
+ if (*t->g) { g=1; }
+}
+
+main() {
+ struct c * t = &s;
+
+ switch(setjmp(env_buffer)) {
+ case 0: break;
+ case 1:
+ if (*t->g) { g=1; }
+ // This refinement somehow adds bottom for keyword as an explicit binding (???)
+ set_key(t);
+ longjmp(env_buffer, 2); //NOWARN
+ break;
+ case 2:
+ return;
+ }
+
+ set_key(t);
+ g = 4;
+
+ longjmp(env_buffer, 1);
+}
diff --git a/tests/regression/68-longjmp/48-bot-buff.c b/tests/regression/68-longjmp/48-bot-buff.c
new file mode 100644
index 0000000000..eaf92f89af
--- /dev/null
+++ b/tests/regression/68-longjmp/48-bot-buff.c
@@ -0,0 +1,6 @@
+#include
+jmp_buf env_buffer;
+
+int main() {
+ longjmp(env_buffer, 1); //WARN
+}
diff --git a/tests/regression/68-longjmp/49-arguments-inline.c b/tests/regression/68-longjmp/49-arguments-inline.c
new file mode 100644
index 0000000000..7c8c00b1d0
--- /dev/null
+++ b/tests/regression/68-longjmp/49-arguments-inline.c
@@ -0,0 +1,15 @@
+#include
+#include
+
+jmp_buf env_buffer;
+
+int main () {
+ if (setjmp(env_buffer)) {
+ __goblint_check(1); // reachable
+ return 8;
+ }
+
+ longjmp(env_buffer, 0); // WARN
+ __goblint_check(0); // NOWARN
+ return 0;
+}
diff --git a/tests/regression/68-longjmp/50-arguments-non-top.c b/tests/regression/68-longjmp/50-arguments-non-top.c
new file mode 100644
index 0000000000..fd5f30a166
--- /dev/null
+++ b/tests/regression/68-longjmp/50-arguments-non-top.c
@@ -0,0 +1,31 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+
+int fun() {
+ int r;
+ __goblint_assume(0 <= r);
+ __goblint_assume(r <= 10);
+ longjmp(env_buffer, r); //WARN
+}
+
+
+int main () {
+ int val;
+ if (val = setjmp( env_buffer )) {
+ __goblint_check(val == 1); // UNKNOWN!
+ __goblint_check(val != 1); // UNKNOWN!
+ __goblint_check(1 <= val); // TODO (better interval exclude)
+ __goblint_check(val <= 10);
+ return 8;
+ }
+
+ fun();
+
+ __goblint_check(0); // NOWARN
+ return(0);
+}
diff --git a/tests/regression/68-longjmp/51-worries.c b/tests/regression/68-longjmp/51-worries.c
new file mode 100644
index 0000000000..d25df25712
--- /dev/null
+++ b/tests/regression/68-longjmp/51-worries.c
@@ -0,0 +1,26 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int bar() {
+ longjmp(env_buffer, 2);
+ return 8;
+}
+
+void foo() {
+ global = bar();
+}
+
+int main() {
+ if(setjmp( env_buffer )) {
+ assert(global == 0);
+ return 0;
+ }
+
+ foo();
+}
diff --git a/tests/regression/68-longjmp/README.md b/tests/regression/68-longjmp/README.md
new file mode 100644
index 0000000000..4e3f00d05b
--- /dev/null
+++ b/tests/regression/68-longjmp/README.md
@@ -0,0 +1,5 @@
+# Tests for the support of setjmp/longjmp by Goblint
+
+Some of these tests are technically illegal according to the C standard, as `setjmp` may only appear inside a condition.
+We still have it pulled out here sometimes to allow conveniently inspecting analysis results without having to deal with
+CIL inserted temporaries. GCC also support this without any issues.