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
d9d05e18
Commit
d9d05e18
authored
Jul 13, 2021
by
Stefan Gränitz
Committed by
Virgile Prevosto
Apr 05, 2022
Browse files
Drop a few warnings and default definitions from the test suite
parent
d2210718
Changes
3
Hide whitespace changes
Inline
Side-by-side
tests/stl/oracle/stl_functional.res.oracle
View file @
d9d05e18
...
...
@@ -5,8 +5,6 @@ Now output intermediate result
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function exception::Ctor can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function forward<std::minus<int>> can't throw any exception
[kernel] Warning: Assuming declared function forward<std::plus<int>> can't throw any exception
/* Generated by Frama-C */
struct _frama_c_vmt_content {
void (*method_ptr)() ;
...
...
@@ -278,11 +276,17 @@ int *forward<int>(type *t)
/*@ requires \valid(t);
ensures \valid(\result); */
struct minus<int> *forward<std::minus<int>>(type *t);
struct minus<int> *forward<std::minus<int>>(type *t)
{
return t;
}
/*@ requires \valid(t);
ensures \valid(\result); */
struct plus<int> *forward<std::plus<int>>(type *t);
struct plus<int> *forward<std::plus<int>>(type *t)
{
return t;
}
/*@ requires \valid(t);
ensures \valid_read(\result); */
...
...
tests/stl/oracle/stl_memory.res.oracle
View file @
d9d05e18
...
...
@@ -11,9 +11,6 @@ Now output intermediate result
[kernel] Warning: Assuming declared function free can't throw any exception
[kernel] Warning: Assuming declared function free can't throw any exception
[kernel] Warning: Assuming declared function free can't throw any exception
[kernel] Warning: Assuming declared function swap<std::default_delete<int>> can't throw any exception
[kernel] Warning: Assuming declared function forward<std::default_delete<int[]>> can't throw any exception
[kernel] Warning: Assuming declared function forward<std::default_delete<int[]>> can't throw any exception
[kernel] Warning: Assuming declared function exception::Ctor can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function malloc can't throw any exception
...
...
@@ -21,8 +18,6 @@ Now output intermediate result
[kernel] Warning: Assuming declared function malloc can't throw any exception
[kernel] Warning: Assuming declared function malloc can't throw any exception
[kernel] Warning: Assuming declared function malloc can't throw any exception
[kernel] Warning: Assuming declared function forward<std::unique_ptr<int[],std::default_delete<int[]>>> can't throw any exception
[kernel] Warning: Assuming declared function forward<std::unique_ptr<int[],std::default_delete<int[]>>> can't throw any exception
/* Generated by Frama-C */
struct _frama_c_vmt_content {
void (*method_ptr)() ;
...
...
@@ -290,19 +285,40 @@ void swap<int*>(int **a, int **b)
return;
}
struct default_delete<int> *operator=(struct default_delete<int> *this,
struct default_delete<int> const *__frama_c_arg_0);
void default_delete<int>::Ctor(struct default_delete<int> const *this,
struct default_delete<int> const *__frama_c_arg_0);
/*@ requires \valid(b);
requires \valid(a); */
void swap<std::default_delete<int>>(struct default_delete<int> *a,
struct default_delete<int> *b);
struct default_delete<int> *b)
{
struct default_delete<int> *tmp_0;
struct default_delete<int> *tmp_1;
struct default_delete<int> tmp;
default_delete<int>::Ctor(& tmp,(struct default_delete<int> const *)a);
tmp_0 = operator=(a,(struct default_delete<int> const *)b);
tmp_1 = operator=(b,(struct default_delete<int> const *)(& tmp));
return;
}
/*@ requires \valid(t);
ensures \valid(\result); */
struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>
(type *t);
(type *t)
{
return t;
}
/*@ requires \valid(t);
ensures \valid(\result); */
struct default_delete<int[]> *forward<std::default_delete<int[]>>(type *t);
struct default_delete<int[]> *forward<std::default_delete<int[]>>(type *t)
{
return t;
}
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this);
...
...
@@ -1697,12 +1713,6 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.pvmt = (struct _frama_c_vmt *)0};
void default_delete<int>::Ctor(struct default_delete<int> const *this);
void default_delete<int>::Ctor(struct default_delete<int> const *this,
struct default_delete<int> const *__frama_c_arg_0);
struct default_delete<int> *operator=(struct default_delete<int> *this,
struct default_delete<int> const *__frama_c_arg_0);
void default_delete<int>::Dtor(struct default_delete<int> const *this);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
...
...
tests/stl/oracle/stl_utility.res.oracle
View file @
d9d05e18
[kernel] Parsing tests/stl/stl_utility.cpp (external front-end)
Now output intermediate result
[kernel] Warning: Assuming declared function operator><S> can't throw any exception
/* Generated by Frama-C */
struct _frama_c_vmt_content {
void (*method_ptr)() ;
...
...
@@ -622,9 +621,16 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
_Bool operator<(struct S const *x, struct S const *y);
/*@ requires \valid_read(y);
requires \valid_read(x); */
_Bool operator><S>(struct S const *x, struct S const *y);
_Bool operator><S>(struct S const *x, struct S const *y)
{
_Bool tmp;
tmp = operator<(y,x);
return tmp;
}
/*@ requires \valid(b);
requires \valid(a); */
...
...
Write
Preview
Supports
Markdown
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