frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-11-09T08:24:50Zhttps://git.frama-c.com/pub/frama-c/-/issues/2676E-ACSL : non-existent assigns clause in behavior2023-11-09T08:24:50ZYani ZIANIE-ACSL : non-existent assigns clause in behavior<!--
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.
-->
Run the following code with E-ACSL using ``e-acsl-gcc.sh -c -O assigns_test.out assigns_test.c``:
```C
/* assigns_test.c */
#include <limits.h>
int global_int;
/*@
requires INT_MIN < global_int < INT_MAX;
assigns global_int;
*/
int abs_global(){
if(global_int < 0) {return -global_int;}
return global_int;
}
int main(){
global_int = 0;
int local_int = abs_global();
return local_int;
}
```
### Expected behaviour
Instrumentation happens without warning.
### Actual behaviour
The following warning ``[e-acsl] assigns_test.c:9: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported.`` is reported, despite the function contract of ``abs_global`` not featuring any behavior.
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: at least from 26, still there in 28~beta
- Plug-in used: E-ACSL
- OS name: Ubuntu (via WSL)
- OS version: 22.04.2 LTS
FYI @nkosmatov
<!--
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.
-->Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/179Can't use e-acsl on a dynamic library containing all the instrumentations2023-03-22T03:49:51Zmantis-gitlab-migrationCan't use e-acsl on a dynamic library containing all the instrumentationsID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002422 | Frama-C | Plug-in > E-ACSL | public | 2019-01-22 | 2019-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.19 Ocaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 19-Potassium | **Fixed in Version** | - |
### Description :
Hi !
main.c contains the entry point : the main function and is not instrumented by frama-c
it calls instrumented func.c (e-acsl.func.c containing the __e_acsl_memory_init call) compiled as a dynamic library libe-acsl.func.so
then the e-acsl code segfault at
e_acsl_segment_tracking.h:815
### Additional Information :
Why the hell am I doing this ? :)
Contiki-NG is an IoT OS. It can be build as a firmware for several IoT devices, as a ELF for Linux x86/x86_64, and as a shared library loaded by the Java Cooja network simulator (with some JNI).
Before experimenting with dlopen in C and JNI in Java, which is going to fail because of the __executable_start symbol at ./share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h:47
(this will the subject of another future post)
I would like to be able, as a first step, to use a e-acsl instrumented dynamic library used by a non-instrumented program (containing main or not).
I am open to a solution that eventually needs some change inside the C E-ACSL code.
### Steps To Reproduce :
$ make
rm -vf *.*o ./loader ./main *e-acsl*
frama-c -main func -variadic-no-translation -machdep gcc_x86_64 -c11 -cpp-extra-args="-std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64" -no-frama-c-stdlib func.c -e-acsl-prepare -rte -warn-signed-overflow -warn-unsigned-overflow -warn-signed-downcast -warn-unsigned-downcast -rte-div -rte-float-to-int -rte-mem -rte-pointer-call -rte-shift -rte-no-trivial-annotations -then -e-acsl -e-acsl-full-mmodel -then-last -print -ocode e-acsl.func.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 func.c (with preprocessing)
[rte] annotating function __bswap_16
[rte] annotating function __bswap_32
[rte] annotating function __bswap_64
[rte] annotating function __uint16_identity
[rte] annotating function __uint32_identity
[rte] annotating function __uint64_identity
[rte] annotating function func
[e-acsl] beginning translation.
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap16, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap32, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap64, generating default assigns from the prototype
[kernel:annot:missing-spec] /usr/include/stdio.h:332: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
gcc -shared -fPIC -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_STACK_SIZE=32 -DE_ACSL_HEAP_SIZE=128 -std=c99 -m64 -O0 -g -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jean/local-frama-c/share/frama-c/e-acsl/ -o libe-acsl.func.so e-acsl.func.c /home/jean/local-frama-c/share/frama-c/e-acsl/e_acsl_rtl.c /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-dlmalloc.a /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-gmp.a -lm
gcc -o main main.c -L. -le-acsl.func
LD_LIBRARY_PATH=:./ ./main
Segmentation fault
make: *** [Makefile:11: e-acsl-main-shared] Error 139
## Attachments
- [e-acsl-is-fun.tar](/uploads/c1c5ac773627666455f1b0a93e66da53/e-acsl-is-fun.tar)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/182missing E-ACSL code, control flow graph, function pointer2021-03-30T13:47:26Zmantis-gitlab-migrationmissing E-ACSL code, control flow graph, function pointerID0002416:
**This issue was created automatically from Mantis Issue 2416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002416:
**This issue was created automatically from Mantis Issue 2416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002416 | Frama-C | Plug-in > E-ACSL | public | 2018-12-11 | 2018-12-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **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,
Is there a workaround for the function pointer limitation
//////////////// cfg.c
void func(void)
{
int i = 0 ;
int *ptr = &i;
/*@ assert \valid(ptr); */
*ptr = 0 ;
}
int main(int argc, char **argv)
{
void (*ptr_func)(void) = &func;
(*ptr_func)();
return 0;
}
////////////////
### Additional Information :
I would like to find a solution that do not involve :
- the use of EVA
OR
- modifying the code
### Steps To Reproduce :
$ frama-c -machdep gcc_x86_64 cfg.c -e-acsl -then-last -print -ocode cfg.e-acsl.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 cfg.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] cfg.c:12: Warning:
function pointers may introduce too limited instrumentation.
[e-acsl] translation done in project "e-acsl".
$ gcc -DE_ACSL_SEGMENT_MMODEL -Wno-attributes -I$(frama-c -print-share-path)/e-acsl/ -o cfg.e-acsl cfg.e-acsl.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
$ ./cfg.e-acsl
Assertion failed at line 5 in function func.
The failing predicate is:
\valid(ptr).
AbortedJulien SignolesJulien Signoleshttps://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 Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/266e-acsl-gcc failes on macOS2021-02-22T12:57:55ZJens Gerlache-acsl-gcc failes on macOSID0002369:
**This issue was created automatically from Mantis Issue 2369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002369:
**This issue was created automatically from Mantis Issue 2369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002369 | Frama-C | Plug-in > E-ACSL | public | 2018-02-23 | 2018-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to process the example 'true.i' from http://frama-c.com/eacsl.html
the `e-acsl-gcc.sh` script fails and reports
e-acsl-gcc: fatal error: unexpected output of system getopt
### Additional Information :
This problem does not occur on my Linux installation.Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/172Failure to detect overflows into an allocated area within a struct2021-02-22T13:35:04ZKostyantyn VorobyovFailure to detect overflows into an allocated area within a structID0002327:
**This issue was created automatically from Mantis Issue 2327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002327:
**This issue was created automatically from Mantis Issue 2327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002327 | Frama-C | Plug-in > E-ACSL | public | 2017-08-24 | 2019-01-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Presently E-ACSL treats structs as single units of program allocation issuing one call to `store_block` per struct. Such an approach fails to detect overflows within structs. Consider, for instance, the following program:
int main() {
struct node {
char buf1[8];
char buf2[8];
} n;
/*@assert manual_assertion: \valid(&n.buf1[12]); */
n.buf1[12] = '0';
return 0;
}
This program results in an overflow via assignment n.buf1[12] = '0'; that accesses buffer n.buf2 via n.buf1. However, since E-ACSL treats n as a single memory block the issue is not detected.Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/174Failure to record global variable with initialiser2022-09-28T12:12:55ZKostyantyn VorobyovFailure to record global variable with initialiserID0002194:
**This issue was created automatically from Mantis Issue 2194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002194:
**This issue was created automatically from Mantis Issue 2194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002194 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2019-01-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
/* The following example wrongly fails the assertion */
#include <inttypes.h>
char *B = "foo";
unsigned long ref() {
return (intptr_t)B;
}
int main(int argc, char **argv) {
char *ptr = (char*)ref();
//@ assert \valid_read(ptr);
return 0;
}
### Additional Information :
This seems to be the case where memory analysis incorrectly determines that global variable 'B' should not be modelled and therefore it is omitted from the instrumentation.Julien SignolesJulien Signoles