diff --git a/src/cil.ml b/src/cil.ml
index 288c49ce4..e8fea5787 100755
--- a/src/cil.ml
+++ b/src/cil.ml
@@ -839,7 +839,7 @@ and instr =
   | Asm        of attributes * (* Really only const and volatile can appear
                                * here *)
                   string list *         (* templates (CR-separated) *)
-                  (string option * string * lval) list *
+                  ((string option * string * lval) list *
                                           (* outputs must be lvals with
                                            * optional names and constraints.
                                            * I would like these
@@ -849,6 +849,7 @@ and instr =
                   (string option * string * exp) list *
                                         (* inputs with optional names and constraints *)
                   string list *         (* register clobbers *)
+                  string list) option * (* goto locations *)
                   location
         (** An inline assembly instruction. The arguments are (1) a list of
             attributes (only const and volatile can appear here and only for
@@ -1113,7 +1114,7 @@ let get_instrLoc (inst : instr) =
   match inst with
       Set(_, _, loc, _) -> loc
     | Call(_, _, _, loc, _) -> loc
-    | Asm(_, _, _, _, _, loc) -> loc
+    | Asm(_, _, _, loc) -> loc
     | VarDecl(_,loc) -> loc
 let get_globalLoc (g : global) =
   match g with
@@ -1341,7 +1342,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 dummyInstr = (Asm([], ["dummy statement!!"], None, lu))
 let dummyStmt =  mkStmt (Instr [dummyInstr])
 
 let compactStmts (b: stmt list) : stmt list =
@@ -3673,7 +3674,8 @@ class defaultCilPrinterClass : cilPrinter = object (self)
              ++ unalign)
         ++ text (")" ^ printInstrTerminator)
 
-    | Asm(attrs, tmpls, outs, ins, clobs, l) ->
+    | Asm(attrs, tmpls, details, l) ->
+        let (outs, ins, clobs, gotos) = Option.value ~default:([],[],[],[]) details in
         self#pLineDirective l
           ++ text ("__asm__ ")
           ++ self#pAttrs () attrs
@@ -3683,7 +3685,9 @@ class defaultCilPrinterClass : cilPrinter = object (self)
                       (fun x -> text ("\"" ^ escape_string x ^ "\""))
                       () tmpls)
                 ++
-                (if outs = [] && ins = [] && clobs = [] then
+                (if details = None then 
+                    nil
+              else if outs = [] && ins = [] && clobs = [] && gotos = [] then
                   chr ':'
               else
                 (text ": "
@@ -3697,7 +3701,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
                               ++ self#pLval () lv
                               ++ text ")") () outs)))
               ++
-                (if ins = [] && clobs = [] then
+                (if ins = [] && clobs = [] && gotos = [] then
                   nil
                 else
                   (text ": "
@@ -3711,13 +3715,21 @@ class defaultCilPrinterClass : cilPrinter = object (self)
                                 ++ self#pExp () e
                                 ++ text ")") () ins)))
                 ++
-                (if clobs = [] then nil
+                (if clobs = [] && gotos = [] then nil
                 else
                   (text ": "
                       ++ (docList ~sep:(chr ',' ++ break)
                             (fun c -> text ("\"" ^ escape_string c ^ "\""))
                             ()
                             clobs)))
+                ++
+                (if gotos = [] then nil
+                else
+                  (text ": "
+                      ++ (docList ~sep:(chr ',' ++ break)
+                            text
+                            ()
+                            gotos)))
                 ++ unalign)
           ++ text (")" ^ printInstrTerminator)
 
@@ -5290,7 +5302,7 @@ 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) ->
+  | Asm(sl,isvol,Some(outs,ins,clobs,gotos),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
@@ -5298,7 +5310,8 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
                                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
+        Asm(sl,isvol,Some(outs',ins',clobs,gotos),l) else i
+  | Asm _ -> i
 
 
 (* visit all nodes in a Cil statement tree in preorder *)
@@ -5971,7 +5984,7 @@ 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)
+  fun d l -> Asm([], [sprint ~width:!lineLength d], None, l)
 
 let dGlobal: doc -> location -> global =
   fun d l -> GAsm(sprint ~width:!lineLength d, l)
