diff --git a/goblint.opam.locked b/goblint.opam.locked
index b0a1c9ef20..d66084af78 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -131,6 +131,10 @@ post-messages: [
 ]
 # TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
 pin-depends: [
+  [
+    "goblint-cil.2.0.3"
+    "git+https://github.com/N0W0RK/goblint-cil.git#second_try" 
+  ]
   [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index efad8b4c2e..4e46f96b2a 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -25,8 +25,10 @@ struct
 
   let collect_local = ref false
   let emit_single_threaded = ref false
+  let ignore_asm = ref true
 
   let init _ =
+    ignore_asm := get_bool "asm_is_nop";
     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 (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
@@ -73,6 +75,17 @@ struct
       ctx.local
     end
 
+  let asm ctx outs ins =
+    if not !ignore_asm then begin
+      let handle_in exp = access_one_top ctx Read false exp in
+      List.iter handle_in ins;
+      (* deref needs to be set to true because we have to use AddrOf *)
+      let handle_out lval = access_one_top ~deref:true ctx Write false (AddrOf lval) in
+      List.iter handle_out outs;
+    end;
+    ctx.local
+
+
   let branch ctx exp tv : D.t =
     access_one_top ctx Read false exp;
     ctx.local
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 42e43b623a..ddaa88e04f 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -82,6 +82,7 @@ struct
   let name () = "base"
   let startstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
   let exitstate  v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
+  let ignore_asm = ref true
 
   (**************************************************************************
    * Helpers
@@ -160,6 +161,7 @@ struct
     end;
     return_varstore := Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType;
     longjmp_return := Cilfacade.create_var @@ makeVarinfo false "LONGJMP_RETURN" intType;
+    ignore_asm := get_bool "asm_is_nop";
     Priv.init ()
 
   let finalize () =
@@ -1240,9 +1242,11 @@ struct
           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 ~ctx ~top:(VD.bot ()) ctx.local jmp_buf None with
-            | JmpBuf (x, copied) ->
+            | JmpBuf (x, copied, invalid) ->
               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;
+              if invalid then
+                M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a was modified by inline assembly. This is may lead to Undefined Behavior." d_exp e;
               x
             | Top
             | Bot ->
@@ -2582,7 +2586,7 @@ struct
     | Setjmp { env }, _ ->
       let st' = match eval_rv ~ctx st env with
         | Address jmp_buf ->
-          let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false) in
+          let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false, false) in
           let r = set ~ctx 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
@@ -2898,6 +2902,11 @@ struct
     in
     D.join ctx.local e_d'
 
+  let asm ctx outs ins = 
+    if not !ignore_asm then
+      ctx.emit (Events.Invalidate {lvals=outs});
+    ctx.local
+
   let event ctx e octx =
     let ask = Analyses.ask_of_ctx ctx in
     let st: store = ctx.local in
@@ -2929,6 +2938,9 @@ struct
           {st' with cpa = CPA.remove !longjmp_return st'.cpa}
         | None -> ctx.local
       end
+    | Events.Invalidate {lvals} ->
+      let exps = List.map Cil.mkAddrOrStartOf lvals in
+      invalidate ~ctx st exps
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 3b23dc03fc..001aeac8d0 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -101,6 +101,15 @@ struct
       of_expr true e >? of_lval >? of_clval |? Queries.Result.top q
     | _ -> Queries.Result.top q
 
+  let event ctx event octx = 
+    match event with
+    | Events.Invalidate {lvals} -> 
+      let mpts = List.map (fun lval -> mayPointTo ctx (AddrOf lval)) lvals in
+      let remove_mpt d mpt =
+        List.fold_left (fun d (v,o as k) -> D.remove k d |> D.remove_var v) d mpt in
+      List.fold_left remove_mpt ctx.local mpts
+    | _ -> ctx.local
+  
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     (* remove all keys lval may point to, and all exprs that contain the variables (TODO precision) *)
diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index c23d6f4294..38aafef7a3 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -40,6 +40,7 @@ struct
     let remove ctx l =
       let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
+      
   end
 
   include LocksetAnalysis.MakeMay (Arg)
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index fef3d9ff9f..5758068eba 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -96,6 +96,15 @@ struct
       D.add exp value ctx.local
     | Longjmped _ ->
       emit_splits_ctx ctx
+    | Invalidate {lvals} ->
+      let handle_lval local lval =
+        let exp = Lval lval in
+        if D.mem exp local then
+          D.remove exp local
+        else
+          local
+      in
+      List.fold handle_lval ctx.local lvals
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 6a816b9e6c..3582d147e1 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -1,6 +1,7 @@
 (** Basic lockset analyses. *)
 
 open Analyses
+open GoblintCil
 
 
 module type DS =
@@ -33,6 +34,20 @@ sig
   val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
 end
 
+let addr_set_of_lval (a: Queries.ask) lval =
+  let exp = Cil.mkAddrOrStartOf lval in
+  let addr_set = a.f (Queries.MayPointTo exp) in
+  addr_set
+
+let locks_of_lvals ctx lvals =
+  let ask = Analyses.ask_of_ctx ctx in
+  let collect_addr_sets locks lval = 
+    let addr_set = addr_set_of_lval ask lval in
+    ValueDomain.AD.union locks addr_set 
+  in
+  let addr_set = List.fold_left collect_addr_sets (ValueDomain.AD.empty ()) lvals in
+  ValueDomain.AD.elements addr_set
+  
 module MakeMay (Arg: MayArg) =
 struct
   include Make (Arg.D)
@@ -60,6 +75,7 @@ module type MustArg =
 sig
   include MayArg
   val remove_all: (D.t, _, D.t, _) ctx -> D.t
+  val is_held: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> bool
 end
 
 module MakeMust (Arg: MustArg) =
@@ -82,6 +98,13 @@ struct
       Arg.remove_all ctx (* remove all locks *)
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *)
+    | Events.Invalidate {lvals} ->
+      let locks = locks_of_lvals ctx lvals in
+      let is_held lock = Arg.is_held ctx lock in
+      let locks = List.filter is_held locks in
+      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
+      let ctx = List.fold_left remove_lock ctx locks in
+      ctx.local
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 50f6d5409b..f17ef5e7b4 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -428,7 +428,7 @@ struct
     if q then raise Deadcode else d
 
 
-  let asm (ctx:(D.t, G.t, C.t, V.t) ctx) =
+  let asm (ctx:(D.t, G.t, C.t, V.t) ctx) outs ins =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
@@ -436,7 +436,7 @@ struct
     let ctx'' = outer_ctx "asm" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "asm" ~splits ~post_all ctx'' n d in
-      n, repr @@ S.asm ctx'
+      n, repr @@ S.asm ctx' outs ins
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index d1314d5009..0bc0c0e4c3 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -29,6 +29,14 @@ struct
   let assign ctx lval rval =
     assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let handle_lval local lval = assign_lval ask lval local in
+      List.fold_left handle_lval ctx.local lvals
+    | _ -> ctx.local
+
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)
 
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index f993db0c6e..0946b9f544 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -6,6 +6,7 @@ module Offs = ValueDomain.Offs
 
 open GoblintCil
 open Analyses
