forked from FStarLang/karamel
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathTests.ml
More file actions
24 lines (24 loc) · 767 Bytes
/
Copy pathTests.ml
File metadata and controls
24 lines (24 loc) · 767 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
let _ =
Printf.printf "Printing with w=%d\n" Utils.twidth;
let open CStar in
let open Constant in
let open PPrint in
let p t =
let d: CStar.decl = Type ("t", t) in
let d = CStarToC.mk_stub_or_function d in
match d with
| C.Decl d ->
Print.print (group (PrintC.p_declaration d));
print_newline ()
| _ ->
assert false
in
let t: CStar.typ = Array (Pointer (Int UInt8), Constant (UInt8, "4")) in
p t;
let t: CStar.typ = Pointer (Array (Int UInt8, Constant (UInt8, "4"))) in
p t;
let t: CStar.typ = Pointer (Function (Pointer (Array (Int UInt8, Constant (UInt8, "3"))), [Int UInt32])) in
p t;
let t: CStar.typ = Pointer (Function (Struct (Some "foo", [ "bar", Int UInt8 ]), [Int UInt32])) in
p t;
;;