mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
92d19d80f5
This patch also adds some explicit spaces, to avoir interpreting "- -" as the preincrement operator. It also removes useless precedence from plain functions.
654 lines
17 KiB
Plaintext
654 lines
17 KiB
Plaintext
(** C driver
|
|
|
|
For precedence numbers, see the table at
|
|
https://en.cppreference.com/w/c/language/operator_precedence
|
|
*)
|
|
|
|
printer "c"
|
|
|
|
module ref.Ref
|
|
syntax val (!_) "%d1" prec 2 2
|
|
syntax val (:=) "%d1 = %2" prec 14 2 14
|
|
end
|
|
|
|
module mach.int.Bounded_int
|
|
syntax val of_int "%1" prec 0
|
|
end
|
|
|
|
module mach.int.Int16
|
|
|
|
prelude export "#include <stdint.h>"
|
|
interface export "#include <stdint.h>"
|
|
syntax type int16 "int16_t"
|
|
syntax literal int16 "%c"
|
|
|
|
syntax val (+) "%1 + %2" prec 4 4 3
|
|
syntax val (-) "%1 - %2" prec 4 4 3
|
|
syntax val (-_) "- %1" prec 2 2
|
|
syntax val ( * ) "%1 * %2" prec 3 3 2
|
|
syntax val (/) "%1 / %2" prec 3 3 2
|
|
syntax val (%) "%1 % %2" prec 3 3 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.int.Int32
|
|
|
|
prelude export "#include <stdint.h>"
|
|
interface export "#include <stdint.h>"
|
|
syntax type int32 "int32_t"
|
|
syntax literal int32 "%c"
|
|
|
|
syntax val (+) "%1 + %2" prec 4 4 3
|
|
syntax val (-) "%1 - %2" prec 4 4 3
|
|
syntax val (-_) "- %1" prec 2 2
|
|
syntax val ( * ) "%1 * %2" prec 3 3 2
|
|
syntax val (/) "%1 / %2" prec 3 3 2
|
|
syntax val (%) "%1 % %2" prec 3 3 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.int.Int32BV
|
|
prelude export "#include <stdint.h>"
|
|
interface export "#include <stdint.h>"
|
|
syntax val to_bv "%1" prec 0
|
|
syntax val of_bv "%1" prec 0
|
|
end
|
|
|
|
module mach.int.Int32GMP
|
|
|
|
syntax val bxor "%1 ^ %2" prec 9 9 8
|
|
|
|
end
|
|
|
|
module mach.int.UInt32Gen
|
|
|
|
prelude export "#include <stdint.h>"
|
|
interface export "#include <stdint.h>"
|
|
syntax type uint32 "uint32_t"
|
|
|
|
syntax val max_uint32 "0xffffffff" prec 0
|
|
syntax val length "32" prec 0
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.int.UInt16
|
|
|
|
prelude export "#include <stdint.h>"
|
|
interface export "#include <stdint.h>"
|
|
syntax type uint16 "uint16_t"
|
|
syntax literal uint16 "%cu"
|
|
|
|
syntax val (+) "%1 + %2" prec 4 4 3
|
|
syntax val (-) "%1 - %2" prec 4 4 3
|
|
syntax val (-_) "- %1" prec 2 2
|
|
syntax val ( * ) "%1 * %2" prec 3 3 2
|
|
syntax val (/) "%1 / %2" prec 3 3 2
|
|
syntax val (%) "%1 % %2" prec 3 3 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.int.UInt32BV
|
|
syntax val to_bv "%1" prec 0
|
|
syntax val of_bv "%1" prec 0
|
|
end
|
|
|
|
module mach.int.UInt32
|
|
|
|
prelude export "#include <stdint.h>"
|
|
interface export "#include <stdint.h>"
|
|
syntax literal uint32 "%cU"
|
|
|
|
syntax val (+) "%1 + %2" prec 4 4 3
|
|
syntax val (-) "%1 - %2" prec 4 4 3
|
|
syntax val (-_) "- %1" prec 2 2
|
|
syntax val ( * ) "%1 * %2" prec 3 3 2
|
|
syntax val (/) "%1 / %2" prec 3 3 2
|
|
syntax val (%) "%1 % %2" prec 3 3 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module ieee_float.Float64
|
|
|
|
syntax type t "double"
|
|
|
|
syntax val (.+) "%1 + %2" prec 4 4 3
|
|
syntax val (.-) "%1 - %2" prec 4 4 3
|
|
syntax val (.-_) "- %1" prec 2 2
|
|
syntax val (.*) "%1 * %2" prec 3 3 2
|
|
syntax val (./) "%1 / %2" prec 3 3 2
|
|
syntax val (.=) "%1 == %2" prec 7 7 6
|
|
syntax val (.<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (.<) "%1 < %2" prec 6 6 5
|
|
syntax val (.>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (.>) "%1 > %2" prec 6 6 5
|
|
syntax val eq "%1 == %2" prec 7 7 6
|
|
syntax val le "%1 <= %2" prec 6 6 5
|
|
syntax val lt "%1 < %2" prec 6 6 5
|
|
syntax val ge "%1 >= %2" prec 6 6 5
|
|
syntax val gt "%1 > %2" prec 6 6 5
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.int.UInt32GMP
|
|
|
|
interface "\
|
|
\nstruct __add32_with_carry_result {\
|
|
\n uint32_t __field_0;\
|
|
\n uint32_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstruct __add32_with_carry_result\
|
|
\nadd32_with_carry(uint32_t x, uint32_t y, uint32_t c);\
|
|
\n\
|
|
\nstruct __sub32_with_borrow_result {\
|
|
\n uint32_t __field_0;\
|
|
\n uint32_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstruct __sub32_with_borrow_result\
|
|
\nsub32_with_borrow(uint32_t x, uint32_t y, uint32_t b);\
|
|
\n\
|
|
\nstruct __mul32_double_result {\
|
|
\n uint32_t __field_0;\
|
|
\n uint32_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstruct __mul32_double_result\
|
|
\nmul32_double(uint32_t x, uint32_t y);\
|
|
\n\
|
|
\nstruct __add32_3_result {\
|
|
\n uint32_t __field_0;\
|
|
\n uint32_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstruct __add32_3_result\
|
|
\nadd32_3(uint32_t x, uint32_t y, uint32_t z);\
|
|
\n\
|
|
\nstruct __lsld32_result {\
|
|
\n uint32_t __field_0;\
|
|
\n uint32_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstruct __lsld32_result\
|
|
\nlsld32(uint32_t x, uint32_t cnt);\
|
|
"
|
|
|
|
syntax literal uint32 "%cU"
|
|
|
|
syntax val (+) "%1 + %2" prec 4 4 3
|
|
syntax val (-) "%1 - %2" prec 4 4 3
|
|
syntax val (-_) "- %1" prec 2 2
|
|
syntax val ( * ) "%1 * %2" prec 3 3 2
|
|
syntax val (/) "%1 / %2" prec 3 3 2
|
|
syntax val (%) "%1 % %2" prec 3 3 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
syntax val add_with_carry "add32_with_carry"
|
|
syntax val sub_with_borrow "sub32_with_borrow"
|
|
syntax val mul_double "mul32_double"
|
|
syntax val add3 "add32_3"
|
|
syntax val lsld "lsld32"
|
|
|
|
syntax val add_mod "%1 + %2" prec 4 4 3
|
|
syntax val sub_mod "%1 - %2" prec 4 4 3
|
|
syntax val minus_mod "- %1" prec 2 2
|
|
syntax val mul_mod "%1 * %2" prec 3 3 2
|
|
|
|
syntax val div2by1
|
|
"(uint32_t)((((uint64_t)%1) | (((uint64_t)%2) << 32))/(uint64_t)(%3))"
|
|
prec 2
|
|
|
|
syntax val lsl "%1 << %2" prec 5 5 2
|
|
syntax val lsr "%1 >> %2" prec 5 5 2
|
|
|
|
syntax val is_msb_set "%1 & 0x80000000U" prec 8 8
|
|
|
|
syntax val count_leading_zeros "__builtin_clz"
|
|
syntax val count_trailing_zeros "__builtin_ctz"
|
|
|
|
syntax val of_int32 "(uint32_t)%1" prec 2 2
|
|
syntax val to_int32 "(int32_t)%1" prec 2 2
|
|
|
|
end
|
|
|
|
blacklist "__builtin_clz" "__builtin_ctz" "add32_with_carry" "sub32_with_borrow"
|
|
blacklist "mul32_double" "add32_3" "lsld32"
|
|
|
|
module mach.int.Int64
|
|
|
|
syntax type int64 "int64_t"
|
|
syntax literal int64 "INT64_C(%c)"
|
|
|
|
syntax val (+) "%1 + %2" prec 4 4 3
|
|
syntax val (-) "%1 - %2" prec 4 4 3
|
|
syntax val (-_) "- %1" prec 2 2
|
|
syntax val ( * ) "%1 * %2" prec 3 3 2
|
|
syntax val (/) "%1 / %2" prec 3 3 2
|
|
syntax val (%) "%1 % %2" prec 3 3 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.int.UInt64Gen
|
|
|
|
prelude export "#include <stdint.h>"
|
|
interface export "#include <stdint.h>"
|
|
syntax type uint64 "uint64_t"
|
|
|
|
syntax val max_uint64 "0xffffffffffffffff" prec 0
|
|
syntax val length "64" prec 0
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.int.UInt64
|
|
|
|
syntax literal uint64 "UINT64_C(%c)"
|
|
|
|
syntax val (+) "%1 + %2" prec 4 4 3
|
|
syntax val (-) "%1 - %2" prec 4 4 3
|
|
syntax val (-_) "- %1" prec 2 2
|
|
syntax val ( * ) "%1 * %2" prec 3 3 2
|
|
syntax val (/) "%1 / %2" prec 3 3 2
|
|
syntax val (%) "%1 % %2" prec 3 3 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.int.UInt64GMP
|
|
|
|
interface "\
|
|
\nstruct __add64_with_carry_result {\
|
|
\n uint64_t __field_0;\
|
|
\n uint64_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstatic inline struct __add64_with_carry_result\
|
|
\nadd64_with_carry(uint64_t x, uint64_t y, uint64_t c)\
|
|
\n{\
|
|
\n struct __add64_with_carry_result result;\
|
|
\n uint64_t r = x + y + c;\
|
|
\n result.__field_0 = r;\
|
|
\n if (r == x) result.__field_1 = c;\
|
|
\n else result.__field_1 = (r < x);\
|
|
\n return result;\
|
|
\n}\
|
|
\n\
|
|
\nstruct __sub64_with_borrow_result {\
|
|
\n uint64_t __field_0;\
|
|
\n uint64_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstatic inline struct __sub64_with_borrow_result\
|
|
\nsub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)\
|
|
\n{\
|
|
\n struct __sub64_with_borrow_result result;\
|
|
\n uint64_t r = x - y - b;\
|
|
\n result.__field_0 = r;\
|
|
\n if (r > x) result.__field_1 = 1;\
|
|
\n else if (r == x) result.__field_1 = b;\
|
|
\n else result.__field_1 = 0;\
|
|
\n return result;\
|
|
\n}\
|
|
\n\
|
|
\nstruct __add64_3_result {\
|
|
\n uint64_t __field_0;\
|
|
\n uint64_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstatic inline struct __add64_3_result\
|
|
\nadd64_3(uint64_t x, uint64_t y, uint64_t z)\
|
|
\n{\
|
|
\n struct __add64_3_result result;\
|
|
\n uint64_t r, c1, c2;\
|
|
\n r = x + y;\
|
|
\n c1 = r < y;\
|
|
\n r += z;\
|
|
\n c2 = r < z;\
|
|
\n result.__field_1 = c1 + c2;\
|
|
\n result.__field_0 = r;\
|
|
\n return result;\
|
|
\n}\
|
|
\n\
|
|
\nstruct __lsld64_result {\
|
|
\n uint64_t __field_0;\
|
|
\n uint64_t __field_1;\
|
|
\n};\
|
|
\n\
|
|
\nstatic inline struct __lsld64_result\
|
|
\nlsld64(uint64_t x, uint64_t cnt)\
|
|
\n{\
|
|
\n struct __lsld64_result result;\
|
|
\n result.__field_1 = x >> (64 - cnt);\
|
|
\n result.__field_0 = x << cnt;\
|
|
\n return result;\
|
|
\n}\
|
|
"
|
|
|
|
syntax literal uint64 "UINT64_C(%c)"
|
|
|
|
syntax val uint64_max "0xffffffffffffffffUL" prec 0
|
|
|
|
syntax val (+) "%1 + %2" prec 4 4 3
|
|
syntax val (-) "%1 - %2" prec 4 4 3
|
|
syntax val (-_) "- %1" prec 2 2
|
|
syntax val ( * ) "%1 * %2" prec 3 3 2
|
|
syntax val (/) "%1 / %2" prec 3 3 2
|
|
syntax val (%) "%1 % %2" prec 3 3 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
syntax val add_with_carry "add64_with_carry"
|
|
syntax val sub_with_borrow "sub64_with_borrow"
|
|
syntax val add3 "add64_3"
|
|
syntax val lsld "lsld64"
|
|
|
|
syntax val add_mod "%1 + %2" prec 4 4 3
|
|
syntax val sub_mod "%1 - %2" prec 4 4 3
|
|
syntax val minus_mod "- %1" prec 2 2
|
|
syntax val mul_mod "%1 * %2" prec 3 3 2
|
|
|
|
syntax val lsl "%1 << %2" prec 5 5 2
|
|
syntax val lsr "%1 >> %2" prec 5 5 2
|
|
syntax val lsl_mod "%1 << %2" prec 5 5 2
|
|
syntax val lsr_mod "%1 >> %2" prec 5 5 2
|
|
|
|
syntax val is_msb_set "%1 & 0x8000000000000000UL" prec 8 7
|
|
|
|
syntax val count_leading_zeros "__builtin_clzll(%1)" prec 1 15
|
|
syntax val count_trailing_zeros "__builtin_ctzll(%1)" prec 1 15
|
|
|
|
syntax val to_int32 "(int32_t)%1" prec 2 2
|
|
syntax val of_int32 "(uint64_t)%1" prec 2 2
|
|
syntax val to_uint32 "(uint32_t)%1" prec 2 2
|
|
syntax val of_uint32 "(uint64_t)%1" prec 2 2
|
|
syntax val to_int64 "(int64_t)%1" prec 2 2
|
|
syntax val of_int64 "(uint64_t)%1" prec 2 2
|
|
|
|
syntax val of_int "%1" prec 0
|
|
|
|
end
|
|
|
|
blacklist "__builtin_clzll" "_builtin_ctzll" "add64_with_carry"
|
|
blacklist "sub64_with_borrow" "mul64_double" "add64_3" "lsld64"
|
|
|
|
module bv.BV32
|
|
syntax type t "uint32_t"
|
|
syntax literal t "%cu"
|
|
syntax val eq "%1 == %2" prec 7 7 6
|
|
syntax val bw_and "%1 & %2" prec 8 7 7
|
|
syntax val bw_or "%1 | %2" prec 10 10 9
|
|
syntax val bw_xor "%1 ^ %2" prec 9 9 8
|
|
syntax val bw_not "~ %1" prec 2 2
|
|
(* no extraction of lsr, asr, lsl, to_uint, of_int, to_int (use type `int`) *)
|
|
syntax val add "%1 + %2" prec 4 4 3
|
|
syntax val sub "%1 - %2" prec 4 4 3
|
|
syntax val neg "- %1" prec 2 2
|
|
syntax val mul "%1 * %2" prec 3 3 2
|
|
syntax val udiv "%1 / %2" prec 3 3 2
|
|
syntax val urem "%1 % %2" prec 3 3 2
|
|
syntax val lsr_bv "%1 >> %2" prec 5 5 2
|
|
syntax val asr_bv "%1 >> %2" prec 5 5 2
|
|
syntax val lsl_bv "%1 << %2" prec 5 5 2
|
|
end
|
|
|
|
module mach.array.Array32
|
|
|
|
syntax val ([]) "%1[%2]" prec 1 1 15
|
|
syntax val ([]<-) "%1[%2] = %3" prec 1 1 15 14
|
|
|
|
end
|
|
|
|
module bool.Bool
|
|
|
|
(* FIXME: use bitwise operators instead ? *)
|
|
(* requiring higher-than-needed precedence for arguments
|
|
avoids Wparentheses *)
|
|
syntax val orb "%1 || %2" prec 12 5 5
|
|
syntax val andb "%1 && %2" prec 11 5 5
|
|
syntax val xorb "%1 ^ %2" prec 9 5 5
|
|
syntax val notb "!%1" prec 2 2
|
|
|
|
end
|
|
|
|
module mach.c.C
|
|
|
|
interface "#include <stdlib.h>"
|
|
interface "#include <stdio.h>"
|
|
interface "#include <assert.h>"
|
|
interface "#include <alloca.h>"
|
|
interface
|
|
"#define IGNORE2(x,y) do { (void)(x); (void)(y); } while (0)"
|
|
interface
|
|
"#define IGNORE3(x,y,z) do { (void)(x); (void)(y); (void)(z); } while (0)"
|
|
|
|
syntax type ptr "%1 *"
|
|
syntax type bool "int"
|
|
|
|
syntax val malloc "malloc(%1 * sizeof(%v0))" prec 1 3
|
|
syntax val free "free"
|
|
syntax val realloc "realloc(%1, %2 * sizeof(%v0))" prec 1 15 3
|
|
|
|
syntax val salloc "alloca(%1 * sizeof(%v0))" prec 1 3
|
|
syntax val sfree "(void)%1" prec 2 2
|
|
|
|
(* syntax val is_null "(%1) == NULL" *)
|
|
syntax val is_not_null "%1" prec 0
|
|
syntax val null "NULL" prec 0
|
|
|
|
syntax val incr "%1 + %2" prec 4 4 3
|
|
|
|
syntax val get "*%1" prec 2 2
|
|
syntax val get_ofs "%1[%2]" prec 1 1 15
|
|
|
|
syntax val set "*%1 = %2" prec 14 2 14
|
|
syntax val set_ofs "%1[%2] = %3" prec 14 14 15 14
|
|
|
|
syntax val incr_split "%1 + %2" prec 4 4 3
|
|
syntax val decr_split "%1 - %2" prec 4 4 3
|
|
syntax val join "IGNORE2"
|
|
syntax val join_r "IGNORE2"
|
|
|
|
syntax val c_assert "assert (%1)" prec 1 15
|
|
|
|
syntax val print_space "printf(\" \")" prec 1
|
|
syntax val print_newline "printf(\"\\n\")" prec 1
|
|
syntax val print_uint32 "printf(\"%#010x\",%1)" prec 1 15
|
|
|
|
end
|
|
|
|
blacklist "printf" "alloca"
|
|
|
|
module mach.c.UChar
|
|
|
|
syntax literal uchar "%c"
|
|
syntax type uchar "unsigned char"
|
|
syntax val of_uint64 "(unsigned char)%1" prec 2 2
|
|
syntax val to_uint64 "(uint64_t)%1" prec 2 2
|
|
syntax val of_int32 "(unsigned char)%1" prec 2 2
|
|
syntax val to_int32 "(int32_t)%1" prec 2 2
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
syntax val of_char "(unsigned char)%1" prec 2 2
|
|
syntax val to_char "(char)%1" prec 2 2
|
|
|
|
syntax val open_from_charptr "(unsigned char *)%1" prec 2 2
|
|
syntax val close_from_charptr "IGNORE2"
|
|
|
|
remove module
|
|
|
|
end
|
|
|
|
module mach.c.SChar
|
|
|
|
syntax literal schar "%c"
|
|
syntax type schar "signed char"
|
|
syntax val (<=) "%1 <= %2" prec 6 6 5
|
|
syntax val (<) "%1 < %2" prec 6 6 5
|
|
syntax val (>=) "%1 >= %2" prec 6 6 5
|
|
syntax val (>) "%1 > %2" prec 6 6 5
|
|
|
|
end
|
|
|
|
module string.Char
|
|
|
|
syntax type char "char"
|
|
|
|
end
|
|
|
|
module mach.c.String
|
|
|
|
prelude export "#include <string.h>"
|
|
interface export "#include <string.h>"
|
|
syntax type string "char *"
|
|
|
|
syntax val get "%1[%2]" prec 1 1 15
|
|
syntax val zero_char "'\\0'" prec 0
|
|
syntax val zero_num "'0'" prec 0
|
|
syntax val nine_num "'9'" prec 0
|
|
syntax val small_a "'a'" prec 0
|
|
syntax val small_z "'z'" prec 0
|
|
syntax val big_a "'A'" prec 0
|
|
syntax val big_z "'Z'" prec 0
|
|
syntax val minus_char "'-'" prec 0
|
|
syntax val code "%1" prec 0
|
|
syntax val length "strlen"
|
|
syntax val strlen "strlen"
|
|
syntax val (=) "%1 == %2" prec 7 7 6
|
|
|
|
end
|
|
|
|
module mach.fxp.Fxp
|
|
|
|
syntax val fxp_add "%1 + %2" prec 4 4 3
|
|
syntax val fxp_sub "%1 - %2" prec 4 4 3
|
|
syntax val fxp_mul "%1 * %2" prec 3 3 2
|
|
syntax val fxp_lsl "%1 << %2" prec 5 5 2
|
|
syntax val fxp_lsr "%1 >> %2" prec 5 5 2
|
|
syntax val fxp_asr "(uint64_t)((int64_t)%1 >> %2)" prec 2 1 2
|
|
syntax val fxp_asr' "(uint64_t)((int64_t)%1 >> %2)" prec 2 1 2
|
|
|
|
end
|
|
|
|
(* exclude some stdlib modules from extraction *)
|
|
|
|
module array.Array
|
|
remove module
|
|
end
|
|
|
|
module bool.Bool
|
|
remove module
|
|
end
|
|
|
|
module map.Map
|
|
remove module
|
|
end
|
|
|
|
module map.Const
|
|
remove module
|
|
end
|
|
|
|
module number.Divisibility
|
|
remove module
|
|
end
|
|
|
|
module int.Int
|
|
remove module
|
|
end
|
|
|
|
module int.Abs
|
|
remove module
|
|
end
|
|
|
|
module int.ComputerDivision
|
|
remove module
|
|
end
|
|
|
|
module int.EuclideanDivision
|
|
remove module
|
|
end
|
|
|
|
module int.MinMax
|
|
remove module
|
|
end
|
|
|
|
module int.Power
|
|
remove module
|
|
end
|
|
|
|
module real.Real
|
|
remove module
|
|
end
|
|
|
|
module real.ExpLog
|
|
remove module
|
|
end
|
|
|
|
module real.RealInfix
|
|
remove module
|
|
end
|
|
|
|
module real.Square
|
|
remove module
|
|
end
|
|
|
|
module mach.int.Unsigned
|
|
remove module
|
|
end
|