+open GobConfig
 
 module Spec =
 struct
@@ -16,6 +17,21 @@ struct
   module C = ValueDomain.AddrSetDomain
   module P = IdentityP (D)
 
+  let name () = "malloc_null"
+
+  let return_addr_ = ref Addr.NullPtr
+  let return_addr () = !return_addr_
+
+  let startstate v = D.empty ()
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
+  let exitstate  v = D.empty ()
+  let ignore_asm = ref true
+
+  let init marshal =
+    return_addr_ :=  Addr.of_var (Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType);
+    ignore_asm := get_bool "asm_is_nop"
+
   (*
     Addr set functions:
   *)
@@ -153,6 +169,15 @@ struct
       D.add (Addr.of_mval mval) ctx.local
     | _ -> ctx.local
 
+  let asm ctx outs ins =
+    if not !ignore_asm then begin
+      let handle_in exp = warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local exp in
+      List.iter handle_in ins;
+      let handle_out lval = warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local (Lval lval) in
+      List.iter handle_out outs;
+    end;
+    ctx.local
+
   let branch ctx (exp:exp) (tv:bool) : D.t =
     warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local exp;
     ctx.local
@@ -160,9 +185,6 @@ struct
   let body ctx (f:fundec) : D.t =
     ctx.local
 
-  let return_addr_ = ref Addr.NullPtr
-  let return_addr () = !return_addr_
-
   let return ctx (exp:exp option) (f:fundec) : D.t =
     let remove_var x v = List.fold_right D.remove (to_addrs v) x in
     let nst = List.fold_left remove_var ctx.local (f.slocals @ f.sformals) in
@@ -212,15 +234,6 @@ struct
       end
     | _ -> ctx.local
 
-  let name () = "malloc_null"
-
-  let startstate v = D.empty ()
-  let threadenter ctx ~multiple lval f args = [D.empty ()]
-  let threadspawn ctx ~multiple lval f args fctx = ctx.local
-  let exitstate  v = D.empty ()
-
-  let init marshal =
-    return_addr_ :=  Addr.of_var (Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType)
 end
 
 let _ =
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 456d434be7..707887f30e 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -216,9 +216,8 @@ struct
         | ad when (not (Queries.AD.is_top ad)) && Queries.AD.cardinal ad = 1 ->
           (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
           begin match Queries.AD.choose ad with
-            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) ->
-              ToppedVarInfoSet.remove v ctx.local
-            | _ -> ctx.local
+            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> ToppedVarInfoSet.remove v state
+            | _ -> state
           end
         | _ -> ctx.local
       end
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index a13c8d6bfd..9d8b3cf739 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -154,10 +154,14 @@ struct
         (s', Multiplicity.increment (fst l) m)
       | _ -> (s', m)
 
+    let is_held ctx l =
+      let s, _ = ctx.local in
+      Lockset.mem (l, true) s || Lockset.mem(l, false) s
+
     let remove' ctx ~warn l =
       let s, m = ctx.local in
       let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
-      if warn &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
+      if warn && (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
       match Addr.to_mval l with
       | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
         let m',rmed = Multiplicity.decrement l m in
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index a6ffa54ed6..63d716b06e 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -75,6 +75,29 @@ struct
       | Some r when Lvals.is_empty r -> false
       | _ -> true
   end
+
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+        begin
+          match ctx.local with
+          | `Lifted reg ->
+            let old_regpart = ctx.global () in
+            let regpart, reg =
+              List.fold_left
+                (fun (regpart_acc, reg_acc) lval ->
+                  Reg.assign_bullet lval (regpart_acc, reg_acc)
+                )
+                (old_regpart, reg)
+                lvals
+            in
+            if not (RegPart.leq regpart old_regpart) then
+              ctx.sideg () regpart;
+            `Lifted reg
+          | _ -> ctx.local
+        end
+      | _ -> ctx.local
+    
   let access ctx (a: Queries.access) =
     match a with
     | Point ->
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index c237967a7a..e7214b2f32 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -103,6 +103,13 @@ struct
       (* TODO: why doesn't invalidate_exp involve any reachable for deep write? *)
       List.fold_left (fun st e -> invalidate_exp (Analyses.ask_of_ctx ctx) e st) st write_args
 
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let invalidate local lval = invalidate_lval ask lval local in
+      List.fold_left invalidate ctx.local lvals
+    | _ -> ctx.local
 
   module A =
   struct
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index 85dabd1c9d..606620e602 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -103,6 +103,18 @@ struct
 
 end
 
+let event ctx e octx =
+  match e with
+  | Events.Invalidate {lvals} ->
+    (* Handle the Invalidate event and update the tainted set *)
+    List.fold_left (fun acc lval ->
+      Spec.taint_lval ctx lval 
+    ) ctx.local lvals
+   
+  | _ -> ctx.local
+
+
+
 let _ =
   MCP.register_analysis (module Spec : MCPSpec)
 
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 5895f242c9..3939efa517 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -304,7 +304,7 @@ struct
 
     emit_unassume {ctx with local = st} (* doesn't query, so no need to redefine ask *)
 
-  let asm ctx =
+  let asm ctx outs ins =
     emit_unassume ctx
 
   let skip ctx =
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 8693599a4d..20043ad50d 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -7,6 +7,7 @@ module Offs = ValueDomain.Offs
 
 open GoblintCil
 open Analyses
+open GobConfig
 
 module Spec =
 struct
@@ -29,6 +30,11 @@ struct
   let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
+  let ignore_asm = ref true
+
+  let init _ =
+    ignore_asm := get_bool "asm_is_nop"
+
   let access_address (ask: Queries.ask) write lv =
     match ask.f (Queries.MayPointTo (AddrOf lv)) with
     | ad when not (Queries.AD.is_top ad) ->
@@ -223,6 +229,14 @@ struct
     ignore (is_expr_initd (Analyses.ask_of_ctx ctx) rval ctx.local);
     init_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
+  let asm ctx outs ins = 
+    if not !ignore_asm then begin
+      let handle_in exp = ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local) in
+      List.iter handle_in ins;
+      let handle_out local lval = init_lval (Analyses.ask_of_ctx ctx) lval local in
+      List.fold_left handle_out ctx.local outs
+    end else ctx.local
+
   let branch ctx (exp:exp) (tv:bool) : trans_out =
     ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local);
     ctx.local
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 69db6b4bfa..b29741bd21 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -4,6 +4,7 @@ open GoblintCil
 open Analyses
 open MessageCategory
 open AnalysisStateUtil
+open GobConfig
 
 module AllocaVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All alloca() Variables" end)
 module HeapVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
@@ -24,9 +25,12 @@ struct
   module G = ThreadIdToJoinedThreadsMap
   module V = VarinfoV
 
-  let context _ _ = ()
+  let ignore_asm = ref true
 
+  let init _ =
+    ignore_asm := get_bool "asm_is_nop"
 
+  let context _ _ = ()
   (* HELPER FUNCTIONS *)
 
   let get_current_threadid ctx =
@@ -175,6 +179,15 @@ struct
     warn_exp_might_contain_freed "branch" ctx exp;
     ctx.local
 
+  let asm ctx outs ins =
+    if not !ignore_asm then begin
+      let handle_out lval = warn_lval_might_contain_freed "asm" ctx lval in
+      List.iter handle_out outs;
+      let handle_in exp = warn_exp_might_contain_freed "asm" ctx exp in
+      List.iter handle_in ins;
+    end;
+    ctx.local
+
   let return ctx (exp:exp option) (f:fundec) : D.t =
     Option.iter (fun x -> warn_exp_might_contain_freed "return" ctx x) exp;
     ctx.local
@@ -239,7 +252,6 @@ struct
 
   let startstate v = D.bot ()
   let exitstate v = D.top ()
-
 end
 
 let _ =
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 30b36404af..01abc330ae 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -589,6 +589,10 @@ struct
           remove ask (Cil.var v) st
         in
         List.fold_left remove_var ctx.local (EscapeDomain.EscapedVars.elements vars)
+    | Events.Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let remove_lval ctx lval = remove ask lval ctx in
+      List.fold_left remove_lval ctx.local lvals
     | _ ->
       ctx.local
 end
diff --git a/src/cdomain/value/cdomains/jmpBufDomain.ml b/src/cdomain/value/cdomains/jmpBufDomain.ml
index 3c94fa8f47..f2ef201c34 100644
--- a/src/cdomain/value/cdomains/jmpBufDomain.ml
+++ b/src/cdomain/value/cdomains/jmpBufDomain.ml
@@ -37,13 +37,14 @@ struct
   let meet = inter
 end
 
-module JmpBufSetTaint =
+module JmpBufSetTaintInvalid =
 struct
   module Bufs = JmpBufSet
-  include Lattice.Prod(JmpBufSet)(BoolDomain.MayBool)
-  let buffers (a,_) = a
-  let copied (_,b) = b
-  let name () = "JumpbufferCopyTaint"
+  include Lattice.Prod3(JmpBufSet)(BoolDomain.MayBool)(BoolDomain.MayBool)
+  let buffers (buffer,_,_) = buffer
+  let copied (_,copied,_) = copied
+  let invalid (_,_,invalid) = invalid
+  let name () = "JumpbufferTaintOrInvalid"
 end
 
 
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index d748706ad1..3f42978167 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -79,7 +79,7 @@ struct
 end
 
 module Threads = ConcDomain.ThreadSet
-module JmpBufs = JmpBufDomain.JmpBufSetTaint
+module JmpBufs = JmpBufDomain.JmpBufSetTaintInvalid
 
 module rec Compound: sig
   type t =
@@ -153,7 +153,7 @@ struct
       Array (CArrays.make ~varAttr ~typAttr len (bot_value ai))
     | t when is_thread_type t -> Thread (ConcDomain.ThreadSet.empty ())
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.bot ())
-    | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false)
+    | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false, false)
     | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t)
     | _ -> Bot
 
