diff --git a/src/cfg.ml b/src/cfg.ml
index 8ce0c52a6..74d3bb825 100644
--- a/src/cfg.ml
+++ b/src/cfg.ml
@@ -225,6 +225,7 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
       cfgBlock blk (Some s) next (Some s) nodeList rlabels
       (* Since all loops have terminating condition true, we don't put
          any direct successor to stmt following the loop *)
+  | Asm (_, _, _, _, _, labels, _) -> addOptionSucc next (* the extra edges are added inside goblint's cfg *)
 
 (*------------------------------------------------------------*)
 
@@ -247,7 +248,7 @@ and fasStmt (todo) (s : stmt) =
       | If (_, tb, fb, _, _) -> (fasBlock todo tb; fasBlock todo fb)
       | Switch (_, b, _, _, _) -> fasBlock todo b
       | Loop (b, _, _, _, _) -> fasBlock todo b
-      | (Return _ | Break _ | Continue _ | Goto _ | ComputedGoto _ | Instr _) -> ()
+      | (Return _ | Break _ | Continue _ | Goto _ | ComputedGoto _ | Instr _ | Asm _) -> ()
   end
 ;;
 
@@ -270,6 +271,7 @@ let d_cfgnodelabel () (s : stmt) =
       | Switch _ -> "switch"
       | Block _ -> "block"
       | Return _ -> "return"
+      | Asm _ -> "asm"
   end in
     dprintf "%d: %s" s.sid label
 
diff --git a/src/check.ml b/src/check.ml
index 2924fbe48..66e7cc46e 100644
--- a/src/check.ml
+++ b/src/check.ml
@@ -808,9 +808,22 @@ and checkStmt (s: stmt) =
               findCase !statements)
             cases;
 
-      | Instr il -> List.iter checkInstr il)
+      | Instr il -> List.iter checkInstr il
+      | Asm (_, _, _, _, _, labels, l) ->
+        currentLoc := l;
+        List.iter (fun dest ->
+          List.iter (fun label ->
+            let name = match label with
+              | Label (name, _, true) -> name
+              | _ -> failwith "unreachable"
+            in
+            gotoTargets := (name, !dest) :: !gotoTargets
+          ) !dest.labels;
+        ) labels;
+      )
     () (* argument of withContext *)
 
+
 and checkBlock (b: block) : unit =
   List.iter checkStmt b.bstmts
 
@@ -883,8 +896,6 @@ and checkInstr (i: instr) =
       if not v.vhasdeclinstruction then
         E.s (bug "Encountered a VarDecl, but vhasdeclinstruction for the varinfo is not set")
 
-  | Asm _ -> ()  (* Not yet implemented *)
-
 let rec checkGlobal = function
     GAsm _ -> ()
   | GPragma _ -> ()
diff --git a/src/cil.ml b/src/cil.ml
index 8a28dc19e..679dba247 100755
--- a/src/cil.ml
+++ b/src/cil.ml
@@ -813,6 +813,34 @@ and stmtkind =
                                             as a way to keep some attributes
                                             local *)
 
+  (* See the GCC specification for the meaning of ASM.
+     If the source is MS VC then only the templates
+     are used *)
+  (* sm: I've added a notes.txt file which contains more
+     information on interpreting Asm instructions *)
+  | Asm        of attributes * (* Really only const and volatile can appear
+          here *)
+  string list *         (* templates (CR-separated) *)
+  (string option * string * lval) list *
+                   (* outputs must be lvals with
+                      optional names and constraints.
+                      I would like these
+                      to be actually variables, but I
+                      run into some trouble with ASMs
+                      in the Linux sources  *)
+  (string option * string * exp) list *
+                 (* inputs with optional names and constraints *)
+  string list *         (* register clobbers *)
+  stmt ref list *       (* referenced labels *)
+  location
+  (** An inline assembly instruction. The arguments are (1) a list of
+  attributes (only const and volatile can appear here and only for
+  GCC), (2) templates (CR-separated), (3) a list of
+  outputs, each of which is an lvalue with a constraint, (4) a list
+  of input expressions along with constraints, (5) clobbered
+  registers, (6) the labels list for asm goto, and (7) location information *)
+
+
 (** Instructions. They may cause effects directly but may not have control
     flow.*)
 and instr =
@@ -840,33 +868,6 @@ and instr =
                              result then an implicit cast exists.
                              Second location is just for expression when inside condition. *)
 
