Commit 4c45b906 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'wip-frama-c-2564' into stable/chromium

merges pub/frama-clang!2 and fixes pub/frama-c#2564
parents 238ddd72 a7d772c9
......@@ -7426,6 +7426,7 @@ bool FramacVisitor::VisitFunctionDecl(clang::FunctionDecl* Decl) {
qual->decl_name = name;
free_decl_or_impl_name(decl_name);
decl_name = decl_or_impl_name_Implementation(qual);
copyFunc->cons_translation_unit_decl.Function.fun_name = decl_name;
};
_tableForWaitingDeclarations.addIncompleteFunction(Decl,
waitDeclarations, copyFunc);
......
/* run.config
OPT: @CXX@ @MACHDEP@ -print -deps
*/
// 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 5): 100% 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 ;
};
struct Foo *func<Foo>(struct Foo *foo, int x);
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)() ;
......@@ -276,12 +274,8 @@ int *forward<int>(type *t)
return t;
}
/*@ requires \valid(t);
ensures \valid(\result); */
struct minus<int> *forward<std::minus<int>>(type *t);
/*@ requires \valid(t);
ensures \valid(\result); */
struct plus<int> *forward<std::plus<int>>(type *t);
/*@ requires \valid(t);
......
......@@ -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,18 +285,12 @@ void swap<int*>(int **a, int **b)
return;
}
/*@ requires \valid(b);
requires \valid(a); */
void swap<std::default_delete<int>>(struct default_delete<int> *a,
struct default_delete<int> *b);
/*@ 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);
/*@ requires \valid(t);
ensures \valid(\result); */
struct default_delete<int[]> *forward<std::default_delete<int[]>>(type *t);
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this);
......
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,8 +621,6 @@ 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};
/*@ requires \valid_read(y);
requires \valid_read(x); */
_Bool operator><S>(struct S const *x, struct S const *y);
/*@ requires \valid(b);
......
/* run.config
STDOPT: #"-deps"
*/
#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
}
Supports Markdown
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