diff --git a/src/cil.mli b/src/cil.mli
index 57d0be532..13dd2da19 100644
--- a/src/cil.mli
+++ b/src/cil.mli
@@ -1034,7 +1034,7 @@ and instr =
   | Asm        of attributes * (* Really only const and volatile can appear
                                * here *)
                   string list *         (* templates (CR-separated) *)
-                  (string option * string * lval) list *
+                  ((string option * string * lval) list *
                                           (* outputs must be lvals with
                                            * optional names and constraints.
                                            * I would like these
@@ -1044,6 +1044,7 @@ and instr =
                   (string option * string * exp) list *
                                         (* inputs with optional names and constraints *)
                   string list *         (* register clobbers *)
+                  string list) option * (* goto locations *)
                   location
     (** There are for storing inline assembly. They follow the GCC
       * specification:
diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml
index f313e11e9..e139f5bf5 100644
--- a/src/ext/liveness/usedef.ml
+++ b/src/ext/liveness/usedef.ml
@@ -151,7 +151,7 @@ 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) ->
+    | Asm(_,_,Some(slvl,_,_,_),_) -> List.iter (fun (_,s,lv) ->
 	match lv with (Var v, off) ->
 	  if s.[0] = '+' then
 	    varUsed := VS.add v !varUsed;
diff --git a/src/ext/zrapp/availexps.ml b/src/ext/zrapp/availexps.ml
index 2763989c8..0ab0e1142 100644
--- a/src/ext/zrapp/availexps.ml
+++ b/src/ext/zrapp/availexps.ml
@@ -243,7 +243,7 @@ let eh_handle_inst i eh =
       (eh_kill_mem eh;
        eh_kill_addrof_or_global eh;
        eh)
-  | Asm(_,_,_,_,_,_) ->
+  | Asm(_,_,_,_) ->
       let _,d = UD.computeUseDefInstr i in
       (UD.VS.iter (fun vi ->
 	eh_kill_vi eh vi) d;
diff --git a/src/ext/zrapp/availexpslv.ml b/src/ext/zrapp/availexpslv.ml
index 5901403a3..c7faed700 100644
--- a/src/ext/zrapp/availexpslv.ml
+++ b/src/ext/zrapp/availexpslv.ml
@@ -305,7 +305,7 @@ let lvh_handle_inst i lvh =
       end;
       lvh
   end
-  | Asm(_,_,_,_,_,_) -> begin
+  | Asm(_,_,_,_) -> begin
       let _,d = UD.computeUseDefInstr i in
       UD.VS.iter (fun vi ->
 	lvh_kill_vi lvh vi) d;
diff --git a/src/ext/zrapp/deadcodeelim.ml b/src/ext/zrapp/deadcodeelim.ml
index d1e754b08..1dbbaa9ea 100644
--- a/src/ext/zrapp/deadcodeelim.ml
+++ b/src/ext/zrapp/deadcodeelim.ml
@@ -102,7 +102,7 @@ class usedDefsCollectorClass = object(self)
 
   method! vinst i =
     let handle_inst iosh i = match i with
-    | Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) ->
+    | Asm(_,_,Some(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)
diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml
index 23b4b0d14..8cde80533 100644
--- a/src/ext/zrapp/reachingdefs.ml
+++ b/src/ext/zrapp/reachingdefs.ml
@@ -270,7 +270,7 @@ 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
+	      | Asm(_,_,Some(sll,_,_,_),_) -> List.exists
 		    (function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll
 	      | _ -> false)
 	  | None -> false) iihl in
@@ -284,7 +284,7 @@ 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
+	| Asm(a,sl,_,_) -> None
   | VarDecl _ -> None
   ) (* ? *)
 	with Not_found ->
diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml
index 4af909fc6..6a2365ac9 100644
--- a/src/ext/zrapp/rmciltmps.ml
+++ b/src/ext/zrapp/rmciltmps.ml
@@ -994,7 +994,7 @@ class unusedRemoverClass : cilVisitor = object(self)
 	  (match IH.find iioh vi.vid with
 	    None -> true | Some _ -> false)
       end
-      | Asm(_,_,slvlst,_,_,_) -> begin
+      | Asm(_,_,Some(slvlst,_,_,_),_) -> begin
 	  (* make sure the outputs are in the locals list *)
 	  List.iter (fun (_,s,lv) ->
 	    match lv with (Var vi,_) ->
diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml
index a46cb2e7c..e6489a084 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 *)
+      agotos: string list; (* asm goto locations *)
     }
 
 and statement =
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index c60c29727..9eb880be7 100644
--- a/src/frontc/cabs2cil.ml
+++ b/src/frontc/cabs2cil.ml
@@ -6833,7 +6833,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', details) =
 	  match details with
 	  | None ->
 	      let tmpls' =
