GitLab

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