frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-10-06T07:49:50Zhttps://git.frama-c.com/pub/frama-c/-/issues/2546Problems with a simplest Arduino program, that contain only "Arduino.h" include.2021-10-06T07:49:50ZvarosiProblems with a simplest Arduino program, that contain only "Arduino.h" include.Hello!
I'm trying to evaluate if Frama-C could be used for verification of embedded software.
I have a simple program which just include "Arduino.h".
I run this commands:
```
export FC_COMPILER=$'-Os -mlong-calls -falign-functions=4 -...Hello!
I'm trying to evaluate if Frama-C could be used for verification of embedded software.
I have a simple program which just include "Arduino.h".
I run this commands:
```
export FC_COMPILER=$'-Os -mlong-calls -falign-functions=4 -U__STRICT_ANSI__ -ffunction-sections -fdata-sections -fno-exceptions -DPLATFORMIO=50101 -DESP8266 -DARDUINO_ARCH_ESP8266 -DARDUINO_ESP8266_ESP12 -DF_CPU=160000000L -D__ets__ -DICACHE_FLASH -DARDUINO=10805 -DARDUINO_BOARD=PLATFORMIO_ESP12E -DFLASHMODE_DIO -DLWIP_OPEN_SRC -DNONOSDK22x_190703=1 -DTCP_MSSß=536 -DLWIP_FEATURES=1 -DLWIP_IPV6=0 -DVTABLES_IN_FLASH -I.platformio/packages/framework-arduinoespressif8266/cores/esp8266 -I.platformio/packages/framework-arduinoespressif8266/tools/sdk/include -I.platformio/packages/framework-arduinoespressif8266/tools/sdk/libc/xtensa-lx106-elf/include'
export FC_ERRORS="-kernel-warn-key annot-error=error"
frama-c ${FC_ERRORS} -fclang-cpp-extra-args="${FC_COMPILER}" -machdep x86_32 -wp -wp-rte src/main.cpp
```
in a Docker container varosi/frama-c-clang:21.1
I get a lot of errors such as:
```
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
In file included from /usr/local/share/frama-c/frama-clang/libc++/utility:28:
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:46: error: template argument for template type parameter must be a type
using conditional_t = typename conditional<B,T,F>::type;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:278:25: note: template parameter is declared here
template <bool, class T, class F> struct conditional;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:54: error: expected a qualified name after 'typename'
using conditional_t = typename conditional<B,T,F>::type;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:54: error: type-id cannot have a name
using conditional_t = typename conditional<B,T,F>::type;
----------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:33:23: error: unknown type name '_Bool'
template<class T> bool operator!=(const T& x, const T& y) { return !(x == y); }
^
/usr/local/share/frama-c/libc/stdbool.h:25:14: note: expanded from macro 'bool'
#define bool _Bool
----------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:68:40: error: expected a qualified name after 'typename'
const T&, T&&>::type
^
/usr/local/share/frama-c/frama-clang/libc++/utility:68:40: warning: variable templates are a C++14 extension
/usr/local/share/frama-c/frama-clang/libc++/utility:68:44: error: expected ';' at end of declaration
const T&, T&&>::type
^
;
/usr/local/share/frama-c/frama-clang/libc++/utility:69:20: error: unknown type name 'T'
move_if_noexcept(T& x) noexcept { return std::move<T&>(x); }
--------------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:110:16: error: template argument for template type parameter must be a type; did you forget 'typename'?
__and<
^
typename
/usr/local/share/frama-c/frama-clang/libc++/type_traits:274:25: note: template parameter is declared here
template <bool, class T=void> struct enable_if;
--------------------
```
What can be fixed here?Virgile PrevostoVirgile Prevosto