frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:00:23Zhttps://git.frama-c.com/pub/frama-c/-/issues/370problem with Qed's simplification power2021-02-22T13:00:23ZJochen Burghardtproblem with Qed's simplification powerID0002278:
**This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002278:
**This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002278 | Frama-C | Plug-in > wp | public | 2017-02-06 | 2017-02-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | Ubuntu 16.04.1 LTS | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-out wp-out shift.c" on the attached file and inspecting the file "wp-out/typed/foo_post_Alt-Ergo.mlw" shows that lemma "ShiftAssociative" is simplified to "true" (see line 360) by Qed. (The postcondition of foo doesn't matter here, except that it is intentionally unprovable in order to demonstrate the lemma's simplification.)
This situation doesn't change even when all options to disable Qed functionality (i.e. "-wp-no-bits -wp-no-clean -wp-no-core -wp-no-filter -wp-no-init-summarize-array -wp-no-let -wp-no-pruning -wp-no-simpl -wp-no-simplify-forall -wp-no-simplify-is-cint -wp-no-simplify-type") are given. (In contrast, in the somewhat related issue #1751, providing option "-wp-no-bits" is sufficient to circumvent the problem.)
While Qed's simplification capabilities are appreciated in general, the disappearance of the lemma can be a problem:
* In many Coq proofs related to C address computation, a similar lemma has to be stated and proven again and again. There seems to be no easy way to make Coq see what is considered trivial by Qed.
* Considering the discussion at https://github.com/OCamlPro/alt-ergo/issues/19, if I understood the Alt-Ergo people right, Alt-Ergo isn't complete on linear arithmetic with arrays (except for quantifier-free formulas). Therefore it sometimes needs trivial lemmas. In the particular example, to make Alt-Ergo prove the goal "reverse", a kind of associtivity property (axiom "arith") is needed that Qed would simplify also to "true", and even Alt-Ergo would.
Generally speaking, Qed should be (configurable such that it is) no stronger than any of the external provers, such as Coq and Alt-Ergo. This would enable the user to provide appropriate prover hints that are not simplified away by Qed. Maybe a command line option to completely switch off Qed is sufficient. As an alternative, a command-line switch could reduce the capabilities of Qed when applied to lemmas, assuming that the user is responsible to give them in an optimal form.
## Attachments
- [shift.c](/uploads/572d124b06bee30721a80150255027ac/shift.c)
- [foo_post_Alt-Ergo.mlw](/uploads/746bbaa9bc36a947691d7be190773542/foo_post_Alt-Ergo.mlw)Loïc CorrensonLoïc Corrensonhttps://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 Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/348preprocessor fail: unterminated comment2021-02-22T12:59:55Zmantis-gitlab-migrationpreprocessor fail: unterminated commentID0002307:
**This issue was created automatically from Mantis Issue 2307. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002307:
**This issue was created automatically from Mantis Issue 2307. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002307 | Frama-C | Kernel | public | 2017-05-30 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Gcc compiles this code, but frama-c throws preprocessor error.
$ gcc -w -c rte.c
$ echo $?
0
Code:
const char seq_show_option_value;
void *kmalloc_node_tmp;
__inline static void seq_show_option()
{
const char * name = 0;
int * m = 0;
/*@ behavior pre_seq_escape:
assigns *m \from *("= \t\n\\"+0), *(name+0), *m;
*/
&seq_show_option_value;
}
__inline static void mem_cgroup_update_page_stat()
{
__asm__ volatile (
".pushsection __bug_table\"a\"\n.popsection": : "i"("/lib/modules/4.8.12300.fc25.x86_64/build/include/linux/memcontrol.h"),
"i"(sizeof( int)))
/*@ assert \false; */ ;
}
void kmalloc_node()
{
kmalloc_node_tmp = kmalloc();
}
Error:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing rte.c (with preprocessing)
rte.c:17:7: error: unterminated comment
/*@ assert \false; */ ;
^
"rte.c":23:[kernel] user error: Can't preprocess annotation: Preprocessor call exited with an error
Some annotations will be kept as is
### Steps To Reproduce :
frama-c rte.c
## Attachments
- [rte.c](/uploads/d82c4d8c1dffa3fea82613e701df3ef0/rte.c)
- [test1.c](/uploads/49f6fc9782aa38e92aa358c523351fec/test1.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/298"pointer comparison" warning emitted for "p==NULL"2021-02-22T12:58:36ZJochen Burghardt"pointer comparison" warning emitted for "p==NULL"ID0002256:
**This issue was created automatically from Mantis Issue 2256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002256:
**This issue was created automatically from Mantis Issue 2256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002256 | Frama-C | Plug-in > Eva | public | 2016-11-11 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | - |
### Description :
Running "frama-c -val -val-warn-undefined-pointer-comparison=pointer ptrcmp3.c" on the attached file results in a warning:
ptrcmp3.c:10:[kernel] warning: pointer comparison. assert \pointer_comparable((void *)p, (void *)0);
The warning disappears if
1. the type of parameter "name" is changed from "char*" to "char" both in "foo" and in "main", or
2. the "assigns" clause for "foo" is deleted.
The warning seems strange by itself, as every pointer should be comparable to NULL. The changes that make the warning disappear (in particular 1.) support the hypothesis that this is a bug.
## Attachments
- [ptrcmp3.c](/uploads/3c9e9c4fc07c25680f1e5c42b0b24b71/ptrcmp3.c)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2560[Plug-in wp] 96-bits floats2021-10-06T07:52:08Zarun-babu[Plug-in wp] 96-bits floatsFeature request, as I get:
```
[kernel] Parsing file.c (with preprocessing)
[kernel] Plug-in wp aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in wp] 96-bits...Feature request, as I get:
```
[kernel] Parsing file.c (with preprocessing)
[kernel] Plug-in wp aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in wp] 96-bits floats'.
```
I am not sure what this means though!https://git.frama-c.com/pub/frama-c/-/issues/853placement new causes crash2021-02-22T13:13:28ZJochen Burghardtplacement new causes crashID0001960:
**This issue was created automatically from Mantis Issue 1960. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001960:
**This issue was created automatically from Mantis Issue 1960. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001960 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
124.cpp:5:[fclang] failure: Wrong number of arguments in function call (expected 2, got 0)
[kernel] Current source was: 124.cpp:5
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert.ml", line 601, characters 19-79
Called from file "src/frama-clang/convert.ml", line 875, characters 31-57
Called from file "src/frama-clang/convert.ml", line 1132, characters 20-53
Called from file "src/frama-clang/convert.ml", line 1275, characters 20-46
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1265, characters 17-40
Called from file "src/frama-clang/convert.ml", line 2151, characters 21-44
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
## Attachments
- [124.cpp](/uploads/71566326db9e49039b74bf124e12fee7/124.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/668path to non-existing directory given to framaCIRGen2021-02-22T13:26:29ZJochen Burghardtpath to non-existing directory given to framaCIRGenID0001954:
**This issue was created automatically from Mantis Issue 1954. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001954:
**This issue was created automatically from Mantis Issue 1954. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001954 | Frama-Clang | Plug-in > clang | public | 2014-11-06 | 2015-04-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe131.1 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When investigating issue #1953, in order to find out the appropriate command-line arguments for framaCIRGen, I called "frama-c -cxx-clang-command=echo 000.cpp" and got the output
-target i386-unknown-linux-gnu -I /usr/local/share/libc++ -I /usr/local/share/frama-c/libc -I /usr/local/share/frama-c --stop-annot-error 000a.cpp -o /tmp/clang_astb9af51ast
(before frama-c crashed due to lack of stdin input).
However, the first include path, "/usr/local/share/libc++", points to a non-existing directory. This need not be a problem, but it could be. In particular, some include files could be missing that are expected to reside in /usr/local/share/libc++.
### Additional Information :
No need to attach the trivial file 000.cpp here; any file will do.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2347Parse error when using a wide string literal to initialize uint16 array2021-02-22T13:56:58Zmantis-gitlab-migrationParse error when using a wide string literal to initialize uint16 arrayID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000593 | Frama-C | Kernel | public | 2010-09-30 | 2010-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Maria | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm trying to analyze Brew with Frama-C. OS - windows XP.
I've created simple Brew project(see attach), preprocessed it with Visual Studio and after it try to analyze with Frama-C:
C:\Frama-C\bin>frama-c.exe "\Program Files\BREW 3.1.5\sdk\examples\helloworld"\*.i
Also, I've tried to add files to project, using user interface, but nothing happened.
## Attachments
- [helloworld.zip](/uploads/e1faf5861730eaa7d75da589b90c18c6/helloworld.zip)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1034option -nostdinc does not seem to work2021-02-22T14:02:33ZJens Gerlachoption -nostdinc does not seem to workID0001786:
**This issue was created automatically from Mantis Issue 1786. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001786:
**This issue was created automatically from Mantis Issue 1786. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001786 | Frama-Clang | Kernel | public | 2014-05-26 | 2014-05-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When calling the following sample code (nostdinc.cpp)
#include "limits.h"
int foo(int a)
{
if (a >= INT_MAX/2)
return INT_MAX;
else
return a;
}
with
frama-c-gui -cpp-command 'gcc -C -E -nostdinc -I/usr/local/share/frama-c/libc' -cxx-clang-command="framaCIRGen" -cxx-stdinc -cxx-demangling-full -wp -wp-rte -wp-proof alt-ergo nostdin.cpp
refers to std header such as
In file included from nostdin.cpp:2:
In file included from /usr/include/clang/3.3/include/limits.h:38:
In file included from /usr/include/limits.h:25:
In file included from /usr/include/features.h:398:
/usr/include/x86_64-linux-gnu/gnu/stubs.h:7:11: fatal error: 'gnu/stubs-32.h' file not found
# include <gnu/stubs-32.h>
^Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/296Option "-lib-entry" results misses possible values of function pointers2021-02-22T12:58:33ZJochen BurghardtOption "-lib-entry" results misses possible values of function pointersID0002254:
**This issue was created automatically from Mantis Issue 2254. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002254:
**This issue was created automatically from Mantis Issue 2254. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002254 | Frama-C | Plug-in > Eva | public | 2016-11-07 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
(I posed this question also on frama-c-discuss on 3 Nov 2016, 16:20, and received a reply from David Mentré on 5 Nov 2016, 15:52. The advice to use an invariant and increase the slevel originates from Julien Signoles.)
Running "frama-c -val -main foo -lib-entry -slevel 10 fctptr.c" on the attached program results in an output of:
a ∈ [--..--]
fct ∈ {0}
While option "-lib-entry" behaves on the int variable "a" as described in the value analysis manual (sect.5.2.3, p.58), it seems to have no effect on the function pointer variable "fct". Moreover, the latter is analyzed to contain a null pointer, while it actually never does, due to its initialization at the declaration. Instead, since "fct" is declared "static", I'd expect the analysis to report:
a ∈ [--..--]
fct ∈ {{ &f1, &f2 }}
When "-lib-entry" is omitted, Frama-C's analysis coincides with mine:
a ∈ {1}
fct ∈ {{ &f1 }}
Both with and without option "-lib-entry", Frama-C's results don't change when the invariant is removed. To sum up, it seems that the use of option "-lib-entry" inhibits information from call analysis, but also from explicit invariants.
## Attachments
- [fctptr.c](/uploads/35907f38d48ab7e62a81d969080d542a/fctptr.c)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/843"operator==" not recognized as predicate name2021-02-22T14:02:14ZJochen Burghardt"operator==" not recognized as predicate nameID0001949:
**This issue was created automatically from Mantis Issue 1949. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001949:
**This issue was created automatically from Mantis Issue 1949. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001949 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
115.cpp:4:16: expecting an identifier after 'predicate'
Now output intermediate result
It should be easy to accept "operator==" also as an ACSL predicate name, similar as in C++ code.
## Attachments
- [115.cpp](/uploads/3af4fa9c279e598a1fa8f5271ba24e16/115.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2646OPAM installation on macOS fails2023-05-16T06:53:50ZvarosiOPAM installation on macOS fails<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
To install correctly using OPAM on macOS Ventura 13.2 on x64 following - https://frama-c.com/html/get-frama-c.html
### Actual behaviour
After running **opam install frama-c**, I got:
```
> <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
> -> removed conf-gtk2.1
> -> installed conf-gtk2.1
> -> retrieved frama-c.21.1 (cached)
> [ERROR] The compilation of frama-c.21.1 failed at "make -j11".
>
> #=== ERROR while compiling frama-c.21.1 =======================================#
> # context 2.1.4 | macos/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org#0c15cf29
> # path ~/.opam/default/.opam-switch/build/frama-c.21.1
> # command ~/.opam/opam-init/hooks/sandbox.sh build make -j11
> # exit-code 2
> # env-file ~/.opam/log/frama-c-37505-febf41.env
> # output-file ~/.opam/log/frama-c-37505-febf41.out
> ### output ###
> # [...]
> # Ocamlc src/plugins/qed/hcons.cmo
> # Ocamlc src/plugins/qed/listmap.cmo
> # Ocamlc src/plugins/qed/listset.cmo
> # Ocamlc src/plugins/qed/intmap.cmo
> # Ocamlc src/plugins/qed/intset.cmo
> # File "src/plugins/markdown-report/sarif.ml", line 31, characters 17-30:
> # Error: Unbound type constructor Yojson.Safe.t
> # make: *** [src/plugins/markdown-report/sarif.cmo] Error 2
> # make: *** Waiting for unfinished jobs....
> # Ocamlc src/plugins/qed/idxmap.cmo
> # AR src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
> # RANLIB src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: not installed previously
- OS name: macOS
- OS version: Ventura 13.2 on x64Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/576No syntax to apply lambda expressions2021-02-22T13:06:12ZDavid CokNo syntax to apply lambda expressionsID0002196:
**This issue was created automatically from Mantis Issue 2196. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002196:
**This issue was created automatically from Mantis Issue 2196. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002196 | Frama-C | Kernel > ACSL implementation | public | 2015-12-05 | 2015-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL 1.9 allows writing lambda expressions. They can be used in extended quantifiers. But there is no syntax to use them anywhere else, such as to apply a lambda expression to a sequence of arguments.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/864non-predicate on right-hand size of "|" causes segmentation fault2021-03-29T16:34:53ZJochen Burghardtnon-predicate on right-hand size of "|" causes segmentation faultID0001991:
**This issue was created automatically from Mantis Issue 1991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001991:
**This issue was created automatically from Mantis Issue 1991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001991 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Same for "&".
In contrast, "i | (i==i)" is accepted, which might not be ok either, since "i" is not a predicate, and "i | ..." isn't either.
## Attachments
- [155.cpp](/uploads/97f44d774ea3375ac8795a16896f3136/155.cpp)
- [155a.cpp](/uploads/6028e94aafd01c070d1470bd32b6a00c/155a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/36non-compilable slice produced by frama-c2023-06-05T07:47:25ZIvan Postolskinon-compilable slice produced by frama-cHello, I've testing some unstructured programs to study how frama-c slicing plugin works, and I've found that the following code snippet produces a wrong (non-compilable) slice.
Program:
```C
#include <stdio.h> /* printf, scanf, ...Hello, I've testing some unstructured programs to study how frama-c slicing plugin works, and I've found that the following code snippet produces a wrong (non-compilable) slice.
Program:
```C
#include <stdio.h> /* printf, scanf, NULL */
#include <stdlib.h>
int main(int argc, char **argv) {
int x = 1;
int i = 0;
for (; i < x; i = i + 2){
switch (i){
case 6:
L:
x++;
}
}
if (x + 1 == i) {goto L;};
return x;
}
```
Frama-c Command:
`frama-c code.c -then -eva -then -slice-return main -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode slice.c`
Output slice:
```C
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int x = 1;
int i = 0;
while (i < x) {
L: case 6: x ++;
i += 2;
}
if (x + 1 == i) goto L;
return x;
}
```
I would love to understand what went wrong in the slicing analysis, and if you got any references to the algorithm/technique in which the slicer plugin is based upon also would be highly appreciated.Patrick BaudinPatrick Baudinhttps://git.frama-c.com/pub/frama-c/-/issues/2323no multiple assert-clauses accepted in /*@...*/-style comment2021-02-22T13:56:31ZJochen Burghardtno multiple assert-clauses accepted in /*@...*/-style commentID0000601:
**This issue was created automatically from Mantis Issue 601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000601:
**This issue was created automatically from Mantis Issue 601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000601 | Frama-C | Kernel > ACSL implementation | public | 2010-10-12 | 2010-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
See attached program: when #define multipleAsserts is in force, the kernel complains about line 11-12, containing two assert-clauses in a single /*@...*/ comment.
I'm not sure this contradicts some ASCL-syntax definition.
However, it appears strange to me, since multiple requires, ensures, and loop invariant are admitted (although they could be joined into a single one by &&, as for assert, too).
## Attachments
- [ftest.c](/uploads/92ec6efb44e5b83b7f0d4baf1022eecc/ftest.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/66more precise error message for missing closing } of axiomatic block2021-02-22T13:35:01ZJens Gerlachmore precise error message for missing closing } of axiomatic blockID0002504:
**This issue was created automatically from Mantis Issue 2504. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002504:
**This issue was created automatically from Mantis Issue 2504. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002504 | Frama-C | Kernel | public | 2020-03-26 | 2020-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached example lacks the closing '}' of the axiomatic block.
Frama-C's error message says
[kernel:annot-error] ax.c:5: Warning: unexpected token ''
In a more complex setting I have spent some time to figure out what is wrong in line 5 (where 'bar' is defined).
A more precise error message that explicitly mentions the axiomatic block would be helpful.
## Attachments
- [ax.c](/uploads/143e163e821c428dbfad9ab2b22f974b/ax.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/249Model Variables in Frama C2021-02-22T13:33:10Zmantis-gitlab-migrationModel Variables in Frama CID0002397:
**This issue was created automatically from Mantis Issue 2397. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002397:
**This issue was created automatically from Mantis Issue 2397. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002397 | Frama-C | Kernel > ACSL implementation | public | 2018-08-27 | 2018-08-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The model variables in FramaC are giving errors whenever I tried to use them in specification
e.g the following code in ACSL manual complaints at line 3 (unexpected token 'forbidden'):
/* public interface */
//@ model set<integer> forbidden = \empty;
/*@ assigns forbidden;
ensures ! ( \result \in \old(forbidden)) &&
\result \in forbidden && \subset(\old(forbidden),forbidden);
*/
int gen();
p.s: please share if any further examples of model variables available in FramaC?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/588mixed virtual/nonvirtual base class causes error2021-02-22T13:39:25ZJochen Burghardtmixed virtual/nonvirtual base class causes errorID0002077:
**This issue was created automatically from Mantis Issue 2077. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002077:
**This issue was created automatically from Mantis Issue 2077. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002077 | Frama-Clang | Plug-in > clang | public | 2015-02-09 | 2015-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 462.cpp (external front-end)
Now output intermediate result
462.cpp:5:[kernel] failure: Cannot resolve variable __frama_c_arg_0
[kernel] user error: stopping on file "462.cpp" that has errors.
If "virtual" is deleted in line 4, the error disappears; similarly if "virtual" is inserted in line 3.
Since in Stroustrup's book no mixed virtual/nonvirtual base class is discussed, the example in file "462.cpp" may not be of any relevance. However, the clang++ compiler accepts that file without any problems.
## Attachments
- [462.cpp](/uploads/6c5857ed398e1a937d5fade5314a5a1e/462.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/183missing E-ACSL code when ignoring asm annotation2021-03-30T13:44:49Zmantis-gitlab-migrationmissing E-ACSL code when ignoring asm annotationID0002413:
**This issue was created automatically from Mantis Issue 2413. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002413:
**This issue was created automatically from Mantis Issue 2413. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002413 | Frama-C | Plug-in > E-ACSL | public | 2018-12-05 | 2018-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.18 OCaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
//////////////// asm.c
void func()
{
int i = 0;
int *ptr=&i;
/*@ assert \valid(ptr); */
*ptr = 0;
}
int main(int argc, char **argv)
{
func();
__asm__ ("");
return 0;
}
////////////////
### Additional Information :
When one comments the __asm__ line and compare the generated code, it seems that the list of missing functions are :
__e_acsl_memory_clean
__e_acsl_store_block
__e_acsl_delete_block
__e_acsl_initialize
__e_acsl_full_init
The problem is similar on Chlorine and Argon.
i and ptr could also be global static variables, it doesn't change anything
### Steps To Reproduce :
$ frama-c -machdep gcc_x86_64 asm.c -e-acsl -then-last -print -ocode eacsl_asm.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing asm.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] asm.c:11: Warning:
E-ACSL construct `asm' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
$ gcc -DE_ACSL_SEGMENT_MMODEL -Wno-attributes -I$(frama-c -print-share-path)/e-acsl/ -o asm eacsl_asm.c $(frama-c -print-share-path)/e-acsl/e_acsl_rtl.c $(frama-c -print-share-path)/../../lib/libeacsl-dlmalloc.a $(frama-c -print-share-path)/../../lib/libeacsl-gmp.a -lm
$ ./asm
Assertion failed at line 5 in function func.
The failing predicate is:
\valid(ptr).
Aborted
## Attachments
- [asm.c](/uploads/82f7e07cbdb3e0f4c91f1bc55aa7f411/asm.c)Julien SignolesJulien Signoles