-                         (* See the GCC specification for the meaning of ASM.
-                            If the source is MS VC then only the templates
-                            are used *)
-                         (* sm: I've added a notes.txt file which contains more
-                            information on interpreting Asm instructions *)
-  | Asm        of attributes * (* Really only const and volatile can appear
-                                 here *)
-                  string list *         (* templates (CR-separated) *)
-                  (string option * string * lval) list *
-                                          (* outputs must be lvals with
-                                             optional names and constraints.
-                                             I would like these
-                                             to be actually variables, but I
-                                             run into some trouble with ASMs
-                                             in the Linux sources  *)
-                  (string option * string * exp) list *
-                                        (* inputs with optional names and constraints *)
-                  string list *         (* register clobbers *)
-                  location
-        (** An inline assembly instruction. The arguments are (1) a list of
-            attributes (only const and volatile can appear here and only for
-            GCC), (2) templates (CR-separated), (3) a list of
-            outputs, each of which is an lvalue with a constraint, (4) a list
-            of input expressions along with constraints, (5) clobbered
-            registers, and (5) location information *)
-
-
 
 (** Describes a location in a source file *)
 and location = {
@@ -1125,7 +1126,6 @@ let get_instrLoc (inst : instr) =
   match inst with
       Set(_, _, loc, _) -> loc
     | Call(_, _, _, loc, _) -> loc
-    | Asm(_, _, _, _, _, loc) -> loc
     | VarDecl(_,loc) -> loc
 let get_globalLoc (g : global) =
   match g with
@@ -1155,6 +1155,7 @@ let rec get_stmtLoc (statement : stmtkind) =
     | Loop (_, loc, _, _, _) -> loc
     | Block b -> if b.bstmts == [] then lu
                  else get_stmtLoc ((List.hd b.bstmts).skind)
+    | Asm (_, _, _, _, _, _, loc) -> loc
 
 
 (* The next variable identifier to use. Counts up *)
@@ -1353,8 +1354,7 @@ let mkBlock (slst: stmt list) : block =
 let mkEmptyStmt () = mkStmt (Instr [])
 let mkStmtOneInstr (i: instr) = mkStmt (Instr [i])
 
-let dummyInstr = (Asm([], ["dummy statement!!"], [], [], [], lu))
-let dummyStmt =  mkStmt (Instr [dummyInstr])
+let dummyStmt =  mkStmt (Asm([], ["dummy statement!!"], [], [], [], [], lu))
 
 let compactStmts (b: stmt list) : stmt list =
       (* Try to compress statements. Scan the list of statements and remember
@@ -3708,53 +3708,6 @@ class defaultCilPrinterClass : cilPrinter = object (self)
              ++ unalign)
         ++ text (")" ^ printInstrTerminator)
 
-    | Asm(attrs, tmpls, outs, ins, clobs, l) ->
-        self#pLineDirective l
-          ++ text ("__asm__ ")
-          ++ self#pAttrs () attrs
-          ++ text " ("
-          ++ (align
-                ++ (docList ~sep:line
-                      (fun x -> text ("\"" ^ escape_string x ^ "\""))
-                      () tmpls)
-                ++
-                (if outs = [] && ins = [] && clobs = [] then
-                  chr ':'
-              else
-                (text ": "
-                    ++ (docList ~sep:(chr ',' ++ break)
-                          (fun (idopt, c, lv) ->
-                          text(match idopt with
-                                None -> ""
-                              | Some id -> "[" ^ id ^ "] "
-                          ) ++
-                            text ("\"" ^ escape_string c ^ "\" (")
-                              ++ self#pLval () lv
-                              ++ text ")") () outs)))
-              ++
-                (if ins = [] && clobs = [] then
-                  nil
-                else
-                  (text ": "
-                      ++ (docList ~sep:(chr ',' ++ break)
-                            (fun (idopt, c, e) ->
-                              text(match idopt with
-                                    None -> ""
-                                  | Some id -> "[" ^ id ^ "] "
-                              ) ++
-                              text ("\"" ^ escape_string c ^ "\" (")
-                                ++ self#pExp () e
-                                ++ text ")") () ins)))
-                ++
-                (if clobs = [] then nil
-                else
-                  (text ": "
-                      ++ (docList ~sep:(chr ',' ++ break)
-                            (fun c -> text ("\"" ^ escape_string c ^ "\""))
-                            ()
-                            clobs)))
-                ++ unalign)
-          ++ text (")" ^ printInstrTerminator)
 
 
   (**** STATEMENTS ****)
@@ -3977,6 +3930,82 @@ class defaultCilPrinterClass : cilPrinter = object (self)
                   ++ self#pBlock () b)
     end
     | Block b -> align ++ self#pBlock () b
+    | Asm(attrs, tmpls, outs, ins, clobs, labels, l) ->
+        let rec names_of_stmtrefs stmtrefs =
+          match stmtrefs with
+          | [] -> []
+          | stmtref :: xs -> 
+            let s = !stmtref in
+            let rec names_of_labels = function
+              | [] -> []
+              | Label (name, _, true) :: ys -> name :: names_of_labels ys
+              | Label (_, _, false) :: ys -> names_of_labels ys
+              | _ -> failwith "unreachable"
+            in
+            let names = names_of_labels s.labels in
+            let rest = names_of_stmtrefs xs in
+            let rec prepend_new_names (names: string list) rest =
+              match names with
+              | [] -> rest
+              | name :: ys when not (List.mem name rest) -> prepend_new_names ys (name :: rest)
+              | _ :: ys -> prepend_new_names ys rest
+            in
+            prepend_new_names names rest
+        in
+        self#pLineDirective l
+          ++ text ("__asm__ ")
+          ++ self#pAttrs () attrs
+          ++ text " ("
+          ++ (align
+                ++ (docList ~sep:line
+                      (fun x -> text ("\"" ^ escape_string x ^ "\""))
+                      () tmpls)
+                ++
+                (if outs = [] && ins = [] && clobs = [] && labels = [] then
+                  nil
+              else
+                (text ": "
+                    ++ (docList ~sep:(chr ',' ++ break)
+                          (fun (idopt, c, lv) ->
+                          text(match idopt with
+                                None -> ""
+                              | Some id -> "[" ^ id ^ "] "
+                          ) ++
+                            text ("\"" ^ escape_string c ^ "\" (")
+                              ++ self#pLval () lv
+                              ++ text ")") () outs)))
+              ++
+                (if ins = [] && clobs = [] && labels = [] then
+                  nil
+                else
+                  (text ": "
+                      ++ (docList ~sep:(chr ',' ++ break)
+                            (fun (idopt, c, e) ->
+                              text(match idopt with
+                                    None -> ""
+                                  | Some id -> "[" ^ id ^ "] "
+                              ) ++
+                              text ("\"" ^ escape_string c ^ "\" (")
+                                ++ self#pExp () e
+                                ++ text ")") () ins)))
+                ++
+                (if clobs = [] && labels = [] then nil
+                else
+                  (text ": "
+                      ++ (docList ~sep:(chr ',' ++ break)
+                            (fun c -> text ("\"" ^ escape_string c ^ "\""))
+                            ()
+                            clobs)))
+                ++
+                (if labels = [] then nil
+                else
+                  (text ": "
+                      ++ (docList ~sep:(chr ',' ++ break)
+                            text
+                            ()
+                            (names_of_stmtrefs labels))))
+                ++ unalign)
+          ++ text (")" ^ printInstrTerminator)
 
 
   (*** GLOBALS ***)
@@ -4329,6 +4358,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
     | "aconst", [] -> text "__const__", true
     | "thread", [] -> text "__thread", false
     | "volatile", [] -> text "volatile", false
+    | "goto", [] -> text "goto", false
     | "restrict", [] -> text "__restrict", false
     | "missingproto", [] -> text "/* missing proto */", false
     | "asm", args ->
@@ -4355,7 +4385,6 @@ class defaultCilPrinterClass : cilPrinter = object (self)
     | "arraylen", [a] ->
         (* text "/*[" ++ self#pAttrParam () a ++ text "]*/" *) nil, false
 
-
     | _ -> (* This is the default case *)
         (* Add underscores to the name *)
         let an' =  "__" ^ an ^ "__" in
@@ -5325,16 +5354,6 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
       if lv' != lv || fn' != fn || args' != args
       then Call(Some lv', fn', args', l, el) else i
 
-  | Asm(sl,isvol,outs,ins,clobs,l) ->
-      let outs' = mapNoCopy (fun ((id,s,lv) as pair) ->
-                               let lv' = fLval lv in
-                               if lv' != lv then (id,s,lv') else pair) outs in
-      let ins'  = mapNoCopy (fun ((id,s,e) as pair) ->
-                               let e' = fExp e in
-                               if e' != e then (id,s,e') else pair) ins in
-      if outs' != outs || ins' != ins then
-        Asm(sl,isvol,outs',ins',clobs,l) else i
-
 
 (* visit all nodes in a Cil statement tree in preorder *)
 and visitCilStmt (vis: cilVisitor) (s: stmt) : stmt =
