diff --git a/tests/basic/oracle/underlying_type.res.oracle b/tests/basic/oracle/underlying_type.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..fb792c5a9475e60ff3be166184b1b544506eab48 --- /dev/null +++ b/tests/basic/oracle/underlying_type.res.oracle @@ -0,0 +1,122 @@ +[kernel] Parsing tests/basic/underlying_type.cpp (external front-end) +Now output intermediate result +/* Generated by Frama-C */ +struct _frama_c_vmt_content { + void (*method_ptr)() ; + int shift_this ; +}; +struct _frama_c_rtti_name_info_node; +struct _frama_c_vmt { + struct _frama_c_vmt_content *table ; + int table_size ; + struct _frama_c_rtti_name_info_node *rtti_info ; +}; +struct _frama_c_rtti_name_info_content { + struct _frama_c_rtti_name_info_node *value ; + int shift_object ; + int shift_vmt ; +}; +struct _frama_c_rtti_name_info_node { + char const *name ; + struct _frama_c_rtti_name_info_content *base_classes ; + int number_of_base_classes ; + struct _frama_c_vmt *pvmt ; +}; +typedef _Bool value_type; +struct integral_constant<bool,0>; +struct integral_constant<bool,0> { + +}; +typedef _Bool value_type; +struct integral_constant<bool,1>; +struct integral_constant<bool,1> { + +}; +enum E { + A = 1, + B = 2 +}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +/*@ requires \valid_read(this); */ +value_type value_type)(struct integral_constant<bool,0> const *this); + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "integral_constant", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +/*@ requires \valid_read(this); */ +value_type value_type)(struct integral_constant<bool,1> const *this); + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "integral_constant", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "__boolean", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "__boolean", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "_is_void", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "is_enum", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "ok_type", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "ko_type", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "__underlying_type_t", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "underlying_type", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +int f(void) +{ + int __retres; + __retres = (int)((enum E)A); + return __retres; +} + + diff --git a/tests/basic/underlying_type.cpp b/tests/basic/underlying_type.cpp new file mode 100644 index 0000000000000000000000000000000000000000..679b844ff3e4655c47e573a124f980af6732f6e3 --- /dev/null +++ b/tests/basic/underlying_type.cpp @@ -0,0 +1,7 @@ +#include <type_traits> + +enum class E : int { A = 1, B = 2 }; + +int f() { + return static_cast<std::underlying_type<E>::type>(E::A); +}