@@ -724,7 +724,7 @@ struct
       Array (CArrays.set ask n (array_idx_top) v)
     |                 t , Blob n       -> Blob (Blobs.invalidate_value ask t n)
     |                 _ , Thread tid   -> Thread (Threads.join (Threads.top ()) tid)
-    |                 _ , JmpBuf _     -> state (* TODO: no top jmpbuf *)
+    |                 _ , JmpBuf (b, c, _)     -> JmpBuf(b, c, true) (* TODO: no top jmpbuf *)
     | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
     |                 t , _             -> top_value t
 
@@ -1007,7 +1007,7 @@ struct
             | Blob(Bot, _, _) -> Bot (* TODO: Stopgap for malloced jmp_bufs, there is something fundamentally flawed somewhere *)
             | _ ->
               if !AnalysisState.global_initialization then
-                JmpBuf (JmpBufs.Bufs.empty (), false) (* if assigning global init, use empty set instead *)
+                JmpBuf (JmpBufs.Bufs.empty (), false, false) (* if assigning global init, use empty set instead *)
               else
                 Top
           end
@@ -1172,7 +1172,7 @@ struct
 
   let rec mark_jmpbufs_as_copied (v:t):t =
     match v with
-    | JmpBuf (v,t) -> JmpBuf (v, true)
+    | JmpBuf (v,t,i) -> JmpBuf (v, true, i)
     | 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)
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index d47f1efde0..dcc4cfa1e5 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -213,7 +213,8 @@ let createCFG (file: file) =
 
         | Instr _
         | If _
-        | Return _ ->
+        | Return _
+        | Asm _ ->
           stmt, visited_stmts
 
         | Continue _
@@ -291,7 +292,6 @@ let createCFG (file: file) =
             let edge_of_instr = function
               | Set (lval,exp,loc,eloc) -> Cilfacade.eloc_fallback ~eloc ~loc, Assign (lval, exp)
               | Call (lval,func,args,loc,eloc) -> Cilfacade.eloc_fallback ~eloc ~loc, Proc (lval,func,args)
-              | Asm (attr,tmpl,out,inp,regs,loc) -> loc, ASM (tmpl,out,inp)
               | VarDecl (v, loc) -> loc, VDecl(v)
             in
             let edges = List.map edge_of_instr instrs in
@@ -374,6 +374,24 @@ let createCFG (file: file) =
             (* Nothing to do, find_real_stmt skips over these. *)
             ()
 
+          | Asm (_, tmpls, outs, ins, _, labels, loc) ->
+            begin match real_succs () with
+              | [] -> failwith "MyCFG.createCFG: 0 Asm succ"
+              | [succ, skippedStatements] -> begin
+                addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
+                if not (get_bool "asm_is_nop") then
+                  let unique_dests = List.fold_left (fun acc label ->
+                    let succ', skippedStatements' = find_real_stmt ~parent:stmt !label in
+                    match List.assoc_opt succ' acc with
+                    | None when succ' != succ -> (succ', skippedStatements') :: acc
+                    | _ -> acc
+                    ) [] labels in
+                  List.iter (fun (succ, skippedStatements) ->
+                    addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, true)) (Statement succ)
+                    ) unique_dests;
+              end
+              | _ -> failwith "MyCFG.createCFG: >1 Asm succ"
+            end
           | Continue _
           | Break _
           | Switch _ ->
