From 24d806cf8f3659f63e95ee3545dee2f98369cc39 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Thu, 1 Feb 2024 14:27:53 +0100 Subject: [PATCH] commiting to test in goblint --- src/cil.ml | 2 +- src/frontc/cparser.mly | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 8a7e037a6..b966cddf3 100755 --- a/src/cil.ml +++ b/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 diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 0ee071f01..1868277ed 100644 --- a/src/frontc/cparser.mly +++ b/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");