Merge pull request #76 from FStarLang/_taramana_pure_ghost_stmt

Support _ghost_stmt in _pure functions

Author: gebner

src/pass/emit.rs

@@ -2598,6 +2598,25 @@ impl<'a> Emitter<'a> {
                 )
             }
 
+            StmtT::GhostStmt(code) => {
+                let env = &mut env.clone();
+                let ghost_doc = self.emit_inline_pulse_tokens(env, code);
+                let rest = self.emit_pure_body(env, &stmts[1..]);
+                parens(
+                    Doc::text("let")
+                        .append(Doc::line())
+                        .append("_")
+                        .append(Doc::line())
+                        .append("=")
+                        .group()
+                        .nest(2)
+                        .append(Doc::line().append(ghost_doc).nest(2))
+                        .append(Doc::line())
+                        .append("in")
+                        .append(Doc::line().append(rest).nest(2)),
+                )
+            }
+
             StmtT::Decl(x, ty) => {
                 // Look for the assignment to this variable in the next statement
                 if stmts.len() >= 3 {

test/pure_fn.c

@@ -49,3 +49,10 @@ void test() {
     bool pure_not_result = pure_not(true);
     _assert(pure_not_result == false);
 }
+
+_pure int pure_ghost_stmt()
+  _ensures(1 == 0)
+{
+  _ghost_stmt(assume False);
+  return 1;
+}