From d4e98fe81c23e3ee51648dbf6c07f73f29a8e9a7 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Fri, 25 Aug 2023 19:20:45 +0100 Subject: [PATCH] CN: Fix for multiple CN statements on a single line --- backend/cn/core_to_mucore.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/backend/cn/core_to_mucore.ml b/backend/cn/core_to_mucore.ml index 1e4e30d17..bc86914d4 100644 --- a/backend/cn/core_to_mucore.ml +++ b/backend/cn/core_to_mucore.ml @@ -750,8 +750,16 @@ let rec n_expr (loc : Loc.t) ((env, old_states), desugaring_things) (global_type Expr ([], Epure (Pexpr ([], (), PEval Vunit))) -> let separated_annots = List.map (fun (loc, joined_strs) -> - let separate_strs = String.split_on_char '\n' joined_strs in - List.map (fun str -> (loc, str)) separate_strs + let separate_strs = String.split_on_char ';' joined_strs in + let separate_strs = List.map String.trim separate_strs in + let separate_locs_and_strs = List.map (fun str -> + if not (String.equal str "") then + [(loc, str ^ ";")] + else + [] + ) separate_strs + in + List.concat separate_locs_and_strs ) (get_cerb_magic_attr annots) in let@ desugared_stmts_and_stmts = ListM.mapM (fun (stmt_loc, stmt_str) ->