summaryrefslogtreecommitdiff
path: root/test/c
diff options
context:
space:
mode:
authorAlasdair2018-12-18 01:56:51 +0000
committerAlasdair2018-12-18 01:59:02 +0000
commit3da039c72efa210b7b162c4571925504f275a978 (patch)
tree9b64fe9e6452767afab1ea85e5455ad4bee22e60 /test/c
parent586b5f5c27bef271a9a013cad8d5b132df354c23 (diff)
Store function instantiation information within annotations, so we don't
have to recompute it, which can be very expensive for very large specifications Also additional flow typing and fixes for boolean type variables
Diffstat (limited to 'test/c')
-rw-r--r--test/c/bool_bits_mapping.expect2
-rw-r--r--test/c/bool_bits_mapping.sail23
2 files changed, 25 insertions, 0 deletions
diff --git a/test/c/bool_bits_mapping.expect b/test/c/bool_bits_mapping.expect
new file mode 100644
index 00000000..79ebd086
--- /dev/null
+++ b/test/c/bool_bits_mapping.expect
@@ -0,0 +1,2 @@
+ok
+ok
diff --git a/test/c/bool_bits_mapping.sail b/test/c/bool_bits_mapping.sail
new file mode 100644
index 00000000..1a104186
--- /dev/null
+++ b/test/c/bool_bits_mapping.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+$include <prelude.sail>
+
+mapping bool_bits : bool <-> bits(1) = {
+ true <-> 0b1,
+ false <-> 0b0
+}
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+ if bool_bits(0b1) then {
+ print_endline("ok")
+ } else {
+ print_endline("fail")
+ };
+ if bool_bits(true) == 0b1 then {
+ print_endline("ok")
+ } else {
+ print_endline("fail")
+ }
+} \ No newline at end of file