Disable comments by default

adds option to enable them
AeneasVerif · Oct 11, 2024 · 809fdf7 · 809fdf7
1 parent 1fff1c5
commit 809fdf7
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 1 deletion.
diff --git a/bin/main.ml b/bin/main.ml
@@ -24,6 +24,7 @@ Supported options:|}
       ( "--header",
         Arg.Set_string Krml.Options.header,
         " path to a header file to be prepended to the generated C" );
+      "--comments", Arg.Set O.comments, " keep inline comments";
       "--config", Arg.Set_string O.config, " YAML configuration file";
       "-funroll-loops", Arg.Set_int funroll_loops, " unrool loops up to N";
     ]

diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
@@ -1563,7 +1563,7 @@ let rec expression_of_raw_statement (env : env) (ret_var : C.var_id) (s : C.raw_
 
 and expression_of_statement (env: env) (ret_var: C.var_id) (s: C.statement): K.expr =
   { (expression_of_raw_statement env ret_var s.content) with
-    meta = List.map (fun x -> K.CommentBefore x) s.comments_before }
+    meta = if !Options.comments then List.map (fun x -> K.CommentBefore x) s.comments_before else [] }
 
 (** Top-level declarations: orchestration *)
 

diff --git a/lib/Options.ml b/lib/Options.ml
@@ -1,2 +1,3 @@
 let log_level = ref ""
 let config = ref ""
+let comments = ref false