From 985401f124ebd6a257b13bb2f5f01378cc5f0ce5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Mar 2022 23:34:19 +0100
Subject: Change the extension of the serialized files to .llbc

---
 Makefile                       | 30 ++++++++++++-------------
 src/Translate.ml               |  2 +-
 src/main.ml                    |  2 +-
 tests/hashmap/Hashmap.Funs.fst | 50 +++++++++++++++++++++---------------------
 4 files changed, 42 insertions(+), 42 deletions(-)

diff --git a/Makefile b/Makefile
index efbef884..0c772e41 100644
--- a/Makefile
+++ b/Makefile
@@ -42,34 +42,34 @@ translate-hashmap: SUBDIR:=hashmap
 translate-nll-betree_nll: TRANS_OPTIONS=-test-units -no-split-files -no-state -no-decreases-clauses
 translate-nll-betree_nll: SUBDIR:=misc
 
-# Generic rules to extract the CFIM from a rust file
+# Generic rules to extract the LLBC from a rust file
 # The "standard" and the nll (non-linear lifetime) tests are in separate
 # directories in Charon
-.PHONY: gen-cfim-%
+.PHONY: gen-llbc-%
 
 # TODO: remove those "gen-..." rules, and just do `make` in the charon repo
-gen-cfim-%: CHARON_OPTIONS = --dest ../tests/cfim --no-code-duplication
-gen-cfim-%: CHARON_TESTS_SRC = ../tests/src
+gen-llbc-%: CHARON_OPTIONS = --dest ../tests/llbc --no-code-duplication
+gen-llbc-%: CHARON_TESTS_SRC = ../tests/src
 
-gen-cfim-nll-%: CHARON_OPTIONS = --dest ../tests-nll/cfim --no-code-duplication --nll
-gen-cfim-nll-%: CHARON_TESTS_SRC = ../tests-nll/src
+gen-llbc-nll-%: CHARON_OPTIONS = --dest ../tests-nll/llbc --no-code-duplication --nll
+gen-llbc-nll-%: CHARON_TESTS_SRC = ../tests-nll/src
 
-gen-cfim-%: build
+gen-llbc-%: build
 	cd $(CHARON_HOME)/charon && cargo run $(CHARON_TESTS_SRC)/$*.rs $(CHARON_OPTIONS)
 
-gen-cfim-nll-%: build
+gen-llbc-nll-%: build
 	cd $(CHARON_HOME)/charon && cargo run $(CHARON_TESTS_SRC)/$*.rs $(CHARON_OPTIONS)
 
-# Generic rule to test the translation on a CFIM file
+# Generic rule to test the translation on a LLBC file
 .PHONY: translate-%
-translate-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/cfim
-translate-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/cfim
+translate-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
+translate-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc
 
-translate-%: gen-cfim-%
-	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.cfim -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+translate-%: gen-llbc-%
+	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
-translate-nll-%: gen-cfim-nll-%
-	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.cfim -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+translate-nll-%: gen-llbc-nll-%
+	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
 .PHONY: doc
 doc:
diff --git a/src/Translate.ml b/src/Translate.ml
index d337f5b8..1a42892d 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -602,7 +602,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   (* First compute the filename by replacing the extension and converting the
    * case (rust module names are snake case) *)
   let module_name, extract_filebasename =
-    match Filename.chop_suffix_opt ~suffix:".cfim" filename with
+    match Filename.chop_suffix_opt ~suffix:".llbc" filename with
     | None ->
         (* Note that we already checked the suffix upon opening the file *)
         failwith "Unreachable"
diff --git a/src/main.ml b/src/main.ml
index 6d4888f9..00693890 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -103,7 +103,7 @@ let () =
     match !filenames with
     | [ f ] ->
         (* TODO: update the extension *)
