Skip to content

Commit 128edae

Browse files
committed
Extraction.Krml: add ESizeof node
See FStarLang/karamel#743
1 parent 11eaf66 commit 128edae

1 file changed

Lines changed: 3 additions & 1 deletion

File tree

src/extraction/FStarC.Extraction.Krml.fst

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,8 +45,9 @@ module FC = FStarC.Const
4545
- v29: added a SizeT and PtrdiffT width to machine integers
4646
- v30: Added EBufDiff
4747
- v31: Added a `meta` field to binders. Currently only relevant to propagate `CInline`.
48+
- v32: Introduce ESizeof
4849
*)
49-
let current_version: version = 31
50+
let current_version: version = 32
5051

5152
(* COPY-PASTED ****************************************************************)
5253

@@ -140,6 +141,7 @@ and expr =
140141
| EAddrOf of expr
141142
| EBufNull of typ
142143
| EBufDiff of expr & expr
144+
| ESizeof of typ
143145

144146
and op =
145147
| Add | AddW | Sub | SubW | Div | DivW | Mult | MultW | Mod

0 commit comments

Comments
 (0)