Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
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
c65114a3
Commit
c65114a3
authored
Jul 13, 2021
by
Stefan Gränitz
Browse files
Drop a few warnings and default definitions from the test suite
parent
4528105e
Pipeline
#36513
failed with stages
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
tests/stl/oracle/stl_functional.res.oracle
View file @
c65114a3
...
...
@@ -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 @
c65114a3
...
...
@@ -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);
...
...
@@ -1680,12 +1696,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 @
c65114a3
[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
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