Stop using the '_pure' namespace

viperproject · Sep 30, 2020 · f4b4e26 · f4b4e26
1 parent 931b5ec
commit f4b4e26
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/prusti-viper/src/encoder/pure_function_encoder.rs b/prusti-viper/src/encoder/pure_function_encoder.rs
@@ -46,7 +46,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
             encoder,
             mir,
             proc_def_id,
-            "_pure".to_string(),
+            "".to_string(),
             is_encoding_assertion,
         );
         PureFunctionEncoder {

diff --git a/prusti-viper/src/encoder/spec_encoder.rs b/prusti-viper/src/encoder/spec_encoder.rs
@@ -156,7 +156,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> SpecEncoder<'p, 'v, 'tcx> {
 //         }
         // let mut curr_def_id = tcx.hir.local_def_id(curr_node_id);
         let mut curr_def_id = assertion_expr.expr.to_def_id();
-        let mut curr_namespace = "_pure".to_string();
+        let mut curr_namespace = "".to_string();
 
         let mut encoded_expr = self.encoder.encode_pure_function_body(curr_def_id);