@@ -5397,6 +5416,15 @@ and childrenStmt (toPrepend: instr list ref) : cilVisitor -> stmt -> stmt =
     | Block b ->
         let b' = fBlock b in
         if b' != b then Block b' else s.skind
+    | Asm(sl,isvol,outs,ins,clobs,labels,l) ->
+        let outs' = mapNoCopy (fun ((id,s,lv) as pair) ->
+                                 let lv' = visitCilLval vis lv in
+                                 if lv' != lv then (id,s,lv') else pair) outs in
+        let ins'  = mapNoCopy (fun ((id,s,e) as pair) ->
+                                 let e' = fExp e in
+                                 if e' != e then (id,s,e') else pair) ins in
+        if outs' != outs || ins' != ins then
+          Asm(sl,isvol,outs',ins',clobs,labels,l) else s.skind
   in
   if skind' != s.skind then s.skind <- skind';
   (* Visit the labels *)
@@ -5884,7 +5912,7 @@ let rec peepHole1 (* Process one instruction and possibly replace it *)
       | Switch (e, b, _, _, _) -> peepHole1 doone b.bstmts
       | Loop (b, l, el, _, _) -> peepHole1 doone b.bstmts
       | Block b -> peepHole1 doone b.bstmts
-      | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> ())
+      | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ -> ())
     ss
 
 let rec peepHole2  (* Process two instructions and possibly replace them both *)
@@ -5912,7 +5940,7 @@ let rec peepHole2  (* Process two instructions and possibly replace them both *)
       | Loop (b, l, el, _, _) -> peepHole2 dotwo b.bstmts
       | Block b -> peepHole2 dotwo b.bstmts
 
-      | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> ())
+      | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ -> ())
     ss
 
 
@@ -6005,8 +6033,8 @@ let typeSigAttrs = function
 let dExp: doc -> exp =
   fun d -> Const(CStr(sprint ~width:!lineLength d, No_encoding))
 
-let dInstr: doc -> location -> instr =
-  fun d l -> Asm([], [sprint ~width:!lineLength d], [], [], [], l)
+let dStmt: doc -> location -> stmt =
+  fun d l -> mkStmt (Asm([], [sprint ~width:!lineLength d], [], [], [], [], l))
 
 let dGlobal: doc -> location -> global =
   fun d l -> GAsm(sprint ~width:!lineLength d, l)
@@ -6517,6 +6545,7 @@ and succpred_stmt s fallthrough rlabels =
                 | hd :: tl -> link s hd ;
                     succpred_block b fallthrough rlabels
                 end
+  | Asm _ -> trylink s fallthrough
 
 
 let caseRangeFold (l: label list) =
@@ -6581,7 +6610,7 @@ let rec xform_switch_stmt s break_dest cont_dest = begin
   | Default(l,el) -> Label(freshLabel "switch_default",l,false)
   ) s.labels ;
   match s.skind with
-  | Instr _ | Return _ | Goto _ | ComputedGoto _ -> ()
+  | Instr _ | Return _ | Goto _ | ComputedGoto _ | Asm _ -> ()
   | Break(l) -> begin try
                   s.skind <- Goto(break_dest (),l)
                 with e ->
diff --git a/src/cil.mli b/src/cil.mli
index a2ee2d506..87d74494b 100644
--- a/src/cil.mli
+++ b/src/cil.mli
@@ -1007,35 +1007,6 @@ and stmtkind =
     (** Just a block of statements. Use it as a way to keep some block
        attributes local *)
 
