frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-02-09T14:44:32Zhttps://git.frama-c.com/pub/frama-c/-/issues/2662Stack overflow during e-acsl translation of runtime error assertions on coreu...2024-02-09T14:44:32ZRaphaël MonatStack overflow during e-acsl translation of runtime error assertions on coreutils program<!--
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'm trying to leverage frama-c rte and e-acsl plugins to encode all runtime errors through assertions, following ["A Lesson on Runtime Assertion Checking with Frama-C"](https://julien-signoles.fr/publis/2013_rv.pdf). I might have gotten a bit ambitious and tried to launch it on some preprocessed coreutils file.
### Steps to reproduce the issue
Attached is [chcon_comb2.c](/uploads/da99c1b868a8909c7f16a5ee69de1119/chcon_comb2.c).
```
$ frama-c -rte chcon_comb2.c -machdep x86_64 -then -e-acsl -then-on e-ascl -print -ocode chcon_comb2_rte.c
[...]
Ignoring annotation.
[kernel] Current source was: chcon_comb2.c:48883
The full backtrace is:
Raised at Frama_c_kernel__Project.on in file "src/libraries/project/project.ml", line 365, characters 59-66
Called from E_ACSL__Main.generate_code.(fun) in file "src/plugins/e-acsl/src/main.ml", line 46, characters 7-1023
Called from Frama_c_kernel__State_builder.Hashtbl.memo in file "src/libraries/project/state_builder.ml", line 569, characters 17-22
Called from E_ACSL__Main.main in file "src/plugins/e-acsl/src/main.ml", line 162, characters 11-56
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_boot__Boot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel.aux in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 865, characters 30-76
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (Stack overflow).
```
### Expected behaviour
I was wondering if there was an easy fix in the source code to avoid this Stack overflow?
As a side note, the rte package seems to not support "Builtins for long double type". For now I just changed the types.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.0 (Cobalt)
- Plug-in used: RTE & E-ACSL
- OS name: Ubuntu
- OS version: 22.04.2Julien SignolesJulien Signoleshttps://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/982Wrong localisation of not yet supported constructs2023-10-09T13:44:38ZJulien SignolesWrong localisation of not yet supported constructsID0001692:
**This issue was created automatically from Mantis Issue 1692. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001692:
**This issue was created automatically from Mantis Issue 1692. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001692 | Frama-C | Plug-in > E-ACSL | public | 2014-03-13 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | AMD 64 | **OS** | Linux | **OS Version** | Ubuntu |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
===== t.c =====
int main(void) {
//@ assert 2 >> 2 == 0;
return 1;
}
===========
$ frama-c -e-acsl t.c
t.c:1:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
Ignoring annotation.
The warning should be located at line 2, not at line 1.
### Additional Information :
Reported by P.-L. Garoche on Frama-C discuss.https://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/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 Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/177Incorrect handling of \initialized when initialized struct is passed to a fun...2022-09-28T11:30:33ZKostyantyn VorobyovIncorrect handling of \initialized when initialized struct is passed to a function by valueID0002310:
**This issue was created automatically from Mantis Issue 2310. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002310:
**This issue was created automatically from Mantis Issue 2310. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002310 | Frama-C | Plug-in > E-ACSL | public | 2017-06-13 | 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 :
This test case is derived from Toyota ITC benchmarks (File uninit_var.c, test case 012). Consider the following code:
struct S1 {
int t;
};
int foo(struct S1 s) {
/*@assert \initialized(&s.t); */
if (s.t > 0) return 0;
return 1;
}
int main(int argc, const char **argv) {
struct S1 s;
s.t = 1;
foo(s);
return 0;
}
Field `t` of struct `S1` is initialized in `main` but when it is passed to `foo` (by value) it's a brand new block where field `t` is not marked as initialized. Consequently assertion in `foo` wrongly fails.
## Attachments
- [itc-uninit-var-12.c](/uploads/4d29c1dc6442465e49a331c23bdd24b3/itc-uninit-var-12.c)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2613Questions about other function2022-07-12T06:53:28ZJaeD-ShinQuestions about other functionI have a question.
Is there a function to save the output from the `e-acsl-gcc.sh` command as a log(or txt) file ?I have a question.
Is there a function to save the output from the `e-acsl-gcc.sh` command as a log(or txt) file ?Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2604e-acsl-gcc.sh segmentation fault2022-05-12T12:25:35ZJaeD-Shine-acsl-gcc.sh segmentation faultWhenever option --validate-format-strings of e-acsl-gcc.sh is set, E-ACSL detects format-string vulnerabilities in printf-like function. Below is an example which incorrectly tries to print a string through a %d format.
File printf.c
``...Whenever option --validate-format-strings of e-acsl-gcc.sh is set, E-ACSL detects format-string vulnerabilities in printf-like function. Below is an example which incorrectly tries to print a string through a %d format.
File printf.c
```
#include <stdio.h>
int main(void) {
printf ("is %d really an int?", "foo");
return 0;
}
```
```
jaeyoung@jaeyoung-VirtualBox:~/Downloads/frama$ e-acsl-gcc.sh -Oprintf -c --validate-format-strings print.c
+ /home/jaeyoung/.opam/default/bin/frama-c -remove-unused-specified-functions -variadic-no-translation -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib print.c -e-acsl -e-acsl-validate-format-strings -e-acsl-share=/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode a.out.frama.c
[kernel] Parsing print.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] /usr/include/x86_64-linux-gnu/bits/thread-shared-types.h:92: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -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 print.c -o printf
+ gcc -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_VALIDATE_FORMAT_STRINGS -std=c99 -m64 -g -O2 -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/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -o printf.e-acsl a.out.frama.c /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/jaeyoung/.opam/default/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm
jaeyoung@jaeyoung-VirtualBox:~/Downloads/frama$ ./printf.e-acsl
Segmentation fault (core dumped)
```
The error in the printf.c file cannot be detected because a 'segmentation fault' has occurred.
The result of running gdb of ./printf.e-acsl is as follows.
```
(gdb) run
Starting program: /home/jaeyoung/Downloads/frama/printf.e-acsl
Program received signal SIGSEGV, Segmentation fault.
0x000055555555c1fa in shadow_alloca (
ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>, size=size@entry=216)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
302 sec_shadow[j++] = size;
(gdb) bt
#0 0x000055555555c1fa in shadow_alloca (
ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>, size=size@entry=216)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
#1 0x000055555555e9bf in register_safe_locations (
thread_only=thread_only@entry=0)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c:720
#2 0x000055555555ea88 in do_eacsl_memory_init (argc_ref=<optimized out>,
argv_ref=<optimized out>, ptr_size=<optimized out>)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c:324
#3 0x000055555555ebd9 in __e_acsl_memory_init (argc_ref=<optimized out>,
argv_ref=<optimized out>, ptr_size=<optimized out>)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c:331
#4 0x0000555555557856 in main () at a.out.frama.c:243
```Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/1131E-ACSL reports use of invalid pointer while in fact the pointer is valid2022-05-02T09:10:40ZDavid MentréE-ACSL reports use of invalid pointer while in fact the pointer is validID0001478:
**This issue was created automatically from Mantis Issue 1478. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001478:
**This issue was created automatically from Mantis Issue 1478. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001478 | Frama-C | Plug-in > E-ACSL | public | 2013-09-04 | 2014-03-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130601 |
### Description :
On attached program, E-ACSL reports use of invalid pointer:
"""
Precondition failed at line 7 in function loop.
The failing predicate is:
\valid(global_i_ptr).
"""
But in fact the pointer is valid.
This is checked by reading and executing the program, but also statically with WP and Value analysis.
The attached program is compiled with following script, replacing $1 with q7_invalid_under_eacsl.c.
"""
PATH=/usr/local/stow/frama-c-Fluorine-20130601/bin:$PATH
export PATH
eacsl_path=`frama-c -print-share-path`/e-acsl
frama-c \
-cpp-command 'gcc -C -E -I/usr/local/stow/frama-c-Fluorine-20130601/share/frama-c/libc -I SSI'\
-e-acsl \
$1 \
-then-on e-acsl -print -ocode a-e-acsl.c \
&& \
gcc -I$eacsl_path $eacsl_path/memory_model/e_acsl_bittree.c $eacsl_path/memory_model/e_acsl_mmodel.c $eacsl_path/e_acsl.c a-e-acsl.c
"""
## Attachments
- [q7_invalid_under_eacsl.c](/uploads/fc3279cdc60e5191500031773634387f/q7_invalid_under_eacsl.c)https://git.frama-c.com/pub/frama-c/-/issues/180E-ACSL crash with RTE generated assertion with booleans2021-04-20T07:09:09Zmantis-gitlab-migrationE-ACSL crash with RTE generated assertion with booleansID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002412 | Frama-C | Plug-in > E-ACSL | public | 2018-12-03 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux x86_64 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
There might be a regression with the RTE or E-ACSL plugin with Argon.
/////////// boolean.c
#include <stdbool.h>
bool return_false(void)
{
return false;
}
int main(void)
{
return 0;
}
///////////////////////////
### Additional Information :
On Chlorine-20180502 (bfd93b819) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
### Steps To Reproduce :
On Argon 18.0 (2f7a0eee0) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Current source was: rte_boolean.c:10
The full backtrace is:
Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023
Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 18.0 (Argon).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [boolean.c](/uploads/1b34c066b4dc860013dcc10c38a49aad/boolean.c)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/974Command line arguments (argc/argv) are not marked as valid2021-02-22T14:02:26ZArvid JakobssonCommand line arguments (argc/argv) are not marked as validID0001831:
**This issue was created automatically from Mantis Issue 1831. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001831:
**This issue was created automatically from Mantis Issue 1831. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001831 | Frama-C | Plug-in > E-ACSL | public | 2014-07-11 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
See attached file for example. I have a fix coming for this.
## Attachments
- [bug-main-args.c](/uploads/60e1cc41c3422294c74dc182831652eb/bug-main-args.c)https://git.frama-c.com/pub/frama-c/-/issues/633Literal strings can be added multiple times in memory2021-02-22T14:01:51ZArvid JakobssonLiteral strings can be added multiple times in memoryID0001837:
**This issue was created automatically from Mantis Issue 1837. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001837:
**This issue was created automatically from Mantis Issue 1837. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001837 | Frama-C | Plug-in > E-ACSL | public | 2014-07-16 | 2015-06-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Consider the following example:
int i = 4;
while (i--) {
char *s = "toto";
/@ assert \valid(s) ; */
printf(s);
}
Each time the body of the while-loop is executed, the block corresponding to "toto" is added to the memory store, however this string has always the same address.
## Attachments
- [bug-1837-literal-strings.c](/uploads/4765106fd263bda0285e8ccba836efe9/bug-1837-literal-strings.c)https://git.frama-c.com/pub/frama-c/-/issues/632E-ACSL: executes "__store_block()" but never "__delete_block()"!2021-02-22T14:01:28Zmantis-gitlab-migrationE-ACSL: executes "__store_block()" but never "__delete_block()"!ID0001636:
**This issue was created automatically from Mantis Issue 1636. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001636:
**This issue was created automatically from Mantis Issue 1636. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001636 | Frama-C | Plug-in > E-ACSL | public | 2014-01-30 | 2015-06-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ThomasJ | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium |
### Description :
E-ACSL translation of a simple printf like:
printf("###");
results in the following code:
char *__e_acsl_literal_string;
__e_acsl_literal_string = "###";
__store_block((void *)__e_acsl_literal_string,sizeof("###"));
__full_init((void *)__e_acsl_literal_string);
__literal_string((void *)__e_acsl_literal_string);
printf(__e_acsl_literal_string);
The "__store_block()" function allocates memory, but there is no "__delete_block()" function in order to deallocate the memory!
Consider a periodic execution of printf()...
On my ARM processor with 1024KByte Flash and 160KByte RAM, this malloc without free will end up in the following error:
"assertion "new_leaf != NULL" failed: file "e-acsl/memory_model/e_acsl_bittree.c", line 256, function: __add_element"
malloc without free! :O
### Steps To Reproduce :
E-ACSL translation of:
int main(void)
{
int x = 0;
/*@ assert x == 0; */
while(1)
{
printf("###");
}
return 0;
}https://git.frama-c.com/pub/frama-c/-/issues/377Literal strings in global arrays with compound initializers are not correctly...2021-02-22T14:01:28ZArvid JakobssonLiteral strings in global arrays with compound initializers are not correctly initializedID0001817:
**This issue was created automatically from Mantis Issue 1817. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001817:
**This issue was created automatically from Mantis Issue 1817. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001817 | Frama-C | Plug-in > E-ACSL | public | 2014-06-25 | 2017-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | kvorobyov | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 14-Silicon |
### Description :
Frama-C GIT Commit: b71d80efb3808c286f1a2f17dbf54bc3909824d0
The generated function for initializing global variables "__e_acsl_memory_init" does not handle arrays containing literal strings with compound intializers.
Example:
char *A[2] = {"foo", "bar"};
int main(void) {
/*@ assert \valid(A[0]) ; */
/*@ assert \valid(A[1]) ; */
}
Generated __e_acsl_memory_init:
void __e_acsl_memory_init(void)
{
char *__e_acsl_literal_string;
__store_block((void *)(A),sizeof(char *[2]));
__e_acsl_literal_string = "bar";
__store_block((void *)__e_acsl_literal_string,sizeof("bar"));
__full_init((void *)__e_acsl_literal_string,sizeof("bar"));
__literal_string((void *)__e_acsl_literal_string);
A = (char *)__e_acsl_literal_string;
return;
}
The last assignment is incorrect.
## Attachments
- [usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i](/uploads/c0863a05b09fb4259e306909b32e8b9f/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i)https://git.frama-c.com/pub/frama-c/-/issues/253Cannot compile variable length arrays2021-02-22T14:01:19ZArvid JakobssonCannot compile variable length arraysID0001834:
**This issue was created automatically from Mantis Issue 1834. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001834:
**This issue was created automatically from Mantis Issue 1834. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001834 | Frama-C | Plug-in > E-ACSL | public | 2014-07-15 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
The resulting C-code from running Frama-C with E-ACSL on the following program (same as attached):
int main(int argc, char **argv) {
int len = 4;
int data[len];
return 0;
}
cannot be compiled, giving the following error:
bug-vla.c:(.text+0xa74): undefined reference to `alloca'
the code generated is:
[...]
void *alloca(unsigned long);
[...]
int len;
int *data;
unsigned long __lengthofdata;
len = 4;
{
/*sequence*/
__lengthofdata = (unsigned long)len;
data = (int *)alloca(sizeof(*data) * __lengthofdata);
}
[...]
This code does not compile with GCC and the flag -std=c99.
## Attachments
- [bug-vla.c](/uploads/1c4f45e3e9069be2db558c88138b286a/bug-vla.c)https://git.frama-c.com/pub/frama-c/-/issues/252E-ACSL: vla handling2021-02-22T14:01:19Zmantis-gitlab-migrationE-ACSL: vla handlingID0002381:
**This issue was created automatically from Mantis Issue 2381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002381:
**This issue was created automatically from Mantis Issue 2381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002381 | Frama-C | Plug-in > E-ACSL | public | 2018-07-01 | 2018-07-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The code:
<pre>
int main(void)
{
int size = 10;
int array[size];
return 0;
}
</pre>
<pre>
a.out.frama.c:141: undefined reference to `__fc_vla_alloc'
a.out.frama.c:143: undefined reference to `__fc_vla_free'
collect2: error: ld returned 1 exit status
e-acsl-gcc: fatal error: fail to compile/link instrumented code
</pre>https://git.frama-c.com/pub/frama-c/-/issues/973User defined function with specification memset conflicts with __e_acsl_memse...2021-02-22T13:52:54ZArvid JakobssonUser defined function with specification memset conflicts with __e_acsl_memset in e_acsl_mmodel.cID0001838:
**This issue was created automatically from Mantis Issue 1838. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001838:
**This issue was created automatically from Mantis Issue 1838. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001838 | Frama-C | Plug-in > E-ACSL | public | 2014-07-16 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | guillaume-petiot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | - |
### Description :
If the user defines a function "memset" with specifications, then the generated function will be called __e_acsl_memset. But there is already such a function in e_acsl_mmodel.c, so there is an error on linking. Example:
/*@ requires \valid(p) ; */
int memset(char *p) {
return 123;
}
int main() {
char *s = "toto";
memset(s);
return 0;
}
When compiling and linking:
/tmp/ccRT0UnW.o: In function `__e_acsl_memset':
scratch.gen.c:(.text+0x14): multiple definition of `__e_acsl_memset'
/tmp/cc8qdTOL.o:e_acsl_mmodel.c:(.text+0x2b): first defined here
collect2: error: ld returned 1 exit status
## Attachments
- [bug-memset.c](/uploads/2405fa7021b4b65de61fb584e072d2b6/bug-memset.c)https://git.frama-c.com/pub/frama-c/-/issues/977Dynamically allocated variables in body of while without break are not instru...2021-02-22T13:41:16ZArvid JakobssonDynamically allocated variables in body of while without break are not instrumentedID0001716:
**This issue was created automatically from Mantis Issue 1716. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001716:
**This issue was created automatically from Mantis Issue 1716. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001716 | Frama-C | Plug-in > E-ACSL | public | 2014-03-25 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The assertion on line 14 of the attached program fails even though p is a valid pointer at this point. However if the break on line 12 is uncommented, the assertion passes.
### Steps To Reproduce :
Frama-c run with the following parameters:
-machdep x86_64 -e-acsl bug-while-without-break.c -then-on e-acsl -print -ocode bug-while-without-break.gen.c
Compiled with the following flags:
export SHARE=`frama-c -print-share-path`
gcc -g -O0 -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o bug-while-without-break.c.out $SHARE/e-acsl/e_acsl.c $SHARE/e-acsl/memory_model/e_acsl_bittree.c $SHARE/e-acsl/memory_model/e_acsl_mmodel.c bug-while-without-break.gen.c -lgmp
## Attachments
- [bug-while-without-break.c](/uploads/23356798828425f202746243f69640df/bug-while-without-break.c)