"tests/git@git.frama-c.com:pub/frama-c.git" did not exist on "82c8bd8bcfad7c7c4a6868356a02ba9a4672ba1a"
Incorrect representation of std::true_type::value after C++-C translation
Steps to reproduce the issue
#include <type_traits>
int success = 0, failure = 1;
int main(){
return std::true_type::value ? success : failure;
}
> frama-c -deps -print value_fails.cpp
Expected output
...
[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 main:
\result FROM value; success
[from] ====== END OF DEPENDENCIES ======
/* Generated by Frama-C */
...
_Bool const value = (_Bool)1;
...
int success = 0;
int failure = 1;
int main(void)
{
int tmp;
if (value) tmp = success; else tmp = failure;
return tmp;
}
Actual output
...
[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 main:
\result FROM value; success; failure
[from] ====== END OF DEPENDENCIES ======
/* Generated by Frama-C */
...
extern _Bool const value;
...
int success = 0;
int failure = 1;
int main(void)
{
int tmp;
/*@ assert Eva: bool_value: value ≡ 0 ∨ value ≡ 1; */
if (value) tmp = success; else tmp = failure;
return tmp;
}
Minimal working diff
It works if the type of the static data member value is bool (or any other explicit type) instead of type T.
template <class T, T v> struct integral_constant {
-static constexpr T value = v;
+static constexpr bool value = v;
Contextual information
- Frama-C: 22.0
- Frama-Clang: 0.0.10
- Clang: 11.1.0
- Target: x86_64-pc-linux-gnu