Temporary fix for #293

src/PrintC.ml

@@ -367,14 +367,14 @@ and p_stmt (s: stmt) =
         string (KPrint.bsprintf "%s %a" prefix pdoc doc)
       in
       group (mk_line "#if" (p_expr cond) ^^ hardline ^^
-        p_stmts then_block ^^ hardline ^^
+        p_stmt (Compound then_block) ^^ hardline ^^
         separate_map hardline (fun (cond, stmts) ->
           mk_line "#elif" (p_expr cond) ^^ hardline ^^
-          p_stmts stmts) elif_blocks ^^
+          p_stmt (Compound stmts)) elif_blocks ^^
         (if List.length elif_blocks > 0 then hardline else empty) ^^
         (if List.length else_block > 0 then
           string "#else" ^^ hardline ^^
-          p_stmts else_block ^^ hardline
+          p_stmt (Compound else_block) ^^ hardline
         else
           empty) ^^
         string "#endif")

test/IfDefKrml.fst

@@ -0,0 +1,25 @@
+module IfDefKrml
+open FStar.HyperStack.ST
+open LowStar.Buffer
+[@@CIfDef]
+assume
+val flag : bool
+
+
+let something_effectful (x:bool) : Stack bool (requires λ _ → ⊤) (ensures (λ _ _ _ → ⊤)) = x
+
+let test (x y:bool) =
+  let z =
+    if flag
+    then false
+    else let aa = something_effectful x in
+         aa
+  in
+  let z =
+    if flag
+    then false
+    else let aa = something_effectful z in
+         aa
+  in z
+
+let main () = if test true true then 0l else 1l