@@ -382,6 +400,7 @@ let createCFG (file: file) =
 
           | ComputedGoto _ ->
             failwith "CfgTools.createCFG: unsupported stmt"
+        
         in
         Timing.wrap ~args:[("function", `String fd.svar.vname)] "handle" (List.iter handle) fd.sallstmts;
 
diff --git a/src/common/framework/edge.ml b/src/common/framework/edge.ml
index e6f214a4c8..8e66177bcb 100644
--- a/src/common/framework/edge.ml
+++ b/src/common/framework/edge.ml
@@ -21,9 +21,10 @@ type t =
     * transferred to the function node! *)
   | Test of CilType.Exp.t * bool
   (** The true-branch or false-branch of a conditional exp *)
-  | ASM of string list * asm_out * asm_in
+  | ASM of string list * asm_out * asm_in * bool
   (** Inline assembly statements, and the annotations for output and input
-    * variables. *)
+    * variables. The last field is a flag that indicates if this is an edge that
+    * was inserted because of asm goto labels. *)
   | VDecl of CilType.Varinfo.t
   (** VDecl edge for the variable in varinfo. Whether such an edge is there for all
     * local variables or only when it is not possible to pull the declaration up, is
@@ -43,7 +44,7 @@ let pretty () = function
   | Entry (f) -> Pretty.text "(body)"
   | Ret (Some e,f) -> Pretty.dprintf "return %a" dn_exp e
   | Ret (None,f) -> Pretty.dprintf "return"
-  | ASM (_,_,_) -> Pretty.text "ASM ..."
+  | ASM (_,_,_,_) -> Pretty.text "ASM ..."
   | Skip -> Pretty.text "skip"
   | VDecl v -> Cil.defaultCilPrinter#pVDecl () v
 
@@ -91,7 +92,7 @@ let to_yojson e =
         ("function", CilType.Fundec.to_yojson function_);
         ("exp", [%to_yojson: CilType.Exp.t option] exp);
       ]
-    | ASM (instructions, output, input) ->
+    | ASM (instructions, output, input, _) ->
       [
         ("type", `String "asm");
         ("instructions", [%to_yojson: string list] instructions);
diff --git a/src/common/framework/myCFG.ml b/src/common/framework/myCFG.ml
index 76675f3c88..5a66d220db 100644
--- a/src/common/framework/myCFG.ml
+++ b/src/common/framework/myCFG.ml
@@ -17,7 +17,7 @@ type edge = Edge.t =
   | Entry of CilType.Fundec.t
   | Ret of CilType.Exp.t option * CilType.Fundec.t
   | Test of CilType.Exp.t * bool
-  | ASM of string list * Edge.asm_out * Edge.asm_in
+  | ASM of string list * Edge.asm_out * Edge.asm_in * bool
   | VDecl of CilType.Varinfo.t
   | Skip
 
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index d80ce49543..260f9524fa 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -480,13 +480,14 @@ class countFnVisitor = object
     | Switch (_,_,_,loc,_)
     | Loop (_,loc,_,_,_)
       -> Hashtbl.replace locs loc.line (); DoChildren
+    | Asm (_,_,_,_,_,_,loc)
+      -> Hashtbl.replace locs loc.line (); SkipChildren
     | _ ->
       DoChildren
 
   method! vinst = function
     | Set (_,_,loc,_)
     | Call (_,_,_,loc,_)
-    | Asm (_,_,_,_,_,loc)
       -> Hashtbl.replace locs loc.line (); SkipChildren
     | _ -> SkipChildren
 
diff --git a/src/common/util/cilfacade0.ml b/src/common/util/cilfacade0.ml
index 35fd5fb706..989d0bd316 100644
--- a/src/common/util/cilfacade0.ml
+++ b/src/common/util/cilfacade0.ml
@@ -29,7 +29,6 @@ let eloc_fallback ~eloc ~loc =
 let get_instrLoc = function
   | Set (_, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Call (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
-  | Asm (_, _, _, _, _, loc) -> loc
   | VarDecl (_, loc) -> loc
 
 (** Get expression location for [Cil.stmt]. *)
@@ -51,3 +50,4 @@ let rec get_stmtLoc stmt =
   | Switch (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Loop (_, loc, eloc, _, _) -> eloc_fallback ~eloc ~loc
   | Block {bstmts = hd :: _; _} -> get_stmtLoc hd
+  | Asm (_, _, _, _, _, _, loc) -> loc
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 0c83e342e0..fa01e7c655 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -17,6 +17,12 @@
       "type": "string",
       "default": ""
     },
+    "asm_is_nop": {
+      "title": "asm_is_nop",
+      "description": "Treat assembly statements as NOOP",
+      "type": "boolean",
+      "default": true
+    },
     "justcil": {
       "title": "justcil",
       "description": "Just parse and output the CIL.",
diff --git a/src/domains/events.ml b/src/domains/events.ml
index 06561bddbe..375eb63236 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -16,6 +16,7 @@ type t =
   | Assert of exp
   | Unassume of {exp: CilType.Exp.t; uuids: string list}
   | Longjmped of {lval: CilType.Lval.t option}
+  | Invalidate of {lvals: CilType.Lval.t list}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
 let emit_on_deadcode = function
@@ -31,7 +32,8 @@ let emit_on_deadcode = function
   | UpdateExpSplit _ (* Pointless to split on dead. *)
   | Unassume _ (* Avoid spurious writes. *)
   | Assert _ (* Pointless to refine dead. *)
-  | Longjmped _ ->
+  | Longjmped _
+  | Invalidate _ ->
     false
 
 let pretty () = function
@@ -47,3 +49,4 @@ let pretty () = function
   | 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
+  | Invalidate {lvals} -> dprintf "Invalidate {vars=%a}" (docList (d_lval ())) lvals
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 61f43cb1a5..44863ae062 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -177,7 +177,6 @@ let ctx_failwith s = raise (Ctx_failure s) (* TODO: use everywhere in ctx *)
 (** Convert [ctx] to [Queries.ask]. *)
 let ask_of_ctx ctx: Queries.ask = { Queries.f = ctx.ask }
 
-
 module type Spec =
 sig
   module D : Lattice.S
@@ -231,8 +230,9 @@ sig
       "return exp" or "return" in the passed function (fundec) *)
   val return: (D.t, G.t, C.t, V.t) ctx -> exp option  -> fundec -> D.t
 
-  (** A transfer function meant to handle inline assembler program points *)
-  val asm   : (D.t, G.t, C.t, V.t) ctx -> D.t
+  (** A transfer function meant to handle inline assembler program points.
+      It gets outputs (written by asm) and inputs (read by asm) as arguments. *)
+  val asm   : (D.t, G.t, C.t, V.t) ctx -> lval list -> exp list -> D.t
 
   (** A transfer function which works as the identity function, i.e., it skips and does nothing.
       Used for empty loops. *)
@@ -357,10 +357,12 @@ struct
 
   let vdecl ctx _ = ctx.local
 
-  let asm x =
-    M.msg_final Info ~category:Unsound "ASM ignored";
-    M.info ~category:Unsound "ASM statement ignored.";
-    x.local (* Just ignore. *)
+  let asm ctx outs ins =
+    if get_bool "asm_is_nop" then begin
+      M.msg_final Info ~category:Unsound "ASM ignored";
+      M.info ~category:Unsound "ASM statement ignored.";
+    end;
+    ctx.local
 
   let skip x = x.local (* Just ignore. *)
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 84d7eff1ed..0b379221fc 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -71,8 +71,8 @@ struct
   let return ctx r f =
     D.lift @@ S.return (conv ctx) r f
 
-  let asm ctx =
-    D.lift @@ S.asm (conv ctx)
+  let asm ctx outs ins =
+    D.lift @@ S.asm (conv ctx) outs ins
 
   let skip ctx =
     D.lift @@ S.skip (conv ctx)
@@ -155,8 +155,8 @@ struct
   let return ctx r f =
     S.return (conv ctx) r f
 
-  let asm ctx =
-    S.asm (conv ctx)
+  let asm ctx outs ins =
+    S.asm (conv ctx) outs ins
 
   let skip ctx =
     S.skip (conv ctx)
@@ -244,13 +244,13 @@ struct
   let sync ctx reason = lift_fun ctx (lift ctx) S.sync   ((|>) reason)
   let query' ctx (type a) (q: a Queries.t): a Queries.result =
     lift_fun ctx identity   S.query  (fun x -> x q)
-  let assign ctx lv e = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv)
-  let vdecl ctx v     = lift_fun ctx (lift ctx) S.vdecl  ((|>) v)
-  let branch ctx e tv = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e)
-  let body ctx f      = lift_fun ctx (lift ctx) S.body   ((|>) f)
-  let return ctx r f  = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
-  let asm ctx         = lift_fun ctx (lift ctx) S.asm    identity
-  let skip ctx        = lift_fun ctx (lift ctx) S.skip   identity
+  let assign ctx lv e  = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v      = lift_fun ctx (lift ctx) S.vdecl  ((|>) v)
+  let branch ctx e tv  = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e)
+  let body ctx f       = lift_fun ctx (lift ctx) S.body   ((|>) f)
+  let return ctx r f   = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
+  let asm ctx outs ins = lift_fun ctx (lift ctx) S.asm    ((|>) ins % (|>) outs)
+  let skip ctx         = lift_fun ctx (lift ctx) S.skip   identity
   let special ctx r f args        = lift_fun ctx (lift ctx) S.special ((|>) args % (|>) f % (|>) r)
   let combine_env' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
   let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
