diff options
| author | Thomas Bauereiss | 2017-11-02 13:13:13 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-11-02 13:20:27 +0000 |
| commit | 9ea44b8b441eb394ffdd85d0b356167002ad7fdd (patch) | |
| tree | 17f26ee1481c98a1170cbc6d63081efe2da0d879 /src/ast_util.mli | |
| parent | e8cc2e365b7171635eb43853273cc9109e0e2553 (diff) | |
Optionally generate an initial register state for the sequential Lem shallow embedding
Checks for command-line flag -undefined_gen and uses the undefined value
generator functions of the form undefined_typ to initialise registers
Diffstat (limited to 'src/ast_util.mli')
| -rw-r--r-- | src/ast_util.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli index 1a056e58..8f1f06e6 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -244,3 +244,5 @@ val effect_set : effect -> BESet.t val tyvars_of_nexp : nexp -> KidSet.t val tyvars_of_typ : typ -> KidSet.t + +val undefined_of_typ : bool -> Ast.l -> (typ -> 'annot) -> typ -> 'annot exp |