diff options
| author | Alasdair | 2019-03-14 23:39:11 +0000 |
|---|---|---|
| committer | Alasdair | 2019-03-15 00:34:41 +0000 |
| commit | 6137b6b5b788138dd02503cb1e88242a618a3677 (patch) | |
| tree | e0848601a9aa177dbf8879c46dd81a4fc2db2a06 /src/jib/jib_compile.mli | |
| parent | c741e731afe4a6d2c65d43ca299a1a48a1534ec0 (diff) | |
C: Wrap Jib identifiers
Avoids duplication between l-expressions and expressions. Also means that
special variables like current_exception and have_exception are treated
normally by functions such as instr_reads and instr_writes etc. Furthermore
we can now easily annotate Jib identifiers in ways that were not previously
possible with plain sail ids.
Diffstat (limited to 'src/jib/jib_compile.mli')
| -rw-r--r-- | src/jib/jib_compile.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index f3bd8c76..a0cacc3c 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -63,6 +63,8 @@ val opt_debug_flow_graphs : bool ref (** Print the IR representation of a specific function. *) val opt_debug_function : string ref +val ngensym : unit -> name + (** {2 Jib context} *) (** Context for compiling Sail to Jib. We need to pass a (global) |