@@ -387,15 +387,15 @@ struct
     }
   let lift_fun ctx f g = g (f (conv ctx)), snd ctx.local
 
-  let sync ctx reason = lift_fun ctx S.sync   ((|>) reason)
-  let query ctx       = S.query (conv ctx)
-  let assign ctx lv e = lift_fun ctx S.assign ((|>) e % (|>) lv)
-  let vdecl ctx v     = lift_fun ctx S.vdecl  ((|>) v)
-  let branch ctx e tv = lift_fun ctx S.branch ((|>) tv % (|>) e)
-  let body ctx f      = lift_fun ctx S.body   ((|>) f)
-  let return ctx r f  = lift_fun ctx S.return ((|>) f % (|>) r)
-  let asm ctx         = lift_fun ctx S.asm    identity
-  let skip ctx        = lift_fun ctx S.skip   identity
+  let sync ctx reason  = lift_fun ctx S.sync   ((|>) reason)
+  let query ctx        = S.query (conv ctx)
+  let assign ctx lv e  = lift_fun ctx S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v      = lift_fun ctx S.vdecl  ((|>) v)
+  let branch ctx e tv  = lift_fun ctx S.branch ((|>) tv % (|>) e)
+  let body ctx f       = lift_fun ctx S.body   ((|>) f)
+  let return ctx r f   = lift_fun ctx S.return ((|>) f % (|>) r)
+  let asm ctx outs ins = lift_fun ctx S.asm    ((|>) ins % (|>) outs)
+  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)
@@ -480,13 +480,13 @@ struct
 
   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
-  let vdecl ctx v     = lift_fun ctx D.lift   S.vdecl  ((|>) v)            `Bot
-  let branch ctx e tv = lift_fun ctx D.lift   S.branch ((|>) tv % (|>) e) `Bot
-  let body ctx f      = lift_fun ctx D.lift   S.body   ((|>) f)            `Bot
-  let return ctx r f  = lift_fun ctx D.lift   S.return ((|>) f % (|>) r)  `Bot
-  let asm ctx         = lift_fun ctx D.lift   S.asm    identity           `Bot
-  let skip ctx        = lift_fun ctx D.lift   S.skip   identity           `Bot
+  let assign ctx lv e  = lift_fun ctx D.lift   S.assign ((|>) e % (|>) lv) `Bot
+  let vdecl ctx v      = lift_fun ctx D.lift   S.vdecl  ((|>) v)            `Bot
+  let branch ctx e tv  = lift_fun ctx D.lift   S.branch ((|>) tv % (|>) e) `Bot
+  let body ctx f       = lift_fun ctx D.lift   S.body   ((|>) f)            `Bot
+  let return ctx r f   = lift_fun ctx D.lift   S.return ((|>) f % (|>) r)  `Bot
+  let asm ctx outs ins = lift_fun ctx D.lift   S.asm    ((|>) ins % (|>) outs)  `Bot
+  let skip ctx         = lift_fun ctx D.lift   S.skip   identity           `Bot
   let special ctx r f args       = lift_fun ctx D.lift S.special ((|>) args % (|>) f % (|>) r)        `Bot
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
@@ -765,9 +765,12 @@ struct
     end else
       common_joins ctx funs !r !spawns
 
-  let tf_asm var edge prev_node getl sidel getg sideg d =
+  let tf_asm var edge prev_node outs ins getl sidel getg sideg d =
+    let third (_, _, x) = x in
+    let outs = Util.list_map third outs in
+    let ins = Util.list_map third ins in
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.asm ctx) !r !spawns
+    common_join ctx (S.asm ctx outs ins) !r !spawns
 
   let tf_skip var edge prev_node getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
@@ -775,14 +778,14 @@ struct
 
   let tf var getl sidel getg sideg prev_node edge d =
     begin match edge with
