diff options
| -rw-r--r-- | Makefile | 30 | ||||
| -rw-r--r-- | src/Translate.ml | 2 | ||||
| -rw-r--r-- | src/main.ml | 2 | ||||
| -rw-r--r-- | tests/hashmap/Hashmap.Funs.fst | 50 |
4 files changed, 42 insertions, 42 deletions
@@ -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 |