diff --git a/tests/spec/logic_type.c b/tests/spec/logic_type.c index 0b8380d9dc8b4db0c54999da8158c97fa4860dca..008bec88b3cfccc932e2acee9028e9b07b33aa4c 100644 --- a/tests/spec/logic_type.c +++ b/tests/spec/logic_type.c @@ -26,3 +26,11 @@ Point tab[3]; void h(void) { f(tab) ; } + +//@ logic t t_from_t(t x) = (t) x; + +//@ logic _Bool _Bool_from_boolean(boolean b) = (_Bool) b; + +//@ logic boolean boolean_from_integer(integer b) = (boolean) b; +//@ logic boolean boolean_from_int(int b) = (boolean) b; +//@ logic boolean boolean_from_Bool(_Bool b) = (boolean) b; diff --git a/tests/spec/oracle/logic_type.res.oracle b/tests/spec/oracle/logic_type.res.oracle index 4521f06fa5f83b07057e401646a935c01cf0979d..c9a81bc49b728a56715e384d78c293436da2aab8 100644 --- a/tests/spec/oracle/logic_type.res.oracle +++ b/tests/spec/oracle/logic_type.res.oracle @@ -51,4 +51,15 @@ void h(void) return; } +/*@ logic t t_from_t(t x) = x; + */ +/*@ logic _Bool _Bool_from_boolean(𔹠b) = (_Bool)b; + */ +/*@ logic 𔹠boolean_from_integer(ℤ b) = b; + */ +/*@ logic 𔹠boolean_from_int(int b) = b; + */ +/*@ logic 𔹠boolean_from_Bool(_Bool b) = b; + +*/