-      | Assign (lv,rv) -> tf_assign var edge prev_node lv rv
-      | VDecl (v)      -> tf_vdecl var edge prev_node v
-      | Proc (r,f,ars) -> tf_proc var edge prev_node r f ars
-      | Entry f        -> tf_entry var edge prev_node f
-      | Ret (r,fd)     -> tf_ret var edge prev_node r fd
-      | Test (p,b)     -> tf_test var edge prev_node p b
-      | ASM (_, _, _)  -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
-      | Skip           -> tf_skip var edge prev_node
+      | Assign (lv,rv)  -> tf_assign var edge prev_node lv rv
+      | VDecl (v)       -> tf_vdecl var edge prev_node v
+      | Proc (r,f,ars)  -> tf_proc var edge prev_node r f ars
+      | Entry f         -> tf_entry var edge prev_node f
+      | Ret (r,fd)      -> tf_ret var edge prev_node r fd
+      | Test (p,b)      -> tf_test var edge prev_node p b
+      | ASM (_, outs, ins,_) -> tf_asm var edge prev_node outs ins
+      | Skip            -> tf_skip var edge prev_node
     end getl sidel getg sideg d
 
   type Goblint_backtrace.mark += TfLocation of location
@@ -1098,7 +1101,7 @@ struct
   let body   ctx f      = map ctx Spec.body    (fun h -> h f   )
   let return ctx e f    = map ctx Spec.return  (fun h -> h e f )
   let branch ctx e tv   = map ctx Spec.branch  (fun h -> h e tv)
-  let asm ctx           = map ctx Spec.asm     identity
+  let asm ctx outs ins  = map ctx Spec.asm     (fun h -> h outs ins)
   let skip ctx          = map ctx Spec.skip    identity
   let special ctx l f a = map ctx Spec.special (fun h -> h l f a)
 
@@ -1298,7 +1301,7 @@ struct
   let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple 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 asm ctx outs ins = S.asm (conv ctx) outs ins
   let event ctx e octx = S.event (conv ctx) e (conv octx)
 end
 
@@ -1540,7 +1543,7 @@ struct
   let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple 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 asm ctx outs ins = S.asm (conv ctx) outs ins
   let event ctx e octx = S.event (conv ctx) e (conv octx)
 end
 
@@ -1683,7 +1686,7 @@ struct
   let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple 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 asm ctx outs ins = S.asm (conv ctx) outs ins
   let event ctx e octx = S.event (conv ctx) e (conv octx)
 end
 
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index c79735c2b1..e73e64a029 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -309,11 +309,6 @@ let eq_instr (a: instr) (b: instr) ~(rename_mapping: rename_mapping) = match a,
     eq_lval lv1 lv2 ~rename_mapping &&>> eq_exp f1 f2 &&>> forward_list_equal eq_exp args1 args2
   | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) ->
     eq_exp f1 f2 ~rename_mapping &&>> forward_list_equal eq_exp args1 args2
