diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 29da754e5d2dcedfd17436d73e428c2f74a49467..ed1934a750d6bc7465fa4ad1f8aa9dce0e3aa9e4 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -969,11 +969,11 @@ statement: } | ASM GOTO asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON { let loc = Cil_datatype.Location.of_lexing_loc (Parsing.symbol_start_pos (), Parsing.symbol_end_pos ()) in - no_ghost [ASM ($3, $5, $6, loc)] + no_ghost [ASM ($3, mk_asm_templates $5, $6, loc)] } | ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON { let loc = Cil_datatype.Location.of_lexing_loc (Parsing.symbol_start_pos (), Parsing.symbol_end_pos ()) in - no_ghost [ASM ($2, $4, $5, loc)] + no_ghost [ASM ($2, mk_asm_templates $4, $5, loc)] } | MSASM { no_ghost [ASM ([], [fst $1], None, snd $1)]} | TRY block EXCEPT paren_comma_expression block { diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml index 50d016622a4700ac407c6a8262b8dac05d985930..73412c8d1117136e8ea6b334e6602539c105dc64 100644 --- a/src/kernel_services/parsetree/cabshelper.ml +++ b/src/kernel_services/parsetree/cabshelper.ml @@ -232,6 +232,40 @@ let mk_behavior ?(name=Cil.default_behavior_name) ?(assumes=[]) ?(requires=[]) b_extended = extended; } +let mk_asm_templates = + let buf = Buffer.create 100 in + let rec outer res = function + | [] when Buffer.length buf = 0 -> List.rev res + | [] -> + let res = List.rev @@ Buffer.contents buf :: res in + Buffer.clear buf; + res + | str :: tail -> tail |> outer @@ inner res str 0 + and inner res template i = + if i < String.length template then + let c = String.get template i in + Buffer.add_char buf c; + if c = '\n' then + if i < String.length template - 1 then + match String.get template @@ i + 1 with + | '\t' -> + Buffer.add_char buf '\t'; + let res = Buffer.contents buf :: res in + Buffer.clear buf; + inner res template @@ i + 2 + | c -> + let res = Buffer.contents buf :: res in + Buffer.clear buf; + Buffer.add_char buf c; + inner res template @@ i + 2 + else + let res = Buffer.contents buf :: res in + Buffer.clear buf; + res + else inner res template @@ i + 1 + else res in + outer [] + (* Local Variables: diff --git a/src/kernel_services/parsetree/cabshelper.mli b/src/kernel_services/parsetree/cabshelper.mli index 13a295600e72f9bd53dc4d8ae509608d81dc6cbf..a4b0498146e4bce7b14fa47a60c7adf8d615981e 100644 --- a/src/kernel_services/parsetree/cabshelper.mli +++ b/src/kernel_services/parsetree/cabshelper.mli @@ -87,3 +87,5 @@ val mk_behavior : ?extended:Logic_ptree.extension list -> unit -> Logic_ptree.behavior + +val mk_asm_templates : string list -> string list