From 2b51fac8f36c672c63dcffa885e709037c754ff3 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 28 May 2021 20:27:22 +0200
Subject: [PATCH] [tests] test new feature
---
tests/basic/oracle/underlying_type.res.oracle | 122 ++++++++++++++++++
tests/basic/underlying_type.cpp | 7 +
2 files changed, 129 insertions(+)
create mode 100644 tests/basic/oracle/underlying_type.res.oracle
create mode 100644 tests/basic/underlying_type.cpp
diff --git a/tests/basic/oracle/underlying_type.res.oracle b/tests/basic/oracle/underlying_type.res.oracle
new file mode 100644
index 0000000..fb792c5
--- /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 0000000..679b844
--- /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);
+}
--
GitLab