Frama Clang issueshttps://git.frama-c.com/pub/frama-clang/-/issues2023-08-30T23:52:11Zhttps://git.frama-c.com/pub/frama-clang/-/issues/7Build instructions on ubuntu need updating2023-08-30T23:52:11ZchristinaburgeBuild instructions on ubuntu need updating
I am building this to use with Frama-C 27 (which I think should be ok per a recent commit, even though the instructions are not updated).
I have that built (by getting the source code and running make), but I can't seem to build Frama ...
I am building this to use with Frama-C 27 (which I think should be ok per a recent commit, even though the instructions are not updated).
I have that built (by getting the source code and running make), but I can't seem to build Frama Clang.
I've tried running autoconf and automake, but I get:
> /usr/bin/m4:configure.ac:33: cannot open `/home/chrbur02/.opam/default/share/frama-c/share/configure.ac': No such file or directory
configure.ac:45: error: m4_defn: undefined macro: _AC_LANG
./lib/autoconf/lang.m4:108: AC_LANG_POP is expanded from...
./lib/autoconf/c.m4:701: AC_PROG_CXX is expanded from...
configure.ac:45: the top level
autom4te: error: /usr/bin/m4 failed with exit status: 1
automake: error: autoconf failed with exit status: 1
What am I doing wrong?https://git.frama-c.com/pub/frama-clang/-/issues/6instructions for building frama-clang on MacOs are incomplete2023-04-01T03:25:03ZDavid Cokinstructions for building frama-clang on MacOs are incompleteThe instructions say to run ./configure
but there is no such file, just a configure.ac
However autoconf looks for such a file in the opam-installed instance of frama-c, which it does not find
And autoconf ./configure.ac is not successful...The instructions say to run ./configure
but there is no such file, just a configure.ac
However autoconf looks for such a file in the opam-installed instance of frama-c, which it does not find
And autoconf ./configure.ac is not successful either.
Perhaps a clone of the frama-c source tree is needed as well? and a setting of some FRAMA_C environment variables?https://git.frama-c.com/pub/frama-clang/-/issues/5Dependencies for building frame-clang on Ubuntu are incomplete or wrong2022-08-24T09:58:23ZDavid CokDependencies for building frame-clang on Ubuntu are incomplete or wrong
On Ubuntu, either 18.04 or 20.04
the description of dependencies for building frame-clang is incomplete.
With llvm@14 installed (with brew)
and frama-c 24 installed (with opam)
frame-clang fails to build or run (variously compile fail...
On Ubuntu, either 18.04 or 20.04
the description of dependencies for building frame-clang is incomplete.
With llvm@14 installed (with brew)
and frama-c 24 installed (with opam)
frame-clang fails to build or run (variously compile failures, link failures and failure to find .so at runtime)
unless also gcc/g++ -12 is installed (gcc-11 and gcc-10 at least both fail).
Even so, there are warnings during the build of frama-clang.
Also, I suspect that frame-clang is not buildable with earlier versions of llvm, but I did not exhaustively search for an appropriate version of gcc.
Note that https://frama-c.com/fc-plugins/frama-clang.html does say that frama-clang 0.0.12 depends on Frama-c 24 (correctly), but claims any clang above 10 is OK. I don't think that is correct, but if it is, each clang version should state which g++ version is required.
But the frame-clang manual linked on that page (https://frama-c.com/download/frama-clang-manual.pdf) points to frame-clang version 0.0.10 and Frama-C 22.https://git.frama-c.com/pub/frama-clang/-/issues/3Incorrect representation of std::true_type::value after C++-C translation2022-03-18T09:05:57ZT-GruberIncorrect 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
```
...
...### 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-gnuhttps://git.frama-c.com/pub/frama-clang/-/issues/1Parsing a file with including some bits of the STL2021-10-20T06:02:24ZAndre MaronezeParsing a file with including some bits of the STLThe following file does not parse when running `frama-c testing.cpp`, with Frama-Clang 0.0.11 installed, with a Frama-C 23.1+dev, OCaml 4.13, in Ubuntu 20.04:
```c++
#include<bits/stdc++.h>
using namespace std;
int main(){
cout<<"Hello...The following file does not parse when running `frama-c testing.cpp`, with Frama-Clang 0.0.11 installed, with a Frama-C 23.1+dev, OCaml 4.13, in Ubuntu 20.04:
```c++
#include<bits/stdc++.h>
using namespace std;
int main(){
cout<<"Hello World"<<endl;
return 0;
}
```
It results in:
```
[kernel] Parsing testing.cpp (external front-end)
In file included from /home/harshit/Desktop/testing.cpp:1:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/stdc++.h:35:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/cctype:41:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/c++config.h:524:
/usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/os_defines.h:44:5: error: function-like macro '__GLIBC_PREREQ' is not defined
#if __GLIBC_PREREQ(2,15) && defined(_GNU_SOURCE)
^
In file included from /home/harshit/Desktop/testing.cpp:1:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/stdc++.h:41:
/usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/cmath:45:15: fatal error: 'math.h' file not found
#include_next <math.h>
^~~~~~~~
code generation aborted due to compilation errors
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "testing.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
Is there a way to parse it? Does it require some specific command-line option?
(*issue migrated from a comment in the old, now archived, Frama-Clang Github repository: https://github.com/Frama-C/Frama-C-snapshot/issues/45*)