@@ -6841,8 +6841,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', None)
+	  | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotos = gotos } ->
               let outs' =
 		Util.list_map
 		  (fun (id, c, e) ->
@@ -6865,10 +6865,10 @@ and doStatement (s : A.statement) : chunk =
 		    (id, c, e'))
 		  ins
               in
-	      (tmpls, outs', ins', clobs)
+	      (tmpls, Some (outs', ins', clobs, gotos))
 	in
         !stmts @@
-        (i2c (Asm(attr', tmpls', outs', ins', clobs', loc')))
+        (i2c (Asm(attr', tmpls', details, 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 a2dd69d1b..528927d55 100644
--- a/src/frontc/cabsvisit.ml
+++ b/src/frontc/cabsvisit.ml
@@ -440,13 +440,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; agotos = gotos } ->
 	  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; agotos = gotos }
       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 7e76f54c0..7784fffa9 100644
--- a/src/frontc/cparser.mly
+++ b/src/frontc/cparser.mly
@@ -1644,6 +1644,7 @@ asmattr:
      /* empty */                        { [] }
 |    VOLATILE  asmattr                  { ("volatile", []) :: $2 }
 |    CONST asmattr                      { ("const", []) :: $2 }
+|    GOTO asmattr                       { ("goto", []) :: $2 }
 ;
 asmtemplate:
     one_string_constant                          { [$1] }
@@ -1652,8 +1653,8 @@ asmtemplate:
 asmoutputs:
   /* empty */           { None }
 | COLON asmoperands asminputs
-                        { let (ins, clobs) = $3 in
-                          Some {aoutputs = $2; ainputs = ins; aclobbers = clobs} }
+                        { let (ins, (clobs, gotos)) = $3 in
+                          Some {aoutputs = $2; ainputs = ins; aclobbers = clobs; agotos = gotos} }
 ;
 asmoperands:
      /* empty */                        { [] }
@@ -1670,7 +1671,7 @@ asmoperand:
 ;
 
 asminputs:
-  /* empty */                { ([], []) }
+  /* empty */                { ([], ([], [])) }
 | COLON asmoperands asmclobber
                         { ($2, $3) }
 ;
@@ -1680,8 +1681,8 @@ asmopname:
 ;
 
 asmclobber:
-    /* empty */                         { [] }
-| COLON asmcloberlst                    { $2 }
+    /* empty */                         { ([], []) }
+| COLON asmcloberlst asmgoto            { ($2, $3) }
 ;
 asmcloberlst:
     /* empty */                         { [] }
@@ -1692,4 +1693,17 @@ asmcloberlst_ne:
 |  one_string_constant COMMA asmcloberlst_ne     { $1 :: $3 }
 ;
 
+asmgoto:
+    /* empty */                         { [] }
+| COLON asmgotolst                      { $2 }
+;
+asmgotolst:
+    /* empty */                         { [] }
+| asmgotolst_ne                         { $1 }
+;
+asmgotolst_ne:
+   IDENT                                { [ fst $1 ] }
+|  IDENT COMMA asmgotolst_ne            { ( fst $1 ) :: $3 }
+;
+
 %%
diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml
index fae86f0b4..3e9a31ace 100644
--- a/src/frontc/cprint.ml
+++ b/src/frontc/cprint.ml
@@ -718,7 +718,7 @@ and print_statement stat =
 	begin
 	  match details with
 	  | None -> ()
-	  | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } ->
+	  | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotos = gotos } ->
               print ":"; space ();
               print_commas false print_asm_operand outs;
               if ins <> [] || clobs <> [] then begin
@@ -728,6 +728,10 @@ and print_statement stat =
 		  print ":"; space ();
 		  print_commas false print_string clobs
 		end;
+		if gotos <> [] then begin
+		  print ":"; space ();
+		  print_commas false print gotos
+		end;
               end
 	end;
         print ");"