Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Stefan Gränitz
Frama Clang
Commits
3ac7c020
Commit
3ac7c020
authored
Aug 10, 2021
by
Stefan Gränitz
Browse files
[WIP] Add tests for ratio header (results not gratifying yet)
parent
d47cfdaf
Pipeline
#37173
failed with stages
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
tests/stl/oracle/stl_ratio.res.oracle
0 → 100644
View file @
3ac7c020
[kernel] Parsing tests/stl/stl_ratio.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 long long intmax_t;
typedef intmax_t intmax_t;
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> {
};
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;
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 =
{.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_gcd",
.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 = "__static_abs",
.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 = "__static_abs",
.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 = "__static_abs",
.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 = "__static_abs",
.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 = "__static_abs",
.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 = "__static_abs",
.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 = "__static_abs",
.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 = "__static_sign",
.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 = "__static_sign",
.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 = "__static_sign",
.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 = "__static_sign",
.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 = "__static_sign",
.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 = "__static_sign",
.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 = "__static_sign",
.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 = "__ll_add",
.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 = "__ll_mul",
.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 = "__ll_mul",
.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 = "__ll_mul",
.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 = "__ll_mul",
.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 = "__ll_mul",
.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;
extern intmax_t const num;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "ratio",
.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 = "ratio",
.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 = "ratio",
.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 = "ratio",
.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;
extern intmax_t const num;
extern intmax_t const den;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "ratio",
.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 = "__ratio_multiply",
.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 = "__ratio_add",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
int main(int argc, char **argv)
{
int tmp;
if (((num - num) - den) + (long long)argc == (long long)990) tmp = 0;
else tmp = 1;
return tmp;
}
\ No newline at end of file
tests/stl/stl_ratio.cpp
0 → 100644
View file @
3ac7c020
#include <ratio>
int
main
(
int
argc
,
char
*
argv
[])
{
using
one_third
=
std
::
ratio
<
1
,
3
>
;
using
two_fourths
=
std
::
ratio
<
2
,
4
>
;
using
five_sixth
=
std
::
ratio_add
<
one_third
,
two_fourths
>
;
return
(
std
::
kilo
::
num
-
five_sixth
::
num
-
five_sixth
::
den
+
argc
==
990
)
?
0
:
1
;
}
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment
