commiting to test in goblint

src/cil.ml

@@ -838,7 +838,7 @@ and stmtkind =
   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, (5) location information, and (6) the labels list for asm goto *)
+  registers, (6) the labels list for asm goto, and (7) location information *)
 
 
 (** Instructions. They may cause effects directly but may not have control

src/frontc/cparser.mly

@@ -246,17 +246,19 @@ let transformOffsetOf (speclist, dtype) member =
 
   (* 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 "expected non-empty labels list in asm goto";
+        parse_error goto_no_labels;
         raise Parsing.Parse_error
       | Some details, Some _ when details.alabels = [] ->
-        parse_error "expected non-empty labels list in asm goto";
+        parse_error goto_no_labels;
         raise Parsing.Parse_error
       | Some details, None when details.alabels <> [] ->
-        parse_error "labels provided in inline asm without goto attribute";
+        parse_error labels_no_goto;
         raise Parsing.Parse_error
       | _, _ -> ())
     | _ -> failwith "called checkAsm on non-ASM variant");