-(** {b Instructions}.
- An instruction {!instr} is a statement that has no local
-(intraprocedural) control flow. It can be either an assignment,
-function call, or an inline assembly instruction. *)
-
-(** Instructions. *)
-and instr =
-  Set        of lval * exp * location * location
-   (** An assignment. The type of the expression is guaranteed to be the same
-      with that of the lvalue.
-      Second location is just for expression when inside condition. *)
-  | VarDecl    of varinfo * location
-   (** "Instruction" in the location where a varinfo was declared.
-       All varinfos for which such a VarDecl instruction exists have
-       vhasdeclinstruction set to true.
-       The motivation for the addition of this instruction was to support VLAs
-       for which declerations can not be pulled up like CIL used to do.
-    *)
-  | Call       of lval option * exp * exp list * location * location
-   (** A function call with the (optional) result placed in an lval. It is
-      possible that the returned type of the function is not identical to
-      that of the lvalue. In that case a cast is printed. The type of the
-      actual arguments are identical to those of the declared formals. The
-      number of arguments is the same as that of the declared formals, except
-      for vararg functions. This construct is also used to encode a call to
-      "__builtin_va_arg". In this case the second argument (which should be a
-      type T) is encoded SizeOf(T).
-      Second location is just for expression when inside condition. *)
-
   | Asm        of attributes * (* Really only const and volatile can appear
                                  here *)
                   string list *         (* templates (CR-separated) *)
@@ -1049,17 +1020,18 @@ and instr =
                   (string option * string * exp) list *
                                         (* inputs with optional names and constraints *)
                   string list *         (* register clobbers *)
+                  stmt ref list *       (* referenced labels *)
                   location
     (** There are for storing inline assembly. They follow the GCC
         specification:
-{v
+  {v
   asm [volatile] ("...template..." "..template.."
                   : "c1" (o1), "c2" (o2), ..., "cN" (oN)
                   : "d1" (i1), "d2" (i2), ..., "dM" (iM)
                   : "r1", "r2", ..., "nL" );
- v}
+  v}
 
-where the parts are
+  where the parts are
 
   - [volatile] (optional): when present, the assembler instruction
     cannot be removed, moved, or otherwise optimized
@@ -1080,24 +1052,53 @@ where the parts are
   - "rk": registers to be regarded as "clobbered" by the instruction;
     "memory" may be specified for arbitrary memory effects
 
-an example (from gcc manual):
-{v
+  an example (from gcc manual):
+  {v
   asm volatile ("movc3 %0,%1,%2"
                 : /* no outputs */
                 : "g" (from), "g" (to), "g" (count)
                 : "r0", "r1", "r2", "r3", "r4", "r5");
- v}
+  v}
 
- Starting with gcc 3.1, the operands may have names:
+  Starting with gcc 3.1, the operands may have names:
 
-{v
+  {v
   asm volatile ("movc3 %[in0],%1,%2"
                 : /* no outputs */
                 : [in0] "g" (from), "g" (to), "g" (count)
                 : "r0", "r1", "r2", "r3", "r4", "r5");
- v}
+  v}
 
-*)
+  *)
+
+(** {b Instructions}.
+ An instruction {!instr} is a statement that has no local
+(intraprocedural) control flow. It can be either an assignment,
+function call, or an inline assembly instruction. *)
+
+(** Instructions. *)
+and instr =
+  Set        of lval * exp * location * location
+   (** An assignment. The type of the expression is guaranteed to be the same
+      with that of the lvalue.
+      Second location is just for expression when inside condition. *)
+  | VarDecl    of varinfo * location
+   (** "Instruction" in the location where a varinfo was declared.
+       All varinfos for which such a VarDecl instruction exists have
+       vhasdeclinstruction set to true.
+       The motivation for the addition of this instruction was to support VLAs
+       for which declerations can not be pulled up like CIL used to do.
+    *)
+  | Call       of lval option * exp * exp list * location * location
+   (** A function call with the (optional) result placed in an lval. It is
+      possible that the returned type of the function is not identical to
+      that of the lvalue. In that case a cast is printed. The type of the
+      actual arguments are identical to those of the declared formals. The
+      number of arguments is the same as that of the declared formals, except
+      for vararg functions. This construct is also used to encode a call to
+      "__builtin_va_arg". In this case the second argument (which should be a
+      type T) is encoded SizeOf(T).
+      Second location is just for expression when inside condition. *)
 
 (** Describes a location in a source file. *)
 and location = {
@@ -1751,10 +1752,7 @@ val compactStmts: stmt list -> stmt list
 (** Returns an empty statement (of kind [Instr]) *)
 val mkEmptyStmt: unit -> stmt
 
-(** A instr to serve as a placeholder *)
-val dummyInstr: instr
-
-(** A statement consisting of just [dummyInstr] *)
+(** A statement to serve as a placeholder *)
 val dummyStmt: stmt
 
 (** Make a while loop. Can contain Break or Continue *)
@@ -2650,8 +2648,8 @@ val get_stmtLoc: stmtkind -> location
 (** Generate an {!exp} to be used in case of errors. *)
 val dExp: Pretty.doc -> exp
 
-(** Generate an {!instr} to be used in case of errors. *)
-val dInstr: Pretty.doc -> location -> instr
+(** Generate an {!stmt} to be used in case of errors. *)
+val dStmt: Pretty.doc -> location -> stmt
 
 (** Generate a {!global} to be used in case of errors. *)
 val dGlobal: Pretty.doc -> location -> global
diff --git a/src/dataflow.ml b/src/dataflow.ml
index cd19e3f34..eb3c3e792 100644
--- a/src/dataflow.ml
+++ b/src/dataflow.ml
@@ -221,7 +221,7 @@ module ForwardsDataFlow =
                 List.fold_left handleInstruction curr il
 
             | Goto _ | ComputedGoto _ | Break _ | Continue _ | If _
-            | Switch _ | Loop _ | Return _ | Block _ -> curr
+            | Switch _ | Loop _ | Return _ | Block _ | Asm _ -> curr
           in
           currentLoc := get_stmtLoc s.skind;
 
diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml
index 76afb839b..96af81fbe 100644
--- a/src/ext/liveness/usedef.ml
+++ b/src/ext/liveness/usedef.ml
@@ -150,12 +150,6 @@ class useDefVisitorClass : cilVisitor = object (self)
         E.s (bug "bad call to %s" vi.vname)
     | Call (lvo, f, args, _, _) ->
         doCall f lvo args
-    | Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) ->
-	match lv with (Var v, off) ->
-	  if s.[0] = '+' then
-	    varUsed := VS.add v !varUsed;
-	| _ -> ()) slvl;
-	DoChildren
     | _ -> DoChildren
 
 end
