Commit 4d7d28d5 authored by Stefan Gränitz's avatar Stefan Gränitz
Browse files

Fix std::move for std::unique_ptr with non-primitive payloads

parent 0fe328bf
......@@ -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, copyFunc);
waitDeclarations, func);
isGenerationEffective = false;
}
};
......
/* 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();
}
[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;
}
......@@ -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); */
......
......@@ -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;
......
This diff is collapsed.
[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); */
......
/* 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
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment