diff options
| -rw-r--r-- | Makefile | 19 | ||||
| -rw-r--r-- | src/Translate.ml | 8 | ||||
| -rw-r--r-- | src/main.ml | 13 |
3 files changed, 26 insertions, 14 deletions
@@ -1,10 +1,10 @@ all: build-test -CHARON_HOME=../charon -CHARON_EXEC=$(CHARON_HOME)/charon -CHARON_TESTS_DIR=$(CHARON_HOME)/tests/cfim -CHARON_OPTIONS= --dest ../tests/cfim --no-code-duplication -DEST_DIR=tests +CHARON_HOME = ../charon +CHARON_EXEC = $(CHARON_HOME)/charon +CHARON_TESTS_DIR = $(CHARON_HOME)/tests/cfim +CHARON_OPTIONS = --dest ../tests/cfim --no-code-duplication +DEST_DIR = tests # The user can specify additional translation options for Aeneas: OPTIONS ?= @@ -12,8 +12,8 @@ OPTIONS ?= # Default translation options: # - insert calls to the normalizer in the translated code to test the # generated unit functions -TRANS_OPTIONS:=-test-trans-units $(OPTIONS) -SUBDIR:= +TRANS_OPTIONS := -test-trans-units $(OPTIONS) +SUBDIR := # Build the project and test it .PHONY: build-test @@ -29,9 +29,10 @@ build: test: build translate-no_nested_borrows translate-hashmap translate-paper # Add specific options to some tests -translate-no_nested_borrows translate-paper: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decreases-clauses +translate-no_nested_borrows translate-paper: \ + TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-decreases-clauses translate-no_nested_borrows translate-paper: SUBDIR:=misc -translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses +translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses -no-state translate-hashmap: SUBDIR:=hashmap # Generic rule to extract the CFIM from a rust file diff --git a/src/Translate.ml b/src/Translate.ml index ab9ed216..ac2ee38c 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -29,8 +29,14 @@ type config = { let _ = assert_norm (FUNCTION () = Success ()) ``` *) + use_state_monad : bool; + (** If `true`, use a state-error monad. + If `false`, only use an error monad. + + Using a state-error monad is necessary when modelling I/O, for instance. + *) extract_decreases_clauses : bool; - (** If true, insert `decreases` clauses for all the recursive definitions. + (** If `true`, insert `decreases` clauses for all the recursive definitions. The body of such clauses must be defined by the user. *) diff --git a/src/main.ml b/src/main.ml index 4a111a25..df2d1b0c 100644 --- a/src/main.ml +++ b/src/main.ml @@ -31,8 +31,9 @@ let () = let test_units = ref false in let test_trans_units = ref false in let no_decreases_clauses = ref false in + let no_state = ref false in let template_decreases_clauses = ref false in - let no_split = ref false in + let no_split_files = ref false in let no_check_inv = ref false in let spec = @@ -68,13 +69,16 @@ let () = ( "-no-decreases-clauses", Arg.Set no_decreases_clauses, " Do not add decrease clauses to the recursive definitions" ); + ( "-no-state", + Arg.Set no_state, + " Do not use state-error monads, simply use error monads" ); ( "-template-clauses", Arg.Set template_decreases_clauses, " Generate templates for the required decreases clauses, in a\n\ \ dedicated file. Incompatible with \ -no-decreases-clauses" ); - ( "-no-split", - Arg.Set no_split, + ( "-no-split-files", + Arg.Set no_split_files, " Don't split the definitions between different files for types,\n\ \ functions, etc." ); ( "-no-check-inv", @@ -179,8 +183,9 @@ let () = { Translate.eval_config; mp_config = micro_passes_config; - split_files = not !no_split; + split_files = not !no_split_files; test_unit_functions; + use_state_monad = not !no_state; extract_decreases_clauses = not !no_decreases_clauses; extract_template_decreases_clauses = !template_decreases_clauses; } |