@@ -200,6 +194,11 @@ let computeUseDefStmtKind ?(acc_used=VS.empty)
     | Instr il ->
         List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il
     | Block _ -> ()
+    | Asm (_, _, outs, ins, _, _, _) ->
+        List.iter (fun (_, _, exp) -> match exp with
+          | Lval(Var v, _) -> varUsed := VS.add v !varUsed
+          | _ -> ()
+        ) ins;
   in
   !varUsed, !varDefs
 
@@ -242,6 +241,11 @@ let rec computeDeepUseDefStmtKind ?(acc_used=VS.empty)
       List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il;
       !varUsed, !varDefs
   | Block b -> handle_block b
+  | Asm (a, b, c, d, e, f, g) -> 
+      computeUseDefStmtKind 
+        ~acc_used:!varUsed
+        ~acc_defs:!varDefs
+        (Asm (a, b, c, d, e, f, g))
 
 let computeUseLocalTypes ?(acc_used=VS.empty)
                          (fd : fundec)
diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml
index 2e8dffd6e..ca049367a 100644
--- a/src/ext/pta/ptranal.ml
+++ b/src/ext/pta/ptranal.ml
@@ -298,7 +298,6 @@ let analyze_instr (i : instr ) : unit =
                   Some r -> A.assign_ret site (analyze_lval r) fnres
                 | None -> ()
             end
-    | Asm _ -> ()
     | VarDecl _ -> ()
 
 let rec analyze_stmt (s : stmt ) : unit =
@@ -328,6 +327,7 @@ let rec analyze_stmt (s : stmt ) : unit =
     | Block b -> analyze_block b
     | Break l -> ()
     | Continue l -> ()
+    | Asm _ -> ()
 
 
 and analyze_block (b : block ) : unit =
diff --git a/src/ext/syntacticsearch/funcVar.ml b/src/ext/syntacticsearch/funcVar.ml
index 857d0b042..ffd9af22c 100644
--- a/src/ext/syntacticsearch/funcVar.ml
+++ b/src/ext/syntacticsearch/funcVar.ml
@@ -159,8 +159,6 @@ let rec search_instr_list_for_var list name varid includeCallTmp =
       search_expression exp name loc varid includeCallTmp
       @ search_expression_list exp_list name loc varid includeCallTmp
       @ search_instr_list_for_var xs name varid includeCallTmp
-  (* Should I consider Asm too? *)
-  | _ :: xs -> search_instr_list_for_var xs name varid includeCallTmp
   | [] -> []
 
 (* Finds a variable in a list of statements *)
diff --git a/src/ext/zrapp/availexps.ml b/src/ext/zrapp/availexps.ml
index e9983e2cb..48dc8a740 100644
--- a/src/ext/zrapp/availexps.ml
+++ b/src/ext/zrapp/availexps.ml
@@ -243,11 +243,6 @@ let eh_handle_inst i eh =
       (eh_kill_mem eh;
        eh_kill_addrof_or_global eh;
        eh)
-  | Asm(_,_,_,_,_,_) ->
-      let _,d = UD.computeUseDefInstr i in
-      (UD.VS.iter (fun vi ->
-	eh_kill_vi eh vi) d;
-       eh)
   | VarDecl _ ->   raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexps, to make availexps work for programs without VLA *)
                                                    (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this.  *)
 
diff --git a/src/ext/zrapp/availexpslv.ml b/src/ext/zrapp/availexpslv.ml
index 321b9f656..8b42eb1c1 100644
--- a/src/ext/zrapp/availexpslv.ml
+++ b/src/ext/zrapp/availexpslv.ml
@@ -305,12 +305,6 @@ let lvh_handle_inst i lvh =
       end;
       lvh
   end
-  | Asm(_,_,_,_,_,_) -> begin
-      let _,d = UD.computeUseDefInstr i in
-      UD.VS.iter (fun vi ->
-	lvh_kill_vi lvh vi) d;
-      lvh
-  end
   | VarDecl _ ->   raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexpslv, to make availexpslv work for programs without VLA *)
                                                    (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this.  *)
 
diff --git a/src/ext/zrapp/deadcodeelim.ml b/src/ext/zrapp/deadcodeelim.ml
index f1135fd8d..50ab8f5d7 100644
--- a/src/ext/zrapp/deadcodeelim.ml
+++ b/src/ext/zrapp/deadcodeelim.ml
@@ -102,11 +102,6 @@ class usedDefsCollectorClass = object(self)
 
   method! vinst i =
     let handle_inst iosh i = match i with
