test bundle rename and rename-prefix

Author: tahina-pro

test/rust-val/AuxB.fsti

@@ -0,0 +1,3 @@
+module AuxB
+
+val bar : bool -> bool

test/rust-val/Makefile

@@ -56,9 +56,9 @@ $(CACHE_DIR)/%.checked: | .depend
 
 .PRECIOUS: %.rs
 %.rs: $(ALL_KRML_FILES) $(KRML_BIN)
-	$(KRML) -minimal -bundle $(notdir $(subst rust,Rust,$*))=\* \
+	$(KRML) -minimal -bundle AuxA+AuxB=[rename=Aux,rename-prefix] -bundle $(notdir $(subst rust,Rust,$*))=\* \
 	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
-	$(SED) -i 's/\(patterns..\)/\1\nmod auxa; mod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
+	$(SED) -i 's/\(patterns..\)/\1\nmod aux; mod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
 	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@
 
 %.rust-test: %.rs

test/rust-val/Rusttest.fst

@@ -9,7 +9,9 @@ let test2 (b: B.buffer bool) : HST.Stack bool
   (fun _ _ _ -> True)
 =
   let x = B.index b C._zero_for_deref in
-  AuxA.foo x
+  let r1 = AuxA.foo x in
+  let r2 = AuxB.bar x in
+  r1 && r2
 
 let main_ () : HST.Stack I32.t
   (fun _ -> True)

test/rust-val/auxa.rs test/rust-val/aux.rstest/rust-val/auxa.rs renamed to test/rust-val/aux.rs

@@ -8,3 +8,8 @@ pub fn foo(x: bool) -> bool
 {
     return !x;
 }
+
+pub fn bar(x: bool) -> bool
+{
+    return x;
+}