-  | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) ->
-    (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>>
-    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>>
-    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&>
-    GobList.equal String.equal rk1 rk2(* ignore attributes and locations *)
   | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2 ~rename_mapping
   | _, _ -> false, rename_mapping
 
@@ -351,6 +346,12 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s
   | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 ~rename_mapping &&>> eq_block' block1 block2 &&>> forward_list_equal (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
   | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2 ~rename_mapping
   | Block block1, Block block2 -> eq_block' block1 block2 ~rename_mapping
+  | Asm (attr1, tmp1, ci1, dj1, rk1, lb1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, lb2, l2) ->
+    (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>>
+    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>>
+    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&>
+    GobList.equal String.equal rk1 rk2(* ignore attributes and locations *) &&>
+    GobList.equal (fun st1 st2 -> eq_stmt_with_location (!st1, af) (!st2, bf)) lb1 lb2
   | _, _ -> false, rename_mapping
 
 and eq_stmt ?cfg_comp ((a, af): stmt * fundec) ((b, bf): stmt * fundec) ~(rename_mapping: rename_mapping) =
diff --git a/src/transform/deadCode.ml b/src/transform/deadCode.ml
index 1b9db8d06a..35744ba27f 100644
--- a/src/transform/deadCode.ml
+++ b/src/transform/deadCode.ml
@@ -72,7 +72,7 @@ let filter_map_block ?(unchecked_condition = Fun.const (GoblintCil.integer 1)) f
         let keep_block = impl_block b in
         if keep_stmt || keep_block then Some skind else None
 
-      | Instr _ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ as skind ->
+      | Instr _ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ as skind ->
         (* no further statements are contained recursively here, so nothing left to do *)
         if keep_stmt then Some skind else None
 
@@ -91,7 +91,7 @@ let filter_map_block ?(unchecked_condition = Fun.const (GoblintCil.integer 1)) f
 (** Is it possible for this statement to begin executing normally, but not finish? *)
 let may_stop_execution stmt =
   match stmt.skind with
-  | Instr is -> List.exists (function Call _ | Asm _ -> true | _ -> false) is
+  | Instr is -> List.exists (function Call _ -> true | _ -> false) is
   | _ -> false
 
 (** Perform a depth first search over the CFG. Record the IDs of live statements;
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index 1816de90c7..d71ade1851 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -168,13 +168,13 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     lift_fun ctx Fun.const S.query (fun (x) -> x q)
-  let assign ctx lv e = lift_fun ctx lift'   S.assign ((|>) e % (|>) lv)
-  let vdecl ctx v     = lift_fun ctx lift'   S.vdecl  ((|>) v)
-  let branch ctx e tv = lift_fun ctx lift'   S.branch ((|>) tv % (|>) e)
-  let body ctx f      = lift_fun ctx lift'   S.body   ((|>) f)
-  let return ctx r f  = lift_fun ctx lift'   S.return ((|>) f % (|>) r)
-  let asm ctx         = lift_fun ctx lift'   S.asm    identity
-  let skip ctx        = lift_fun ctx lift'   S.skip   identity
+  let assign ctx lv e  = lift_fun ctx lift'   S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v      = lift_fun ctx lift'   S.vdecl  ((|>) v)
+  let branch ctx e tv  = lift_fun ctx lift'   S.branch ((|>) tv % (|>) e)
+  let body ctx f       = lift_fun ctx lift'   S.body   ((|>) f)
+  let return ctx r f   = lift_fun ctx lift'   S.return ((|>) f % (|>) r)
+  let asm ctx outs ins = lift_fun ctx lift'   S.asm    ((|>) ins % (|>) outs)
+  let skip ctx         = lift_fun ctx lift'   S.skip   identity
   let special ctx r f args       = lift_fun ctx lift' S.special ((|>) args % (|>) f % (|>) r)
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 8dedf77a79..188819a7ef 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -189,7 +189,7 @@ struct
   let body   ctx f      = map ctx Spec.body    (fun h -> h f   )
   let return ctx e f    = map ctx Spec.return  (fun h -> h e f )
   let branch ctx e tv   = map ctx Spec.branch  (fun h -> h e tv)
-  let asm ctx           = map ctx Spec.asm     identity
+  let asm ctx outs ins  = map ctx Spec.asm     (fun h -> h outs ins)
   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: ???? *)
diff --git a/tests/regression/65-taint/02-invalidate.c b/tests/regression/65-taint/02-invalidate.c
index cf4636192f..1b0010118e 100644
--- a/tests/regression/65-taint/02-invalidate.c
+++ b/tests/regression/65-taint/02-invalidate.c
@@ -4,7 +4,7 @@
 extern void unknown_fun (int *a);
 
 void mainfunct(int *rptr, int* uptr) {
-  unknown_fun(rptr);
+      unknown_fun(rptr);
 }
 
 int g;
diff --git a/tests/regression/79-assembly/01-assembly-invalidate.c b/tests/regression/79-assembly/01-assembly-invalidate.c
new file mode 100644
index 0000000000..7507a8075b
--- /dev/null
+++ b/tests/regression/79-assembly/01-assembly-invalidate.c
@@ -0,0 +1,12 @@
+// PARAM: --set asm_is_nop false
+
+#include <goblint.h>
+
+int main(void) {
+
+    int v = 0;
+
+    __asm__("nop": "=x"(v)); 
+
+    __goblint_assert(v==0); //UNKNOWN
+}
\ No newline at end of file
diff --git a/tests/regression/79-assembly/02-assembly-precision.c b/tests/regression/79-assembly/02-assembly-precision.c
new file mode 100644
index 0000000000..4b318a7cf3
--- /dev/null
+++ b/tests/regression/79-assembly/02-assembly-precision.c
@@ -0,0 +1,18 @@
+// PARAM: --set asm_is_nop false
+
+#include <goblint.h>
+
+int main(void) {
+
+    int r;
+    int v;
+
+    __asm__ goto ("nop": : : : test);
+
+    v = 0;
+
+    test:
+
+    __goblint_assert(v == 0); //UNKNOWN
+
+}
\ No newline at end of file
diff --git a/tests/regression/79-assembly/03-asm-use-after-free.c b/tests/regression/79-assembly/03-asm-use-after-free.c
new file mode 100644
index 0000000000..47d57f92f6
--- /dev/null
+++ b/tests/regression/79-assembly/03-asm-use-after-free.c
@@ -0,0 +1,11 @@
+//PARAM: --set ana.activated[+] useAfterFree --disable asm_is_nop
+#include <stdlib.h>
+
+int main(void) {
+  int *x = malloc(16);
+  free(x);
+  // write
+  asm ("nop" : "=x" (*x)); // WARN
+  // read
+  asm ("nop" : : "x" (*x)); // WARN
+}
diff --git a/tests/regression/79-assembly/04-asm-modified-since-setjmp.c b/tests/regression/79-assembly/04-asm-modified-since-setjmp.c
new file mode 100644
index 0000000000..dcc6dedab7
--- /dev/null
+++ b/tests/regression/79-assembly/04-asm-modified-since-setjmp.c
@@ -0,0 +1,20 @@
+#include <setjmp.h>
+
+jmp_buf buf;
+
+int main(void) {
+  int x;
+start:
+  x = 5;
+  if (setjmp(buf)) {
+    //read
+    asm ("nop" : : "x" (x));
+    return 0;
+  } else {
+    //write
+    asm goto ("nop" : "=x" (x) : : : exit2, exit); //WARN
+    longjmp(buf, 1);
+  }
+exit2:
+exit: return 0;
+}
diff --git a/tests/regression/79-assembly/05-asm-var-eq.c b/tests/regression/79-assembly/05-asm-var-eq.c
new file mode 100644
index 0000000000..ff53cbcb54
--- /dev/null
+++ b/tests/regression/79-assembly/05-asm-var-eq.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --disable asm_is_nop
+#include<goblint.h>
+#include<stdio.h>
+
+void not_ok(int x) {
+  int y = x;
+  asm ("nop" : "=x" (x));
+  __goblint_check(x == y); // UNKNOWN
+}
+
+void ok(int x) {
+  asm ("nop" : "=x" (x));
+  int y = x;
+  __goblint_check(x == y);
+}
+
+int main() {
+  int x;
+  scanf("%d", &x);
+  ok(x);
+  not_ok(x);
+}
diff --git a/tests/regression/79-assembly/06-asm-uninit.c b/tests/regression/79-assembly/06-asm-uninit.c
new file mode 100644
index 0000000000..a02c6c4393
--- /dev/null
+++ b/tests/regression/79-assembly/06-asm-uninit.c
@@ -0,0 +1,8 @@
+// PARAM: --set ana.activated[+] uninit --disable asm_is_nop
+
+int main() {
+  int x, y, z;
+  asm ("nop" : "=x" (y) : "x" (x)); // WARN
+  z = y + 1; // NOWARN
+  return 0;
+}
diff --git a/tests/regression/79-assembly/07-asm-exp-split.c b/tests/regression/79-assembly/07-asm-exp-split.c
new file mode 100644
index 0000000000..c686ee337f
--- /dev/null
+++ b/tests/regression/79-assembly/07-asm-exp-split.c
@@ -0,0 +1,12 @@
+// PARAM: --set ana.activated[+] expsplit --disable asm_is_nop
+#include <goblint.h>
+
+int main(void) {
+  int r, x;
+  __goblint_split_begin(x);
+  x = r ? 1 : 0;
+  asm("nop" : "=x" (x), "=x" (r));
+  __goblint_check(x == 0 || x == 1); // UNKNOWN (without asm it would be known)
+  __goblint_split_end(x);
+  __goblint_check(x == 0 || x == 1); // UNKNOWN
+}
diff --git a/tests/regression/79-assembly/08-asm-mutex.c b/tests/regression/79-assembly/08-asm-mutex.c
new file mode 100644
index 0000000000..eefacbbb6f
--- /dev/null
+++ b/tests/regression/79-assembly/08-asm-mutex.c
@@ -0,0 +1,14 @@
+// PARAM: --set ana.activated[+] mutexEvents --disable asm_is_nop
+#include <pthread.h>
+
+pthread_mutex_t mutex;
+
+int main() {
+    int x = 2;
+    pthread_mutex_init(&mutex, NULL);
+    pthread_mutex_lock(&mutex);
+    asm ("nop" : "=g" (mutex), "=x" (x));
+    pthread_mutex_unlock(&mutex); // WARN
+    return 0;
+}
+
diff --git a/tests/regression/79-assembly/09-asm-invalidate-condvar.c b/tests/regression/79-assembly/09-asm-invalidate-condvar.c
new file mode 100644
index 0000000000..e6da610251
--- /dev/null
+++ b/tests/regression/79-assembly/09-asm-invalidate-condvar.c
@@ -0,0 +1,28 @@
+// PARAM: --set ana.activated[+] condvars --set ana.activated[+] taintPartialContexts --disable asm_is_nop
+#include <goblint.h>
+
+int glob;
+
+void f() {
+}
+
+int main() {
+  int unk;
+  int tv;
+  if (unk)
+    glob = 0;
+  else
+    glob = 10;
+
+  tv = (glob == 0);
+  f();
+  
+  __asm__("nop": "=x"(glob): "x="(glob));
+
+  if (tv)
+    __goblint_assert(glob == 0); //UNKNOWN
+  else 
+    __goblint_assert(glob != 0); //UNKNOWN
+
+}
+
diff --git a/tests/regression/79-assembly/10-asm-deadlock.c b/tests/regression/79-assembly/10-asm-deadlock.c
new file mode 100644
index 0000000000..82cad87968
--- /dev/null
+++ b/tests/regression/79-assembly/10-asm-deadlock.c
@@ -0,0 +1,31 @@
+//PARAM: --set ana.activated[+] deadlock --disable asm_is_nop
+#include <unistd.h>
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t lock_a;
+pthread_mutex_t lock_b;
+
+void *proc_a(void *arg) {
+    pthread_mutex_lock(&lock_a);
+    asm ("nop" : "=g" (lock_a));
+    sleep(1);
+    pthread_mutex_lock(&lock_b);
+    pthread_exit(NULL);
+}
+
+void *proc_b(void *arg) {
+    pthread_mutex_lock(&lock_b);
+    sleep(1);
+    pthread_mutex_lock(&lock_a);
+    return NULL;
+}
+
+int main(void) {
+    int x;
+    pthread_t a, b;
+    pthread_create(&a, NULL, proc_a, NULL);
+    proc_b(NULL);
+    // this will remove lock_a from must_lockset
+    puts("no deadlock!");
+}
diff --git a/tests/regression/79-assembly/11-asm-mem-leak.c b/tests/regression/79-assembly/11-asm-mem-leak.c
new file mode 100644
index 0000000000..0ffbeb3c57
--- /dev/null
+++ b/tests/regression/79-assembly/11-asm-mem-leak.c
@@ -0,0 +1,23 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --disable asm_is_nop
+#include <stdlib.h>
+
+void ok(void) {
+  char *x = malloc(64);
+  char *y = x;
+  asm ("nop" : "=x" (x));
+  free(y);
+  return; //NOWARN
+}
+
+void not_ok(void) {
+  char *x = malloc(64);
+  asm ("nop" : "=x" (x));
+  free(x); //WARN
+  return;
+}
+
+int main(void) {
+  ok();
+  not_ok();
+  return 0;
+}
diff --git a/tests/regression/79-assembly/12-asm-taint.c b/tests/regression/79-assembly/12-asm-taint.c
new file mode 100644
index 0000000000..cfdcf146a3
--- /dev/null
+++ b/tests/regression/79-assembly/12-asm-taint.c
@@ -0,0 +1,27 @@
+//PARAM --set "ana.activated[+]" taintPartialContexts --set ana.ctx_insens[+] base --disable asm_is_nop
+#include <goblint.h>
+
+
+void mainfunct(int *rptr, int* uptr) {
+      asm("nop" : "=x"(*rptr));
+}
+
+int g;
+
+int main() {
+  int r, u;
+
+  g = 1;
+  r = 1;
+  u = 1;
+  mainfunct(&r, &u);
+
+  g = 2;
+  r = 2;
+  u = 2;
+  mainfunct(&r, &u);
+
+  __goblint_check(g == 2); //UNKNOWN!
+  __goblint_check(r == 2); //UNKNOWN!
+  __goblint_check(u == 2);
+}
diff --git a/tests/regression/79-assembly/13-jmpbuf-invalid.c b/tests/regression/79-assembly/13-jmpbuf-invalid.c
new file mode 100644
index 0000000000..5541e706e3
--- /dev/null
+++ b/tests/regression/79-assembly/13-jmpbuf-invalid.c
@@ -0,0 +1,14 @@
+// PARAM: --set asm_is_nop false
+#include <setjmp.h>
+
+jmp_buf buf;
+
+int main(void) {
+
+    if (!setjmp(buf)) {
+
+        __asm__("nop" : "=m"(buf));
+
+        longjmp(buf, 1); //WARN
+    }
+}
\ No newline at end of file
diff --git a/tests/regression/79-assembly/14-asm-region.c b/tests/regression/79-assembly/14-asm-region.c
new file mode 100644
index 0000000000..64ffe469bb
--- /dev/null
+++ b/tests/regression/79-assembly/14-asm-region.c
@@ -0,0 +1,13 @@
+//PARAM: --set ana.activated[+] region --disable asm_is_nop
+#include <stdlib.h>
+
+int main() {
+    char *buffer = malloc(256);  
+    buffer[0] = 'a';            
+
+    
+    __asm__("movb $0, %0" : "=m" (*buffer));
+
+    free(buffer);               
+    return 0;
+}
diff --git a/tests/regression/79-assembly/15-jumpbuf-poison.c b/tests/regression/79-assembly/15-jumpbuf-poison.c
new file mode 100644
index 0000000000..e44474611f
--- /dev/null
+++ b/tests/regression/79-assembly/15-jumpbuf-poison.c
@@ -0,0 +1,25 @@
+// PARAM: --disable asm_is_nop
+#include <stdio.h>
+#include <setjmp.h>
+
+jmp_buf buf;
+
+void test(void) {
+
+	longjmp(buf, 1);
+}
+
+int main(void) {
+
+	int i = 0;
+
+	if (setjmp(buf)){
+	
+		printf("After Jump: %d\n",i); //WARN
+	} else {
+	
+		printf("Setting i to 69; %d\n", i);
+		asm ("nop" : "=x"(i) : "=x"(i));
+		test();
+	}
+}
diff --git a/tests/regression/79-assembly/16-jumpbuf-read-poison.c b/tests/regression/79-assembly/16-jumpbuf-read-poison.c
new file mode 100644
index 0000000000..8f409bf1de
--- /dev/null
+++ b/tests/regression/79-assembly/16-jumpbuf-read-poison.c
@@ -0,0 +1,25 @@
+// PARAM: --disable asm_is_nop
+#include <stdio.h>
+#include <setjmp.h>
+
+jmp_buf buf;
+
+void test(void) {
+
+	longjmp(buf, 1);
+}
+
+int main(void) {
+
+	int i = 0;
+
+	if (setjmp(buf)){
+	
+		asm ("nop" : "x="(i):"x="(i)); //WARN
+	} else {
+	
+		printf("Setting i to 69; %d\n", i);
+		i = 10;
+		test();
+	}
+}