-        if not (Filename.check_suffix f ".cfim") then (
+        if not (Filename.check_suffix f ".llbc") then (
           print_string "Unrecognized file extension";
           fail ())
         else if not (Sys.file_exists f) then (
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 931f8625..75cd1659 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -10,7 +10,7 @@ include Hashmap.Clauses
 (** [hashmap::hash_key] *)
 let hash_key_fwd (k : usize) : result usize = Return k
 
-(** [hashmap::HashMap{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots] *)
 let rec hash_map_allocate_slots_fwd
   (t : Type0) (slots : vec (list_t t)) (n : usize) :
   Tot (result (vec (list_t t)))
@@ -33,7 +33,7 @@ let rec hash_map_allocate_slots_fwd
     end
   end
 
-(** [hashmap::HashMap{0}::new_with_capacity] *)
+(** [hashmap::HashMap::{0}::new_with_capacity] *)
 let hash_map_new_with_capacity_fwd
   (t : Type0) (capacity : usize) (max_load_dividend : usize)
   (max_load_divisor : usize) :
@@ -54,14 +54,14 @@ let hash_map_new_with_capacity_fwd
     end
   end
 
-(** [hashmap::HashMap{0}::new] *)
+(** [hashmap::HashMap::{0}::new] *)
 let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
   begin match hash_map_new_with_capacity_fwd t 32 4 5 with
   | Fail -> Fail
   | Return hm -> Return hm
   end
 
-(** [hashmap::HashMap{0}::clear_slots] *)
+(** [hashmap::HashMap::{0}::clear_slots] *)
 let rec hash_map_clear_slots_fwd_back
   (t : Type0) (slots : vec (list_t t)) (i : usize) :
   Tot (result (vec (list_t t)))
@@ -84,7 +84,7 @@ let rec hash_map_clear_slots_fwd_back
     end
   else Return slots
 
-(** [hashmap::HashMap{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear] *)
 let hash_map_clear_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
   begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with
@@ -94,11 +94,11 @@ let hash_map_clear_fwd_back
       v)
   end
 
-(** [hashmap::HashMap{0}::len] *)
+(** [hashmap::HashMap::{0}::len] *)
 let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
   Return self.hash_map_num_entries
 
-(** [hashmap::HashMap{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list] *)
 let rec hash_map_insert_in_list_fwd
   (t : Type0) (key : usize) (value : t) (ls : list_t t) :
   Tot (result bool)
@@ -116,7 +116,7 @@ let rec hash_map_insert_in_list_fwd
   | ListNil -> Return true
   end
 
-(** [hashmap::HashMap{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list] *)
 let rec hash_map_insert_in_list_back
   (t : Type0) (key : usize) (value : t) (ls : list_t t) :
   Tot (result (list_t t))
@@ -134,7 +134,7 @@ let rec hash_map_insert_in_list_back
   | ListNil -> let l = ListNil in Return (ListCons key value l)
   end
 
-(** [hashmap::HashMap{0}::insert_no_resize] *)
+(** [hashmap::HashMap::{0}::insert_no_resize] *)
 let hash_map_insert_no_resize_fwd_back
   (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
   result (hash_map_t t)
@@ -190,7 +190,7 @@ let hash_map_insert_no_resize_fwd_back
     end
   end
 
-(** [hashmap::HashMap{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list] *)
 let rec hash_map_move_elements_from_list_fwd_back
   (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
   Tot (result (hash_map_t t))
@@ -209,7 +209,7 @@ let rec hash_map_move_elements_from_list_fwd_back
   | ListNil -> Return ntable
   end
 
-(** [hashmap::HashMap{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements] *)
 let rec hash_map_move_elements_fwd_back
   (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
   Tot (result ((hash_map_t t) & (vec (list_t t))))
@@ -242,7 +242,7 @@ let rec hash_map_move_elements_fwd_back
     end
   else Return (ntable, slots)
 
-(** [hashmap::HashMap{0}::try_resize] *)
+(** [hashmap::HashMap::{0}::try_resize] *)
 let hash_map_try_resize_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
   let i = vec_len (list_t t) self.hash_map_slots in
@@ -278,7 +278,7 @@ let hash_map_try_resize_fwd_back
     end
   end
 
-(** [hashmap::HashMap{0}::insert] *)
+(** [hashmap::HashMap::{0}::insert] *)
 let hash_map_insert_fwd_back
   (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
   result (hash_map_t t)
@@ -304,7 +304,7 @@ let hash_map_insert_fwd_back
     end
   end
 
-(** [hashmap::HashMap{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list] *)
 let rec hash_map_contains_key_in_list_fwd
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result bool)
@@ -322,7 +322,7 @@ let rec hash_map_contains_key_in_list_fwd
   | ListNil -> Return false
   end
 
-(** [hashmap::HashMap{0}::contains_key] *)
+(** [hashmap::HashMap::{0}::contains_key] *)
 let hash_map_contains_key_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result bool =
   begin match hash_key_fwd key with
@@ -343,7 +343,7 @@ let hash_map_contains_key_fwd
     end
   end
 
-(** [hashmap::HashMap{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list] *)
 let rec hash_map_get_in_list_fwd
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls))
@@ -360,7 +360,7 @@ let rec hash_map_get_in_list_fwd
   | ListNil -> Fail
   end
 
-(** [hashmap::HashMap{0}::get] *)
+(** [hashmap::HashMap::{0}::get] *)
 let hash_map_get_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result t =
   begin match hash_key_fwd key with
@@ -381,7 +381,7 @@ let hash_map_get_fwd
     end
   end
 
-(** [hashmap::HashMap{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hash_map_get_mut_in_list_fwd
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
@@ -398,7 +398,7 @@ let rec hash_map_get_mut_in_list_fwd
   | ListNil -> Fail
   end
 
-(** [hashmap::HashMap{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hash_map_get_mut_in_list_back
   (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
   Tot (result (list_t t))
@@ -416,7 +416,7 @@ let rec hash_map_get_mut_in_list_back
   | ListNil -> Fail
   end
 
-(** [hashmap::HashMap{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut] *)
 let hash_map_get_mut_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result t =
   begin match hash_key_fwd key with
@@ -438,7 +438,7 @@ let hash_map_get_mut_fwd
     end
   end
 
-(** [hashmap::HashMap{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut] *)
 let hash_map_get_mut_back
   (t : Type0) (self : hash_map_t t) (key : usize) (ret : t) :
   result (hash_map_t t)
@@ -469,7 +469,7 @@ let hash_map_get_mut_back
     end
   end
 
-(** [hashmap::HashMap{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list] *)
 let rec hash_map_remove_from_list_fwd
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result (option t))
@@ -492,7 +492,7 @@ let rec hash_map_remove_from_list_fwd
   | ListNil -> Return None
   end
 
-(** [hashmap::HashMap{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list] *)
 let rec hash_map_remove_from_list_back
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result (list_t t))
@@ -515,7 +515,7 @@ let rec hash_map_remove_from_list_back
   | ListNil -> Return ListNil
   end
 
-(** [hashmap::HashMap{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove] *)
 let hash_map_remove_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
   begin match hash_key_fwd key with
@@ -545,7 +545,7 @@ let hash_map_remove_fwd
     end
   end
 
-(** [hashmap::HashMap{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove] *)
 let hash_map_remove_back
   (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) =
   begin match hash_key_fwd key with
-- 
cgit v1.2.3