-    | Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) ->
-	match lv with (Var v, off) ->
-	  if s.[0] = '+' then
-	    self#add_defids iosh (Lval(Var v, off)) (UD.VS.singleton v)
-	| _ -> ()) slvl
     | Call(_,ce,el,_,_) when not (!callHasNoSideEffects i) ->
 	List.iter (fun e ->
 	  let u = UD.computeUseExp e in
diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml
index 8a8a2a028..4a953bdd6 100644
--- a/src/ext/zrapp/reachingdefs.ml
+++ b/src/ext/zrapp/reachingdefs.ml
@@ -270,8 +270,6 @@ let getDefRhs didstmh stmdat defId =
 		Set((Var vi',NoOffset),_,_,_) -> vi'.vid = vid (* _ -> NoOffset *)
 	      | Call(Some(Var vi',NoOffset),_,_,_,_) -> vi'.vid = vid (* _ -> NoOffset *)
 	      | Call(None,_,_,_,_) -> false
-	      | Asm(_,_,sll,_,_,_) -> List.exists
-		    (function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll
 	      | _ -> false)
 	  | None -> false) iihl in
 	(match i with
@@ -284,7 +282,6 @@ let getDefRhs didstmh stmdat defId =
 	| Call(lvo,e,el,_,_) ->
 	    (IH.add rhsHtbl defId (Some(RDCall(i),stm.sid,iosh_in));
 	     Some(RDCall(i), stm.sid, iosh_in))
-	| Asm(a,sl,slvl,sel,sl',_) -> None
   | VarDecl _ -> None
   ) (* ? *)
 	with Not_found ->
diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml
index dad6dce77..3809bd821 100644
--- a/src/ext/zrapp/rmciltmps.ml
+++ b/src/ext/zrapp/rmciltmps.ml
@@ -994,16 +994,6 @@ class unusedRemoverClass : cilVisitor = object(self)
 	  (match IH.find iioh vi.vid with
 	    None -> true | Some _ -> false)
       end
-      | Asm(_,_,slvlst,_,_,_) -> begin
-	  (* make sure the outputs are in the locals list *)
-	  List.iter (fun (_,s,lv) ->
-	    match lv with (Var vi,_) ->
-	      if List.mem vi cur_func.slocals
-	      then ()
-	      else cur_func.slocals <- vi::cur_func.slocals
-	    |_ -> ()) slvlst;
-	  true
-      end
       | _ -> true
     in
 
diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml
index d13025b53..12927ce9a 100644
--- a/src/frontc/cabs.ml
+++ b/src/frontc/cabs.ml
@@ -209,7 +209,8 @@ and block =
 and asm_details =
     { aoutputs: (string option * string * expression) list; (* optional name, constraints and expressions for outputs *)
       ainputs: (string option * string * expression) list; (* optional name, constraints and expressions for inputs *)
-      aclobbers: string list (* clobbered registers *)
+      aclobbers: string list; (* clobbered registers *)
+      alabels: string list; (* referenced labels *)
     }
 
 and statement =
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index 34e0c6f0d..8b9090668 100644
--- a/src/frontc/cabs2cil.ml
+++ b/src/frontc/cabs2cil.ml
@@ -843,7 +843,6 @@ module BlockChunk =
         | Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc)
         | VarDecl (v, loc) -> VarDecl (v, doLoc loc)
         | Call (l, f, a, loc, eloc) -> Call (l, f, a, doLoc loc, doLoc eloc)
-        | Asm (a, b, c, d, e, loc) -> Asm (a, b, c, d, e, doLoc loc)
 
       (** Change all stmt and instr locs to synthetic, except the first one.
           Expressions/initializers that expand to multiple instructions cannot have intermediate locations referenced. *)
@@ -881,6 +880,7 @@ module BlockChunk =
             | Block b ->
               doBlock ~first b;
               s.skind
+            | Asm (a, b, c, d, e, l, loc) -> Asm (a, b, c, d, e, l, doLoc loc)
         and doBlock ~first b =
           doStmts ~first b.bstmts
         and doStmts ~first = function
@@ -919,6 +919,7 @@ module BlockChunk =
             | Block b ->
               doBlock b;
               s.skind
+            | Asm (a, b, c, d, e, l, loc) -> Asm (a, b, c, d, e, l, doLoc loc)
         and doBlock b =
           doStmts b.bstmts
         and doStmts = function
@@ -4971,7 +4972,7 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
   with e when continueOnError -> begin
     (*ignore (E.log "error in doExp (%s)" (Printexc.to_string e));*)
     E.hadErrors := true;
-    (i2c (dInstr (dprintf "booo_exp(%t)" d_thisloc) !currentLoc),
+    (s2c (dStmt (dprintf "booo_exp(%t)" d_thisloc) !currentLoc),
      integer 0, intType)
   end
 
@@ -6370,7 +6371,6 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function
                 else if hasAttribute "noreturn" e.vattr then false
                 else true
             | Call _ -> true
-            | Asm _ -> true
             | VarDecl _ -> true
             in
             let rec stmtFallsThrough (s: stmt) : bool =
@@ -6402,6 +6402,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function
                   (* A loop falls through if it can break. *)
                   blockCanBreak b
               | Block b -> blockFallsThrough b
+              | Asm _ -> true
             and blockFallsThrough b =
               let rec fall = function
                   [] -> true
@@ -6439,7 +6440,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function
             (* will we leave this statement or block with a break command? *)
             and stmtCanBreak (s: stmt) : bool =
               match s.skind with
-                Instr _ | Return _ | Continue _ | Goto _ | ComputedGoto _ -> false
+                Instr _ | Return _ | Continue _ | Goto _ | ComputedGoto _ | Asm _ -> false
               | Break _ -> true
               | If (_, b1, b2, _, _) ->
                   blockCanBreak b1 || blockCanBreak b2
@@ -6915,7 +6916,7 @@ and doStatement (s : A.statement) : chunk =
         currentLoc := loc';
         currentExpLoc := loc'; (* for argument doExp below *)
         let stmts : chunk ref = ref empty in
-	let (tmpls', outs', ins', clobs') =
+	let (tmpls', outs', ins', clobs', labels') =
 	  match details with
 	  | None ->
 	      let tmpls' =
@@ -6923,8 +6924,8 @@ and doStatement (s : A.statement) : chunk =
 		      let escape = Str.global_replace pattern "%%" in
 		      Util.list_map escape tmpls
 	      in
-	      (tmpls', [], [], [])
-	  | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } ->
+              (tmpls', [], [], [], [])
+          | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; alabels = labels } ->
               let outs' =
 		Util.list_map
 		  (fun (id, c, e) ->
@@ -6947,10 +6948,18 @@ and doStatement (s : A.statement) : chunk =
 		    (id, c, e'))
 		  ins
               in
-	      (tmpls, outs', ins', clobs)
+              let labels' =
+                Util.list_map (fun lname -> begin
+                  let lref = ref dummyStmt in
+                  addGoto lname lref;
+                  lref
+                end)
+                labels
+              in
+	      (tmpls, outs', ins', clobs, labels')
 	in
         !stmts @@
-        (i2c (Asm(attr', tmpls', outs', ins', clobs', loc')))
+        s2c (mkStmt (Asm(attr', tmpls', outs', ins', clobs', labels', loc')))
 
   with e when continueOnError -> begin
     (ignore (E.log "Error in doStatement (%s)\n" (Printexc.to_string e)));
diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml
index f6344874c..49e168e43 100644
--- a/src/frontc/cabsvisit.ml
+++ b/src/frontc/cabsvisit.ml
@@ -434,13 +434,13 @@ and childrenStatement vis s =
       in
       let details' = match details with
       | None -> details
-      | Some { aoutputs = outl; ainputs = inl; aclobbers = clobs } ->
+      | Some { aoutputs = outl; ainputs = inl; aclobbers = clobs; alabels = labels } ->
 	  let outl' = mapNoCopy childrenIdentStringExp outl in
 	  let inl' = mapNoCopy childrenIdentStringExp inl in
 	  if outl' == outl && inl' == inl then
 	    details
 	  else
-	    Some { aoutputs = outl'; ainputs = inl'; aclobbers = clobs }
+            Some { aoutputs = outl'; ainputs = inl'; aclobbers = clobs; alabels = labels }
       in
       if details' != details then
         ASM (sl, b, details', l) else s
diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly
index 17fa5a34d..1868277ed 100644
--- a/src/frontc/cparser.mly
+++ b/src/frontc/cparser.mly
@@ -244,6 +244,26 @@ let transformOffsetOf (speclist, dtype) member =
       queue;
     Buffer.contents buffer
 
+  (* this makes sure that the labels are only allowed when goto annotation was provided *)
+  let checkAsm asm =
+    let labels_no_goto = "labels provided in inline asm without goto attribute" in
+    let goto_no_labels = "expected non-empty labels list in asm goto" in
+    (match asm with
+    | ASM (attrs, _, details, _) ->
+      (match details, (List.assoc_opt "goto" attrs) with
+      | None, Some _ ->
+        parse_error goto_no_labels;
+        raise Parsing.Parse_error
+      | Some details, Some _ when details.alabels = [] ->
+        parse_error goto_no_labels;
+        raise Parsing.Parse_error
+      | Some details, None when details.alabels <> [] ->
+        parse_error labels_no_goto;
+        raise Parsing.Parse_error
+      | _, _ -> ())
+    | _ -> failwith "called checkAsm on non-ASM variant");
+    asm
+
 %}
 
 %token <string * Cabs.cabsloc> IDENT
@@ -982,7 +1002,7 @@ statement_no_null:
 |   GOTO STAR comma_expression SEMICOLON
                                  { COMPGOTO (smooth_expression (fst $3), joinLoc $1 $4) }
 |   ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON
-                        { ASM ($2, $4, $5, joinLoc $1 $7) }
+                        { checkAsm (ASM ($2, $4, $5, joinLoc $1 $7)) }
 |   error location   SEMICOLON   { (NOP $2)}
 ;
 
@@ -1646,6 +1666,7 @@ asmattr:
 |    VOLATILE  asmattr                  { ("volatile", []) :: $2 }
 |    CONST asmattr                      { ("const", []) :: $2 }
 |    INLINE asmattr                     { ("inline", []) :: $2 }
+|    GOTO asmattr                       { ("goto", []) :: $2 }
 ;
 asmtemplate:
     one_string_constant                          { [$1] }
@@ -1654,8 +1675,11 @@ asmtemplate:
 asmoutputs:
   /* empty */           { None }
 | COLON asmoperands asminputs
-                        { let (ins, clobs) = $3 in
-                          Some {aoutputs = $2; ainputs = ins; aclobbers = clobs} }
+                        { let (ins, clobs, labels) = $3 in
+                          Some {aoutputs = $2;
+                                ainputs = ins;
+                                aclobbers = clobs;
+                                alabels = labels} }
 ;
 asmoperands:
      /* empty */                        { [] }
@@ -1672,9 +1696,9 @@ asmoperand:
 ;
 
 asminputs:
-  /* empty */                { ([], []) }
+    /* empty */                { ([], [], []) }
 | COLON asmoperands asmclobber
-                        { ($2, $3) }
+                        { ($2, fst $3, snd $3) }
 ;
 asmopname:
     /* empty */                         { None }
@@ -1682,16 +1706,23 @@ asmopname:
 ;
 
 asmclobber:
-    /* empty */                         { [] }
-| COLON asmclobberlst                   { $2 }
+    /* empty */                         { ([], []) }
+| COLON asmclobberlst asmlabellst       { ($2, $3) }
 ;
 asmclobberlst:
     /* empty */                         { [] }
-| asmclobberlst_ne                       { $1 }
+| asmclobberlst_ne                      { $1 }
 ;
 asmclobberlst_ne:
    one_string_constant                           { [$1] }
 |  one_string_constant COMMA asmclobberlst_ne    { $1 :: $3 }
 ;
+asmlabellst:
+    /* empty */                         { [] }
+| COLON asmlabellst_ne                  { $2 }
+;
+asmlabellst_ne:
+  IDENT                               { [fst $1] }
+| IDENT COMMA asmlabellst_ne          { (fst $1) :: $3 }
 
 %%
diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml
index 07a75ada5..704c62602 100644
--- a/src/frontc/cprint.ml
+++ b/src/frontc/cprint.ml
@@ -715,22 +715,25 @@ and print_statement stat =
         print_attributes attrs;
         print "(";
         print_list (fun () -> new_line()) print_string tlist; (* templates *)
-	begin
-	  match details with
-	  | None -> ()
-	  | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } ->
+        begin
+          match details with
+          | None -> ()
+          | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; alabels = labels } ->
               print ":"; space ();
               print_commas false print_asm_operand outs;
-              if ins <> [] || clobs <> [] then begin
-		print ":"; space ();
-		print_commas false print_asm_operand ins;
-		if clobs <> [] then begin
-		  print ":"; space ();
-		  print_commas false print_string clobs
-		end;
-              end
-	end;
-        print ");"
+              if ins <> [] || clobs <> [] || labels <> [] then begin
+                print ":"; space ();
+                print_commas false print_asm_operand ins;
+                if clobs <> [] || labels <> [] then begin
+                  print ":"; space ();
+                  print_commas false print_string clobs;
+                  if labels <> [] then 
+                    print ":"; space ();
+                    print_commas false print labels
+                end;
+              end;
+        end;
+        print ");";
       end;
       new_line ()
 
diff --git a/src/mergecil.ml b/src/mergecil.ml
index 028649c7b..aa20ad9ff 100644
--- a/src/mergecil.ml
+++ b/src/mergecil.ml
@@ -1165,6 +1165,7 @@
      | Switch (_, b, _, _, _) -> 43 + (47 * stmtListSum b.bstmts) (* don't look at stmt list b/c is not part of tree *)
      | Loop (b, _, _, _, _) -> 49 + (53 * stmtListSum b.bstmts)
      | Block b -> 59 + (61 * stmtListSum b.bstmts)
+     | Asm _ -> 71
    in
 
    (* disabled 2nd and 3rd measure because they appear to get different
diff --git a/src/rmUnused.ml b/src/rmUnused.ml
index 834e1b9db..8897b6311 100644
--- a/src/rmUnused.ml
+++ b/src/rmUnused.ml
@@ -642,7 +642,14 @@ class markUsedLabels (labelMap: (string, unit) H.t) = object
         (* Mark it as used *)
         H.replace labelMap ln ();
         DoChildren
-
+    | Asm (_, _, _, _, _, labels, _) ->
+        List.iter (fun dest ->
+          let (ln, _, _), _ = labelsToKeep !dest.labels in
+          if ln = "" then
+            E.s (E.bug "rmUnused: destination of statement does not have labels");
+          H.replace labelMap ln ();
+        ) labels;
+        DoChildren
     | _ -> DoChildren
 
   method! vexpr e = match e with
diff --git a/test/small1/asm_goto1.c b/test/small1/asm_goto1.c
new file mode 100644
index 000000000..071d7db64
--- /dev/null
+++ b/test/small1/asm_goto1.c
@@ -0,0 +1,6 @@
+#include "testharness.h"
+
+int main() {
+  asm goto ("nop");
+  E(1);
+}
diff --git a/test/small1/asm_goto2.c b/test/small1/asm_goto2.c
new file mode 100644
index 000000000..dc1e1ada0
--- /dev/null
+++ b/test/small1/asm_goto2.c
@@ -0,0 +1,6 @@
+#include "testharness.h"
+
+void code() {
+  asm goto ("nop" : );
+  E(1);
+}
diff --git a/test/small1/asm_goto3.c b/test/small1/asm_goto3.c
new file mode 100644
index 000000000..a5d6aa433
--- /dev/null
+++ b/test/small1/asm_goto3.c
@@ -0,0 +1,9 @@
+#include "testharness.h"
+
+int main(void) {
+start:
+  asm goto ("nop" : : : : start, exit);
+exit:
+  SUCCESS;
+}
+
diff --git a/test/small1/asm_goto4.c b/test/small1/asm_goto4.c
new file mode 100644
index 000000000..290d1689c
--- /dev/null
+++ b/test/small1/asm_goto4.c
@@ -0,0 +1,10 @@
+#include "testharness.h"
+
+void code() {
+start:
+  asm("nop" : : : : start, exit);
+exit:
+  E(1);
+}
+
+
diff --git a/test/small1/asm_goto5.c b/test/small1/asm_goto5.c
new file mode 100644
index 000000000..208119256
--- /dev/null
+++ b/test/small1/asm_goto5.c
@@ -0,0 +1,8 @@
+#include "testharness.h"
+
+void code() {
+  asm goto ("nop" : : : : start, exit);
+  E(1);
+}
+
+
diff --git a/test/small1/asm_goto6.c b/test/small1/asm_goto6.c
new file mode 100644
index 000000000..6d9109993
--- /dev/null
+++ b/test/small1/asm_goto6.c
@@ -0,0 +1,9 @@
+#include "testharness.h"
+
+void code() {
+  asm goto ("nop" : : : );
+  E(1);
+}
+
+
+
diff --git a/test/testcil.pl b/test/testcil.pl
index a33e9af7a..78e0924a0 100644
--- a/test/testcil.pl
+++ b/test/testcil.pl
@@ -180,6 +180,12 @@ sub addToGroup {
 addTest("test/asm4 _GNUCC=1");
 addTest("test/asm_emptyclobberallowed _GNUCC=1");
 addTest("testobj/asm5 _GNUCC=1");
+addTestFail("test/asm_goto1", "expected non-empty labels list in asm goto");
+addTestFail("test/asm_goto2", "expected non-empty labels list in asm goto");
+addTest("test/asm_goto3");
+addTestFail("test/asm_goto4", "labels provided in inline asm without goto attribute");
+addTestFail("test/asm_goto5", "Error: Label start not found");
+addTestFail("test/asm_goto6", "expected non-empty labels list in asm goto");
 
 addTest("testrun/offsetof");
 addTest("testrun/offsetof1");