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
e22b32aa
Commit
e22b32aa
authored
Jul 08, 2021
by
Stefan Gränitz
Browse files
Fix std::move for std::unique_ptr with non-primitive payloads
parent
59a2f1d4
Pipeline
#36535
failed with stages
Changes
8
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
ClangVisitor.cpp
View file @
e22b32aa
...
...
@@ -7392,25 +7392,42 @@ bool FramacVisitor::VisitFunctionDecl(clang::FunctionDecl* Decl) {
if
(
isInstance
&&
Decl
->
getPrimaryTemplate
())
_clangUtils
->
popTemplateInstance
(
Decl
->
getPrimaryTemplate
());
if
(
!
waitDeclarations
.
empty
())
{
func
->
cons_translation_unit_decl
.
Function
.
body
=
opt_none
();
translation_unit_decl
copyFunc
=
translation_unit_decl_dup
(
func
);
free
(
copyFunc
->
cons_translation_unit_decl
.
Function
.
body
);
copyFunc
->
cons_translation_unit_decl
.
Function
.
body
=
body
;
//
// The code below was commented out in order to allow analysis for a
// widely used C++ construct. For the moment, it might be useful to
// leave it here, so the approach can be revisited easily. Please find
// more details in the bugtracker:
// https://git.frama-c.com/pub/frama-c/-/issues/2564
//
// It appears that it was the intention to avoid duplicate definitions
// in the output AST and instead only emit declarations for first
// occurences. However, this also caused the frama-c engine to
// generate default definitions for such first occurences and ignore
// the actual implementations later on.
//
// The duplicate definitions don't seem harmful and the test suite
// still works well. Analysis will use only one of them and report
// the other one as uncovered.
//
//func->cons_translation_unit_decl.Function.body = opt_none();
//translation_unit_decl copyFunc = translation_unit_decl_dup(func);
//free(copyFunc->cons_translation_unit_decl.Function.body);
//copyFunc->cons_translation_unit_decl.Function.body = body;
if
(
_parents
.
hasLexicalContext
()
&&
!
_parents
.
isClass
())
_parents
.
add
(
func
);
else
{
_globals
.
insertContainer
(
func
);
};
if
(
decl_name
->
tag_decl_or_impl_name
==
DECLARATION
)
{
decl_name
->
cons_decl_or_impl_name
.
Declaration
.
name
=
strdup
(
""
);
qualified_name
qual
=
_clangUtils
->
makeQualifiedName
(
*
Decl
);
free
(
const_cast
<
char
*>
(
qual
->
decl_name
));
qual
->
decl_name
=
name
;
free_decl_or_impl_name
(
decl_name
);
decl_name
=
decl_or_impl_name_Implementation
(
qual
);
};
//
if (decl_name->tag_decl_or_impl_name == DECLARATION) {
//
decl_name->cons_decl_or_impl_name.Declaration.name = strdup("");
//
qualified_name qual = _clangUtils->makeQualifiedName(*Decl);
//
free(const_cast<char*>(qual->decl_name));
//
qual->decl_name = name;
//
free_decl_or_impl_name(decl_name);
//
decl_name = decl_or_impl_name_Implementation(qual);
//
};
_tableForWaitingDeclarations
.
addIncompleteFunction
(
Decl
,
waitDeclarations
,
copyF
unc
);
waitDeclarations
,
f
unc
);
isGenerationEffective
=
false
;
}
};
...
...
tests/bugs/issue2564.cpp
0 → 100644
View file @
e22b32aa
/* run.config
OPT: @MACHDEP@ -deps -print
*/
// Function func should be analysed based on its source definition. Generating
// definitions with default assigns for it caused the misbehavior described in
// the bug report:
// https://git.frama-c.com/pub/frama-c/-/issues/2564
//
// Required preconditions that triggered the misbehavior:
// - function must be a template
// - function must be declared before the class used as template parameter
// - function must access a template member
// - function must be defined in a namespace
//
namespace
test
{
template
<
class
T
>
T
*
func
(
T
*
foo
,
int
x
)
{
foo
->
add
(
x
);
return
foo
;
}
}
struct
Foo
{
int
val
=
0
;
int
get
()
{
return
val
;
}
void
add
(
int
x
)
{
val
=
x
;
}
};
int
main
(
int
argc
,
char
**
argv
)
{
Foo
foo
;
foo
.
add
(
argc
);
return
test
::
func
(
&
foo
,
argc
)
->
get
();
}
tests/bugs/oracle/issue2564.res.oracle
0 → 100644
View file @
e22b32aa
[kernel] Parsing tests/bugs/issue2564.cpp (external front-end)
Now output intermediate result
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
_frama_c_rtti_name_info.name ∈ {{ "Foo" }}
{.base_classes; .number_of_base_classes; .pvmt} ∈
{0}
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
5 functions analyzed (out of 6): 83% coverage.
In these functions, 12 statements reached (out of 12): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
0 alarms generated by the analysis.
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 0 valid 0 unknown 0 invalid 0 total
Preconditions 4 valid 0 unknown 0 invalid 4 total
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[from] Computing for function add
[from] Done for function add
[from] Computing for function get
[from] Done for function get
[from] Computing for function Foo::Ctor
[from] Done for function Foo::Ctor
[from] Computing for function func<Foo>
[from] Done for function func<Foo>
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function add:
foo FROM this; x
[from] Function get:
\result FROM this; foo
[from] Function Foo::Ctor:
NO EFFECTS
[from] Function func<Foo>:
foo FROM foo; x
\result FROM foo
[from] Function main:
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
/* 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 ;
};
struct Foo;
struct Foo {
int val ;
};
void add(struct Foo *this, int x);
struct Foo *func<Foo>(struct Foo *foo, int x)
{
add(foo,x);
return foo;
}
void Foo::Ctor(struct Foo const *this);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid(this); */
int get(struct Foo *this)
{
int __retres;
__retres = this->val;
return __retres;
}
/*@ requires \valid(this); */
void add(struct Foo *this, int x)
{
this->val = x;
return;
}
/*@ requires \valid_read(this); */
void Foo::Ctor(struct Foo const *this)
{
return;
}
struct Foo *func<Foo>(struct Foo *foo, int x)
{
add(foo,x);
return foo;
}
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "Foo",
.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_0;
struct Foo *tmp;
struct Foo foo;
Foo::Ctor(& foo);
add(& foo,argc);
tmp = func<Foo>(& foo,argc);
tmp_0 = get(tmp);
return tmp_0;
}
tests/stl/oracle/stl_functional.res.oracle
View file @
e22b32aa
...
...
@@ -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 @
e22b32aa
...
...
@@ -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_unique_ptr.res.oracle
0 → 100644
View file @
e22b32aa
This diff is collapsed.
Click to expand it.
tests/stl/oracle/stl_utility.res.oracle
View file @
e22b32aa
[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); */
...
...
tests/stl/stl_unique_ptr.cpp
0 → 100644
View file @
e22b32aa
/* run.config
OPT: @MACHDEP@ -deps -print
*/
#include <memory>
int
test_primitive_payload
(
int
var
)
{
std
::
unique_ptr
<
int
>
up1
(
&
var
);
std
::
unique_ptr
<
int
>
up2
(
new
int
);
*
up1
=
var
;
*
up2
=
2
;
std
::
swap
(
up1
,
up2
);
up1
.
reset
();
std
::
unique_ptr
<
int
[]
>
up3
(
new
int
[
2
]);
up3
[
0
]
=
*
up2
;
// var
up3
[
1
]
=
up3
[
0
]
+
1
;
int
*
up2_raw
=
up2
.
release
();
if
(
up2_raw
!=
&
var
)
{
delete
up2_raw
;
// unreachable
return
0
;
}
std
::
unique_ptr
<
int
[]
>
up4
=
std
::
move
(
up3
);
std
::
unique_ptr
<
int
[]
>
up5
=
std
::
forward
<
std
::
unique_ptr
<
int
[]
>>
(
up4
);
int
*
up5_raw
=
up5
.
release
();
int
result
=
up5_raw
[
0
];
delete
[]
up5_raw
;
return
result
;
}
struct
PlainOldStruct
{
int
val
=
0
;
int
pull
()
{
return
val
;
}
void
push
(
int
x
)
{
val
=
x
;
}
};
int
test_struct_payload
(
int
var
)
{
PlainOldStruct
pos
;
std
::
unique_ptr
<
PlainOldStruct
>
up1
(
&
pos
);
std
::
unique_ptr
<
PlainOldStruct
>
up2
(
new
PlainOldStruct
);
up1
->
push
(
var
);
up2
->
push
(
up1
->
pull
()
+
1
);
std
::
swap
(
up1
,
up2
);
up1
.
reset
();
std
::
unique_ptr
<
PlainOldStruct
>
up3
=
std
::
move
(
up2
);
std
::
unique_ptr
<
PlainOldStruct
>
up4
=
std
::
forward
<
std
::
unique_ptr
<
PlainOldStruct
>>
(
up3
);
int
result
=
up4
->
pull
();
PlainOldStruct
*
up4_raw
=
up4
.
release
();
if
(
up4_raw
!=
&
pos
)
{
delete
up4_raw
;
// unreachable
return
0
;
}
return
result
;
}
// Declaration before use.
template
<
typename
T
,
int
N
=
0
>
class
ClassTemplate
{
private:
T
val
=
N
;
public:
T
*
pull
();
void
push
(
T
*
x
);
};
// Use of declared ClassTemplate.
int
test_template_payload
(
int
var
)
{
ClassTemplate
<
int
>
ct
;
std
::
unique_ptr
<
ClassTemplate
<
int
>>
up1
(
&
ct
);
std
::
unique_ptr
<
ClassTemplate
<
int
,
0
>>
up2
(
new
ClassTemplate
<
int
,
0
>
);
up1
->
push
(
&
var
);
std
::
swap
(
up1
,
up2
);
up1
.
reset
();
std
::
unique_ptr
<
ClassTemplate
<
int
>>
up3
=
std
::
move
(
up2
);
std
::
unique_ptr
<
ClassTemplate
<
int
>>
up4
=
std
::
forward
<
std
::
unique_ptr
<
ClassTemplate
<
int
>>>
(
up3
);
int
result
=
*
up4
->
pull
();
// var
ClassTemplate
<
int
>
*
up4_raw
=
up4
.
release
();
if
(
up4_raw
!=
&
ct
)
{
delete
up4_raw
;
// unreachable
return
0
;
}
return
result
;
}
// Definitions after use.
template
<
typename
T
,
int
N
>
T
*
ClassTemplate
<
T
,
N
>::
pull
()
{
return
&
val
;
}
template
<
typename
T
,
int
N
>
void
ClassTemplate
<
T
,
N
>::
push
(
T
*
x
)
{
val
=
*
x
;
}
// Driver loops through the input argc.
int
main
(
int
argc
,
char
*
argv
[])
{
int
t1
=
test_primitive_payload
(
argc
);
int
t2
=
test_struct_payload
(
t1
);
int
t3
=
test_template_payload
(
t2
);
return
t3
;
// Expecting output: \result FROM argc
}
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