diff --git a/drivers/rust_unsafe_usize.drv b/drivers/rust_unsafe_usize.drv new file mode 100644 index 0000000000000000000000000000000000000000..ab52aaa014864387bf5a4d56284206e55ceaa0f3 --- /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