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
402d8578
Commit
402d8578
authored
Jul 08, 2021
by
Stefan Gränitz
Committed by
Virgile Prevosto
Apr 05, 2022
Browse files
[WIP] Fix recognition of certain functions with r-value return types
parent
238ddd72
Changes
2
Hide whitespace changes
Inline
Side-by-side
tests/bugs/issue2564.cpp
0 → 100644
View file @
402d8578
/* run.config
OPT: @MACHDEP@ -deps
*/
struct
Foo
;
namespace
test
{
// Implementations of the two functions works() and fails() are equivalent.
// Their invocations from main() are equivalent as well. The only difference
// is that fails() gets DECLARED here, i.e. before its r-value return type got
// DEFINED. Commenting out this declaration avoids the problem.
//
// All known preconditions:
// * function must be a template
// * function must be in a namespace
// * function must return an r-value reference
// * function must be declared before the return type is defined
//
// This seems to be the root cause for misbehaviors of std::forward<T>() and
// std::move() on std::unique_ptr instances.
//
template
<
class
X
>
Foo
&&
fails
(
Foo
*
foo
,
X
x
);
}
struct
Foo
{
int
val
=
0
;
int
get
()
{
return
val
;
}
void
add
(
int
x
)
{
val
=
x
;
}
};
namespace
test
{
template
<
class
X
>
Foo
&&
works
(
Foo
*
foo
,
X
x
)
{
foo
->
add
(
x
);
return
static_cast
<
Foo
&&>
(
*
foo
);
}
template
<
class
X
>
Foo
&&
fails
(
Foo
*
foo
,
X
x
)
{
foo
->
add
(
x
);
return
static_cast
<
Foo
&&>
(
*
foo
);
}
}
int
main
(
int
argc
,
char
**
argv
)
{
Foo
foo
;
int
a
=
test
::
works
(
&
foo
,
argc
).
get
();
int
b
=
test
::
fails
(
&
foo
,
argc
).
get
();
return
a
+
b
;
}
tests/bugs/oracle/issue2564.res.oracle
0 → 100644
View file @
402d8578
[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:alarm] tests/bugs/issue2564.cpp:47: Warning:
signed overflow. assert -2147483648 ≤ a + b;
[eva:alarm] tests/bugs/issue2564.cpp:47: Warning:
signed overflow. assert a + b ≤ 2147483647;
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
6 functions analyzed (out of 6): 100% coverage.
In these functions, 18 statements reached (out of 18): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
2 alarms generated by the analysis:
2 integer overflows
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 0 valid 0 unknown 0 invalid 0 total
Preconditions 5 valid 0 unknown 0 invalid 5 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 fails<int>
[from] Done for function fails<int>
[from] Computing for function works<int>
[from] Done for function works<int>
[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 fails<int>:
foo FROM foo; x
\result FROM foo
[from] Function works<int>:
foo FROM foo; x
\result FROM foo
[from] Function main:
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
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