From a8dac7fdf36cf44e944306825d1950dccd2f1694 Mon Sep 17 00:00:00 2001
From: nilfit <nils.fitinghoff@gmail.com>
Date: Thu, 28 Feb 2019 16:58:32 +0100
Subject: [PATCH] add unsafe driver mapping int.Int to usize

---
 drivers/rust_unsafe_usize.drv | 98 +++++++++++++++++++++++++++++++++++
 1 file changed, 98 insertions(+)
 create mode 100644 drivers/rust_unsafe_usize.drv

diff --git a/drivers/rust_unsafe_usize.drv b/drivers/rust_unsafe_usize.drv
new file mode 100644
index 000000000..ab52aaa01
--- /dev/null
+++ b/drivers/rust_unsafe_usize.drv
@@ -0,0 +1,98 @@
+printer "rust"
+
+theory BuiltIn
+  syntax type int "usize"
+  syntax literal int "%1"
+  syntax predicate (=) "%1 == %2"
+end
+
+theory Bool
+  syntax type bool "bool"
+  syntax function True "true"
+  syntax function False "false"
+end
+
+module int.Int
+  syntax constant zero "0"
+  syntax constant one "1"
+
+  syntax predicate (<)  "%1 < %2"
+  syntax predicate (<=) "%1 <= %2"
+  syntax predicate (>)   "%1 > %2"
+  syntax predicate (>=)  "%1 >= %2"
+  syntax val       (=)   "%1 == %2"
+
+  syntax function  (+)   "%1 + %2"
+  syntax function  (-)   "%1 - %2"
+  syntax function  ( * ) "%1 * %2"
+  syntax function  (-_)  "-%1"
+end
+
+module Ref
+  syntax type ref "%1"
+  syntax function contents "%1"
+  syntax val ref "%1"
+end
+
+module ref.Ref
+  syntax val (!_) "%1"
+  syntax val (:=) "%1 = %2"
+end
+
+module ref.Refint
+  syntax val incr "%1 += 1"
+  syntax val decr "%1 -= 1"
+  syntax val (+=) "%1 += %2"
+  syntax val (-=) "%1 -= %2"
+  syntax val ( *= ) "%1 *= %2"
+end
+
+module int.ComputerDivision
+  syntax val div "%1 / %2"
+  syntax val mod "%1 % %2"
+end
+
+module mach.int.Int
+  syntax val ( / ) "%1 / %2"
+  syntax val ( % ) "%1 % %2"
+end
+
+module mach.int.Int32
+  syntax type     int32     "i32"
+
+  syntax literal   int32    "%1"
+
+  syntax val of_int "%1 as i32"
+  syntax val to_int "%1 as u32"
+
+  syntax val      ( + )     "%1 + %2"
+  syntax val      ( - )     "%1 - %2"
+  syntax val      (-_)      "- %1"
+  syntax val      ( * )     "%1 * %2"
+  syntax val      ( / )     "%1 / %2"
+  syntax val      ( % )     "%1 % %2"
+  syntax val      (=)       "%1 == %2"
+  syntax val      (<=)      "%1 <= %2"
+  syntax val      (<)       "%1 < %2"
+  syntax val      (>=)      "%1 >= %2"
+  syntax val      (>)       "%1 > %2"
+
+end
+
+module array.Array
+  syntax type array "&mut [%1]"
+
+  syntax val ([])          "%1[%2]"
+  syntax val ([]<-)        "%1[%2] = %3"
+  syntax val length        "%1.len()"
+
+  syntax val copy          "&mut %1.iter().cloned().collect::<Vec<u32>>()[..]"
+
+(*   syntax val blit          "%1[%2 .. (%2 + %5)].clone_from_slice(&%3[%4 .. (%4 + %5)])" *)
+  syntax val blit          "%3[%4 .. (%4 + %5)].clone_from_slice(&%1[%2 .. (%2 + %5)])"
+end
+
+module int.MinMax
+  syntax val min "%1.min(%2)"
+  syntax val max "%1.max(%2)"
+end
-- 
GitLab