diff options
author | Son HO | 2024-05-24 14:16:37 +0200 |
---|---|---|
committer | GitHub | 2024-05-24 14:16:37 +0200 |
commit | c6c9e351546a723e62cc21579b2359dba3bfb56f (patch) | |
tree | 74ed652b8862d1dde24ccd65b6c29503ea3db35c /compiler/InterpreterExpansion.mli | |
parent | e669de58b71fd68642cfacf1a2e3cbd1c5b2f4fe (diff) | |
parent | 69ff150ede10b7d24f9777298e8ca3de163c33e1 (diff) |
Merge pull request #175 from AeneasVerif/afromher/meta
Rename meta into span
Diffstat (limited to 'compiler/InterpreterExpansion.mli')
-rw-r--r-- | compiler/InterpreterExpansion.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 7140d55f..7f8c3a0a 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -13,7 +13,7 @@ type proj_kind = LoanProj | BorrowProj *) val apply_symbolic_expansion_non_borrow : config -> - Meta.meta -> + Meta.span -> symbolic_value -> eval_ctx -> symbolic_expansion -> @@ -21,20 +21,20 @@ val apply_symbolic_expansion_non_borrow : (** Expand a symhbolic value, without branching *) val expand_symbolic_value_no_branching : - config -> Meta.meta -> symbolic_value -> SA.mplace option -> cm_fun + config -> Meta.span -> symbolic_value -> SA.mplace option -> cm_fun (** Expand a symbolic enumeration (leads to branching if the enumeration has more than one variant). Parameters: - [config] - - [meta] + - [span] - [sv] - [sv_place] *) val expand_symbolic_adt : config -> - Meta.meta -> + Meta.span -> symbolic_value -> SA.mplace option -> eval_ctx -> @@ -46,7 +46,7 @@ val expand_symbolic_adt : *) val expand_symbolic_bool : config -> - Meta.meta -> + Meta.span -> symbolic_value -> SA.mplace option -> eval_ctx -> @@ -69,7 +69,7 @@ val expand_symbolic_bool : *) val expand_symbolic_int : config -> - Meta.meta -> + Meta.span -> symbolic_value -> SA.mplace option -> integer_type -> @@ -82,4 +82,4 @@ val expand_symbolic_int : (** If this mode is activated through the [config], greedily expand the symbolic values which need to be expanded. See {!type:Contexts.config} for more information. *) -val greedy_expand_symbolic_values : config -> Meta.meta -> cm_fun +val greedy_expand_symbolic_values : config -> Meta.span -> cm_fun |