frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-10-13T09:04:40Zhttps://git.frama-c.com/pub/frama-c/-/issues/2550Frama-c crash with z.Overflow error2021-10-13T09:04:40ZKarine EMFrama-c crash with z.Overflow error<!--
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
No external headers required, just run: (the program is at the end of this report)
```
frama-c -eva da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c
```
<!--
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
<!--
Please explain here what is the expected behaviour.
-->
Not to crash. The code is passing compilation with gcc and clang with few warnings.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Frama-c crashed:
```
[kernel] Parsing da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c (with preprocessing)
[kernel] Current source was: da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c:4
The full backtrace is:
Raised by primitive operation at file "src/libraries/stdlib/integer.ml" (inlined), line 100, characters 13-21
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10006, characters 47-64
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9976, characters 13-36
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9697, characters 25-48
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9687, characters 9-1023
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9328, characters 10-294
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10326, characters 12-35
Called from file "list.ml", line 110, characters 12-15
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10330, characters 2-25
Called from file "src/kernel_internals/typing/frontc.ml", line 83, characters 14-36
Called from file "src/kernel_services/ast_queries/file.ml", line 602, characters 25-44
Called from file "src/kernel_services/ast_queries/file.ml", line 622, characters 14-38
Called from file "src/kernel_services/ast_queries/file.ml", line 685, characters 46-72
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_queries/file.ml", line 685, characters 17-89
Called from file "src/kernel_services/ast_queries/file.ml", line 1625, characters 24-60
Called from file "src/kernel_services/ast_queries/file.ml", line 1702, characters 4-27
Called from file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
Called from file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Z.Overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: Frama-C version is 21.0 (Scandium) and Frama-C version is 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
I reduced the program that crashed Frama-c into this: (via Creduce)
```
long a;
void b() {
switch (a)
case 0 ... 9999999999999999999:;
}
void main() {}
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2565Arch Linux package uninstallable due to dependency that no longer exists2021-10-06T07:53:07ZOlivier NicoleArch Linux package uninstallable due to dependency that no longer exists- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [ ] you insta...- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Arch Linux User Repository package
- Frama-C version: 21.1-1
- Plug-in used: N/A
- OS name: Arch Linux
- OS version: N/A
The Arch Linux User Repository package `frama-c` depends on gtksourceview2 which seems to no longer exist in the repositories, preventing the installation.
# Fix ideas
I'm not sure which would be simpler between upgrading to a newer version of gtksourceview or making that dependency available again.https://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/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/2570[frama-clang] Crash parsing compound literals2021-10-06T07:48:17ZEvgenii Kotelnikov[frama-clang] Crash parsing compound literals<!--
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
The following is a valid C++ code that initialises variables `i` and `j` using compound literals.
```cpp
typedef struct A_ { int a; } A;
struct B { int b; };
struct C { A aa; struct B bb; };
struct B i{0};
struct C j{{0}, i};
```
### Expected behaviour
`frama-c struct_fail.cpp` should parse the file.
### Actual behaviour
```
$ frama-c struct_fail.cpp
[kernel] Parsing struct_fail.cpp (external front-end)
Now output intermediate result
[fclang] struct_fail.cpp:6: Failure: Compound init on a scalar type
[kernel] Current source was: struct_fail.cpp:6
The full backtrace is:
Raised at Log.finally_raise in file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 546, characters 24-31
Called from Log.Register.fatal in file "src/kernel_services/plugin_entry_points/log.ml", line 1115, characters 17-55
Called from Log.logwithfinal.(fun) in file "src/kernel_services/plugin_entry_points/log.ml", line 539, characters 9-23
Re-raised at Log.logwithfinal.(fun) in file "src/kernel_services/plugin_entry_points/log.ml", line 542, characters 9-16
Called from Log.Register.fatal in file "src/kernel_services/plugin_entry_points/log.ml", line 1115, characters 4-125
Called from Convert.mk_compound_init.aux.aux_struct in file "convert.ml", line 558, characters 24-44
Called from Convert.mk_compound_init in file "convert.ml", line 563, characters 19-37
Called from Convert.convert_global in file "convert.ml", line 4028, characters 29-62
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Convert.convert_ast in file "convert.ml", line 4120, characters 12-76
Called from Frama_Clang_register.parse_cxx in file "frama_Clang_register.ml", line 175, characters 13-36
Called from File.parse_cabs in file "src/kernel_services/ast_queries/file.ml", line 621, characters 6-49
Called from File.to_cil_cabs in file "src/kernel_services/ast_queries/file.ml", line 630, characters 14-38
Called from File.files_to_cabs_cil.(fun) in file "src/kernel_services/ast_queries/file.ml", line 693, characters 46-72
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from File.files_to_cabs_cil in file "src/kernel_services/ast_queries/file.ml", line 693, characters 17-89
Called from File.prepare_from_c_files in file "src/kernel_services/ast_queries/file.ml", line 1784, characters 24-60
Called from File.init_from_cmdline in file "src/kernel_services/ast_queries/file.ml", line 1861, characters 4-27
Called from Ast.force_compute in file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
Called from Ast.compute in file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.1 (Vanadium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *23.1 (Vanadium)*
- Plug-in used: *frama-clang-0.0.11*
- OS name: *macOS*
- OS version: *Big Sur 11.5.2*Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2575[WP] Soundness issue when handling a pointer on a structure containing an array.2021-10-06T07:07:23ZAlexCid[WP] Soundness issue when handling a pointer on a structure containing an array.<!--
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
Save the following code into a file called "error.c":
```C
#include <__fc_builtin.h>
struct slice {
int len;
char *buf;
};
int main() {
char b[4] = {0};
struct slice s = {.len = Frama_C_int_interval(2, 100000), .buf=b};
struct slice *p = &s;
//@ assert \valid_read(p->buf + (0..(p->len-1)));
return (int)p->buf[p->len-1];
}
```
Then analyse this code using the WP plugin with the command
`frama-c error.c -eva -wp -wp-rte -wp-prover alt-ergo`
<!--
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
The assertion `//@ assert \valid_read(p->buf + (0..(p->len-1)));` does obviously not hold and should be rejected by WP.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
The manually added assertion, as well as the RTE assertion generated by wp-rte, are proved by alt-ergo. Using a different prover (z3, cvc4) yields the same result.
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: docker
- Frama-C version: 23.1
- Plug-in used: Eva, WP
- OS name: Ubuntu
- OS version: 20.04
### Additional information (optional)
Handling a pointer on a structure containing the array is required to trigger the bug - a simple structure containing the array won't trigger it.
This bug can also be triggered in a slightly more complex setting, where the array access is done in a second function and the `assert` clause is replaced by an equivalent `requires` clause in the preconditions of that second function.
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/125Shape of VC depends on selection of properties2021-09-21T13:53:03ZJens GerlachShape of VC depends on selection of propertiesID0002404:
**This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002404:
**This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002404 | Frama-C | Plug-in > wp | public | 2018-10-08 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP allows to select properties by using the option -wp-prop. I have noticed the following:
When selecting a property 'foo' by -wp-prop=foo, sometimes all VCs that belong to that property are verified.
However, when I wish to verify all properties, some VC's of the property 'foo' are not verified.
This might be caused by the fact that the the actual "shape" of a VC appears to depend on -wp-prop.
(I attach an example of the slight differences between a VC that belongs to a certain property "foo" depending on whether -wp-prop=foo is used or not.)
This of course defeats somehow the purpose of using -wp-prop and it would be a welcome feature
if the generation of a VC of a property 'foo' is not affected by "-wp-prop=foo".
### Additional Information :
Is this maybe a problem of Qed?
Also, if there are several ways to generate/simplify a VC, it would be nice if one chooses one that has a higher likelihood to be verified.
## Attachments
- [diff.txt](/uploads/14ff154d537bcec5e27f7f5946ba2bfd/diff.txt)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1145Develop strategies to efficiently run WP with different ATP and Coq2021-09-21T13:22:14ZJens GerlachDevelop strategies to efficiently run WP with different ATP and CoqID0001699:
**This issue was created automatically from Mantis Issue 1699. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001699:
**This issue was created automatically from Mantis Issue 1699. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001699 | Frama-C | Plug-in > wp | public | 2014-03-14 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This strategy should be controlled by a view options that also take into account how many processes are available.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/334poor errors message texts for Hoare memory model checks2021-09-21T13:21:18ZJochen Burghardtpoor errors message texts for Hoare memory model checksID0002311:
**This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002311:
**This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002311 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | sometimes |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-model Hoare memmodel_Hoare.c" on the attached program produces the output:
...
[rte] annotating function foo
memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:8:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:8:[wp] warning: No validity
memmodel_Hoare.c:4:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:3:[wp] warning: No validity
[wp] 4 goals scheduled
...
The name of the memory model is "Hoare" on the command line and in the WP manual (Sect.3.2, p.44), but it is called "Empty" in the error message output.
Moreover, the message "No validity" should be expanded to be more understandable. As an additional convenience, Frama-C could mention in each message the variable it refers to ("x" resp. "*x") in all cases in the example).
## Attachments
- [memmodel_Hoare.c](/uploads/913f6495cac3874938af5d592e39d609/memmodel_Hoare.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2554Error when using docker file with Singularity2021-09-03T20:05:38Zthuynt_57Error when using docker file with Singularity<!--
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]…
-->
I used **Singularity** to pull the image of frama-c from docker hub.
However, when I run `frama-c -help`, I got the following error.
Could you please help me check it?
I don't have any problem when I use docker desktop.
[Updated] The image I tried is the one with tag 22.0
> [kernel] Current source was: :0
> The full backtrace is:
> Raised at file "stdlib.ml", line 29, characters 17-33
> Called from file "findlib.ml", line 166, characters 10-151
> Called from file "src/kernel_services/plugin_entry_points/dynamic.ml", line 299, characters 2-45
> Called from file "src/kernel_services/plugin_entry_points/kernel.ml", line 848, characters 4-49
> Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 886, characters 2-22
> Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
>
> Unexpected error (Failure("Config file not found - neither /root/.opam/ocaml-base-compiler.4.08.1/lib/findlib.conf nor the directory /root/.opam/ocaml-base-compiler.4.08.1/lib/findlib.conf.d")).
> Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
> Your Frama-C version is 22.0 (Titanium).
> Note that a version and a backtrace alone often do not contain enough
> information to understand the bug. Guidelines for reporting bugs are at:
> https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugsAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2571struct fields not assignable if any are const2021-08-31T16:52:57ZAaron Carrollstruct fields not assignable if any are const### Steps to reproduce the issue
Consider the following C snippet:
```
struct A {
const int x;
int y;
};
static struct A a;
/*@
assigns a.y;
*/
void f(void)
{
a.y = 1;
}
```
produces:
```
$ frama-c test_global_assi...### Steps to reproduce the issue
Consider the following C snippet:
```
struct A {
const int x;
int y;
};
static struct A a;
/*@
assigns a.y;
*/
void f(void)
{
a.y = 1;
}
```
produces:
```
$ frama-c test_global_assign.c
[kernel] Parsing test_global_assign.c (with preprocessing)
[kernel:annot-error] test_global_assign.c:9: Warning:
not an assignable left value: a.y. Ignoring logic specification of function f
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "test_global_assign.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```
### Expected behavior
Frama-C should accept the snippet since the `y` field of `a` is mutable.
### Actual behaviour
Code is rejected for `a.y` being non-assignable lvalue. Frama-C seems to treat the entire struct `a` as const, even though only one field is declared const. Removing the `const` specifier from `x` causes Frama-C to accept the code.
### Contextual information
23.1 (Vanadium) via opam on macOS. Does not reproduce on Frama-C 22.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/907axiom "addr_le_def" given to Alt-Ergo considered too weak2021-08-05T14:15:00ZJochen Burghardtaxiom "addr_le_def" given to Alt-Ergo considered too weakID0002047:
**This issue was created automatically from Mantis Issue 2047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002047:
**This issue was created automatically from Mantis Issue 2047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002047 | Frama-Clang | Plug-in > wp | public | 2015-01-12 | 2015-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Jan2015-Neon-20140301+dev-STANC | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The loop invariant "xx5" of the attached program "fill1.c" can't be proven with Alt-Ergo. The goal reads fine, viz.:
goal fill_loop_inv_xx5_preserved:
forall a_3,a_2,a_1,a : addr.
(a_1 <> a_2) ->
addr_le(a_3, a_2) ->
(region(a.base) <= 0) ->
(region(a_3.base) <= 0) ->
addr_le(a_3, shift_sint16(a_2, 1))
However, the axiom "addr_le_def" appears to be too weak, it currently reads:
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
(addr_le(p, q) -> ((p).offset <= (q).offset))))
While the loop inveriant certainly should be provable, I don't see any way to prove a_3.base=a_2.base with the current version of the file.
Moreover, in order for axioms "addr_le_def" and "addr_le_def1" to be a definition of "addr_le(.,.)" in terms of "=" and "<=" etc., axiom "addr_le_def" should be changed to:
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)].
(addr_le(p, q) -> p.base = q.base and p.offset <= q.offset))
After that change, Alt-Ergo proves the goal without any problems. The attached file "fill_loop_inv_xx5_preserved_Alt-Ergo.mlw" contains the changed version in a comment at line 408.
If my argument is right, the whole axiomatization should be reviewed to remove similar flaws, which give Frama-C a rather poor performance on address arithmetic. (For that reason, I assigned a higher severity.)
### Additional Information :
Originally, I'd submitted this issue to the Alt-Ergo issue tracker, see https://github.com/OCamlPro/alt-ergo/issues/9. I'm indebted to Mohamed Iguernelala for hinting at the weak axiom "addr_le_def", where I had a blind spot.
## Attachments
- [fill1.c](/uploads/e5ff187165a5e10b7858e1f325eea68a/fill1.c)
- [fill_loop_inv_xx5_preserved_Alt-Ergo.mlw](/uploads/6292554fc2953d67792737e6dac31199/fill_loop_inv_xx5_preserved_Alt-Ergo.mlw)
- [fill.c](/uploads/c1dcc11d568e2e09d95aeabf0b9df093/fill.c)
- [fill4.c](/uploads/5ce99f117503a2df12c827af1b439520/fill4.c)
- [fill5.c](/uploads/ece00cbe919a18c0800d32b0adb27fb2/fill5.c)
- [fill4r.c](/uploads/81225ff5f9ecee0d89645919cbe59e44/fill4r.c)
- [find_arr.c](/uploads/fec90cf4fecefaee9a7cea344c14b693/find_arr.c)
- [find_ptr.c](/uploads/8430a7bbd76c8f263bd433d3cfd746d8/find_ptr.c)
- [find_ptr_foo_post_Alt-Ergo_modified.mlw](/uploads/d52e028cdf21562b07c9e340031cef8c/find_ptr_foo_post_Alt-Ergo_modified.mlw)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/513Make find(1) command POSIX-compliant2021-08-05T14:12:49Zmantis-gitlab-migrationMake find(1) command POSIX-compliantID0002222:
**This issue was created automatically from Mantis Issue 2222. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002222:
**This issue was created automatically from Mantis Issue 2222. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002222 | Frama-C | Plug-in > wp | public | 2016-04-09 | 2016-04-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mmcc | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | All | **OS** | OpenBSD | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
src/plugins/wp/share/Makefile uses the -delete option of find(1), which is a GNU extension. The same behavior can be achieved using the POSIX-specified -exec option. The attached patch changes this Makefile to use -exec, fixing 'make clean' on systems that don't use GNU find.
Thanks,
Mike
### Steps To Reproduce :
Run 'make clean' on a system that uses a non-GNU find(1) utility.
## Attachments
- [t.diff](/uploads/095f86b8d788cfe86e200c4ce7eec41b/t.diff)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2098suggest to provide FILE,LINE references for proof obligations in WP cmd-line ...2021-08-05T13:14:10ZJochen Burghardtsuggest to provide FILE,LINE references for proof obligations in WP cmd-line outputID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001011 | Frama-C | Plug-in > wp | public | 2011-11-04 | 2011-11-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the command-line (i.e. non-gui) version of WP gives internally-generated names of proof obligations, like e.g.
[wp] [Simplify] Goal store_axiom_pop_of_push_pre31_push_stack_s1 : Valid
[wp] [Simplify] Goal store_axiom_pop_of_push_pre26_pop_stack_s2 : Timeout
In order to support the user in improving his program to get it verified, it should be made clear where an unproven obligation originated from, by providing file name and line number. Although a lot of information can be found in the directory specified with "-wp-out", the FILE,LINE information cannot.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2568Known WP limitations on the reads clause2021-08-05T09:28:31ZAllan BlanchardKnown WP limitations on the reads clauseThis issue lists known WP issues with the reads clause. Related issues are closed (as duplicates) and listed here.
- [ ] Generate `reads` footprint
- pub/frama-c#1146
- pub/frama-c#410
- [ ] Better handle missing `reads`
- p...This issue lists known WP issues with the reads clause. Related issues are closed (as duplicates) and listed here.
- [ ] Generate `reads` footprint
- pub/frama-c#1146
- pub/frama-c#410
- [ ] Better handle missing `reads`
- pub/frama-c#2172Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/1912Post-state of statement spec2021-08-05T09:27:36Zmantis-gitlab-migrationPost-state of statement specID0000765:
**This issue was created automatically from Mantis Issue 765. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000765:
**This issue was created automatically from Mantis Issue 765. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000765 | Frama-C | Plug-in > wp | public | 2011-03-25 | 2013-03-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When there is a [goto] going out of a block, the post-condition should be check at the normal exit of the block (ie. the program point after the '}'). But there is a problem when the [goto] precisely jump to that point...
The CFG for WP should be able to find only the edge coming from the block exit !
### Additional Information :
$ frama-c -wp toto.c -wp-print
Goal store_f_default_for_stmt_2_stmt_post_1:
forall c:int.
is_in_format(sint32_format, c)
-> ( tag_Then:( (c <> 0) -> (let x= 1 in (x = 10)))
and tag_Else:( (c = 0) -> (let x= 10 in (x = 10))))
## Attachments
- [toto.c](/uploads/8feb2b09fab3964d8240b54efa9b2d18/toto.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/625validity of obligation from statement contract depends on whether the stateme...2021-08-05T09:27:25ZJochen Burghardtvalidity of obligation from statement contract depends on whether the statement is enclosed in block {}ID0002123:
**This issue was created automatically from Mantis Issue 2123. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002123:
**This issue was created automatically from Mantis Issue 2123. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002123 | Frama-C | Plug-in > wp | public | 2015-06-01 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 480.c" on the attached program produces one unproven Alt-Ergo obligation (see file "in_block_foo_stmt_post_Alt-Ergo.mlw").
If the block parentheses in line 16 and 23 are removed, the corresponding obligation (file "not_in_block_foo_stmt_post_Alt-Ergo.mlw") is proven.
The differences between both obligations files are:
772c772
< forall t_2,t_1 : (addr,int) farray.
---
> forall t_1 : (addr,int) farray.
780c780
< (1 = L_deref(t_2, a))
---
> (1 = L_deref(t_1, a))
So, enclosing the statement in a block apparently creates an unrelated memory state.
## Attachments
- [480.c](/uploads/55316dd19dad2a676e3bd65c099feb68/480.c)
- [in_block_foo_stmt_post_Alt-Ergo.mlw](/uploads/a9e4708fc1538ad58d7a2b081be33aa2/in_block_foo_stmt_post_Alt-Ergo.mlw)
- [not_in_block_foo_stmt_post_Alt-Ergo.mlw](/uploads/825bcad7efb1e4837cdba3c38b5efd31/not_in_block_foo_stmt_post_Alt-Ergo.mlw)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/337suggest to check (loop) assigns clauses by data flow analysis2021-08-05T09:22:29ZJochen Burghardtsuggest to check (loop) assigns clauses by data flow analysisID0002308:
**This issue was created automatically from Mantis Issue 2308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002308:
**This issue was created automatically from Mantis Issue 2308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002308 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | low | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | n/a | **OS** | n/a | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp ifft_assigns.c -wp-prop check -wp-prover cvc4" on the attached file proved \false in line 339, which was intentionally inserted as a consistency check at the file's end. The reason for the inconsistency turned out to be a missing variable in a loop assigns clause (commented out for demo purposes in line 237). The detailled argument doesn't matter here; nevertheless it is given in (*) below for convenience.
I guess it would be easy for Frama-C to perform some coarse data-flow analysis and issue a warning about "nu2" being modified in line 295, but missing in the "loop assigns" clauses for the loop in line 242-302. Such an analysis could ignore nontrivial aliases, dead code, and array subranges, thus making it straight-forward to implement.
The example shows the value of warnings that such an analysis is able to issue. Already in this tiny example, it is easy to lose overview (cf. the many experimental "asserts", most of which a probably unncessary, or even nonsensical), and any tool help that doesn't cost much additional computation time is appreciated.
As a further application, it could print suggestions for "assigns" clauses of loops and procedure contracts.
(*): In fact, property "a2" from line 214 implies "nu1!=65536", if the latter variable remained unchanged during the loop in line 242-302, then property "c2" in line 232 boild down to "nu1+l==nu", which is false after the loop since then the termination condition "nu<l" has to hold, and "nu1" is unsigned.
## Attachments
- [ifft_assigns.c](/uploads/c813b7d252cb81e38d9f4fe871139244/ifft_assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/410Logic with read clauses can have their values invalidated by writes to separa...2021-08-05T09:15:39Zmantis-gitlab-migrationLogic with read clauses can have their values invalidated by writes to separated memory locationsID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002244 | Frama-C | Plug-in > wp | public | 2016-08-08 | 2016-08-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
In some cases, axiomatic logic using reads clauses can be true for a certain memory location, and then become unknown once an unrelated memory location is assigned to. You can even prove the memory locations as separate, but it does not fix the issue.
### Additional Information :
This bug is present on both Frama-C versions Sodium and Aluminum.
### Steps To Reproduce :
== File bug.c:
/*@
axiomatic Axiomatic {
logic boolean property_of_buffer(char *buffer) reads *buffer;
}
*/
/*@
assigns *buffer;
ensures property_of_buffer(buffer);
*/
void foo(char *buffer);
/*@
requires property_of_buffer(buffer);
assigns *buffer;
ensures property_of_buffer(buffer);
*/
int bar(char *buffer);
char buf1[1];
char buf2[1];
void main() {
foo(buf1);
bar(buf1);
foo(buf2);
bar(buf1);
}
== Command to run:
frama-c -wp bug.c
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_main_call_bar_pre : Valid
[wp] [alt-ergo] Goal typed_main_call_bar_pre_2 : Unknown (562ms)
[wp] Proved goals: 1 / 2
Qed: 1
alt-ergo: 0 (unknown: 1)
== Expected behavior: For typed_main_call_bar_pre_2 to prove valid.
## Attachments
- [bug.c](/uploads/40ef28c81962575b7520fa0642241586/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1146Generate footprint from reads clauses of logic declarations2021-08-05T09:15:35ZJens GerlachGenerate footprint from reads clauses of logic declarationsID0001693:
**This issue was created automatically from Mantis Issue 1693. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001693:
**This issue was created automatically from Mantis Issue 1693. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001693 | Frama-C | Plug-in > wp | public | 2014-03-13 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | high | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It would be helpful if the reads clause of an axiomatic definition would be
used to generate additional hypothesis for coq proofs.Loïc CorrensonLoïc Correnson