frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-07-24T10:25:01Zhttps://git.frama-c.com/pub/frama-c/-/issues/327Statement contracts and WP2023-07-24T10:25:01ZJens GerlachStatement contracts and WPID0002317:
**This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002317:
**This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002317 | Frama-C | Documentation > manuals | public | 2017-07-18 | 2017-07-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a follow-up on issue https://bts.frama-c.com/view.php?id=2300 which was rather briskly closed.
I can understand that the question on the semantics of statement contracts in WP is not discussed in the ACSL implementation manual. However, in my opinion, it should then be discussed in the WP manual.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1027Frama-C/WP does not warn about unsatisfied precondition2023-07-21T13:45:04ZJens GerlachFrama-C/WP does not warn about unsatisfied preconditionID0001678:
**This issue was created automatically from Mantis Issue 1678. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001678:
**This issue was created automatically from Mantis Issue 1678. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001678 | Frama-C | Plug-in > wp | public | 2014-03-07 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, OSX | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Here is the setup:
```c
/*@
requires 0 < a ;
assigns \nothing;
ensures 0 < \result < 10;
*/
int foo(int a);
/*@
assigns \nothing;
ensures 0 < \result < 30;
*/
int bar(int x)
{
int a = foo(1); // precondition satisfied
int b = foo(0); // precondition violated and recognized
int c = foo(x); // precondition not satisfied and not recognized
return a + b + c;
}
```
When I process this example with
frama-c-gui -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -no-unicode -wp-out ./out.wp
-wp-proof alt-ergo -wp-proof coq foo.c
then a green bullet appears next to the line
int c = foo(x); // precondition not satisfied and not recognized
However, it is unknown whether x satisfies the precondition "0 < x" of foo.
If, however, the lines are reverse like this
int c = foo(x);
int b = foo(0);
then both calls are correctly flagged as orange (yellow?)
### Additional Information :
The problem also appears in the release candidate for Neon.https://git.frama-c.com/pub/frama-c/-/issues/101-wp-out missing output for Why3 provers in Frama-C 20 beta2023-07-21T13:31:03ZJens Gerlach-wp-out missing output for Why3 provers in Frama-C 20 betaID0002485:
**This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002485:
**This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002485 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the attached programme is processed with
frama-c -wp -wp-rte -wp-prover native:alt-ergo -wp-out abs.wp abs.c
then the output directory 'abs.wp/typed' contains three files
abs_ensures_3_Alt-Ergo.mlw
abs_ensures_3_Alt-Ergo.out
abs_ensures_3.ergo
When using the command line
frama-c -wp -wp-rte -wp-prover alt-ergo -wp-out abs.wp abs.c
then the output directory 'abs.wp/typed' contains only the generated proof obligation
abs_ensures_3_Why3_Alt_Ergo_2_3_0.why
(similiarly when using another Why3 prover, such as cvc4)
Is there a way to output also the result for Why3 provers?
## Attachments
- [abs.c](/uploads/9fd4b3dcc0cf8490758da51b696be918/abs.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/70munmap() breaks WP analysis2023-07-21T13:28:43Zmantis-gitlab-migrationmunmap() breaks WP analysisID0002498:
**This issue was created automatically from Mantis Issue 2498. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002498:
**This issue was created automatically from Mantis Issue 2498. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002498 | Frama-C | Plug-in > wp | public | 2020-02-10 | 2020-02-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | adbq | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | Linux Debian | **OS Version** | Buster (10) |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using unmap() glib function, WP stops analysis with a fatal error "User Error: Invalid infinite range p_1+(0..)".
### Steps To Reproduce :
make frama-c, with appended code snippet.
## Attachments
- [Makefile](/uploads/b3d3d3c48e97cef222db70c65ef942aa/Makefile)
- [test4.c](/uploads/0aa351f38d2e0b1d6c56ae148a58164a/test4.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1147Generate proof obligation for drivers when driver instantiate a logic acsl de...2023-07-21T13:21:41ZJens GerlachGenerate proof obligation for drivers when driver instantiate a logic acsl declarationID0001694:
**This issue was created automatically from Mantis Issue 1694. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001694:
**This issue was created automatically from Mantis Issue 1694. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001694 | Frama-C | Plug-in > wp | public | 2014-03-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 would be helpful for proving (in coq) that a model of an ACSL logic function actually exists.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2632-wp-print for only failed goals2023-07-21T13:01:36ZDavid Cok-wp-print for only failed goalsI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/365Why3ide cannot be opened in this version2023-07-21T13:01:20ZPierre Yves PiriouWhy3ide cannot be opened in this versionID0002289:
**This issue was created automatically from Mantis Issue 2289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002289:
**This issue was created automatically from Mantis Issue 2289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002289 | Frama-C | Plug-in > wp | public | 2017-03-01 | 2017-03-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Pierre-Yves Piriou | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | linux 3.2.0-4-amd64 | **OS** | Debian | **OS Version** | 7.11 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I try to open the Why3 IDE from the GUI to edit a proof (right-click on Why3 column, then 'open why3ide'), the "running icon" is displayed but the IDE does not open.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2663Parse-print-reparse error with WP strategies2023-07-21T09:11:17ZNikolai KosmatovParse-print-reparse error with WP strategies## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 27.0dev (tested commit: 3396bd)
- Alt-Ergo 2.4.3
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, aft...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 27.0dev (tested commit: 3396bd)
- Alt-Ergo 2.4.3
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after parsing and printing the code, running frama-c again to parse the code produces an error (due to missing parentheses around a list of arguments (..)).
[strategy.c](/uploads/d089f42a7b3f32480a9d03227f201f0a/strategy.c)
Commands used:
`frama-c strategy.c -print -no-unicode -ocode pp_strategy.c`
`frama-c pp_strategy.c`Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/1278sliced program does not terminate (csmith)2023-07-12T07:55:12ZPascal Cuoqsliced program does not terminate (csmith)ID0000807:
**This issue was created automatically from Mantis Issue 807. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000807:
**This issue was created automatically from Mantis Issue 807. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000807 | Frama-C | Plug-in > slicing | public | 2011-04-28 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
same conditions as bug 806.
Compile the original with gcc -m32 -D__FRAMAC -I runtime show_each.c noterm.c (executable terminates) and the sliced program with gcc -m32 show_each.c noterm.s.c
## Attachments
- [noterm.c](/uploads/ab1ab0534ff4c95890d574157583e87b/noterm.c)https://git.frama-c.com/pub/frama-c/-/issues/1277typing rule of \old(tab) or tab[index] construct2023-06-26T07:11:16ZPatrick Baudintyping rule of \old(tab) or tab[index] constructID0000761:
**This issue was created automatically from Mantis Issue 761. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000761:
**This issue was created automatically from Mantis Issue 761. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000761 | Frama-C | Kernel > ACSL implementation | public | 2011-03-22 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
\old(t)[0] is interpreted as \old((int*)t)[0] when t is a C variable declared as follow:
int t[10];
That raises a problem when using such constructs combined with \let constructs.
It is mainly accepted that
\old(\let x = t ; x)
is equivalent to
\let x = \old(t) ; x
That propagation rule implies the type of t should be the same than the type of \old(t).
That isn't the case with the current ACSL implementation:
\old(\let x = t ; x) has type int[10] and
\let x = \old(t) ; x has type int*
The issue is more significant on theses expressions
\old(\let x = t ; x)[0] and
(\let x = \old(t) ; x)[0].
So, is the problem with a typing rule or with the propagation rule.https://git.frama-c.com/pub/frama-c/-/issues/2631Naming the anonymous behavior for -wp-bhv2023-06-21T08:58:19ZDavid CokNaming the anonymous behavior for -wp-bhvFeature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax tha...Feature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax that does not interfere with most shells. For example -wp-bhv ~Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2637libgnomecanvas disabled in brew2023-06-21T08:15:31ZLaura Titololibgnomecanvas disabled in brewTrying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/for...Trying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/formula/libgnomecanvas. https://gitlab.gnome.org/Archive/libgnomecanvas).https://git.frama-c.com/pub/frama-c/-/issues/2648Frama-c-gui does not install on macOS Ventura2023-06-21T08:02:03ZNikolaus HuberFrama-c-gui does not install on macOS VenturaI have tried installing Frama-C through opam on macOS Ventura (13.0.1) for a few days now. I have followed the official installation instructions including the installation of all required tools with brew and setting PKG_CONFIG_PATH. Aft...I have tried installing Frama-C through opam on macOS Ventura (13.0.1) for a few days now. I have followed the official installation instructions including the installation of all required tools with brew and setting PKG_CONFIG_PATH. After issuing `opam install frama-c` Frama-C gets installed, however, whatever I tried frama-c-gui is never available.
When I try
```
opam uninstall frama-c
opam install frama-c.25.0
```
everything works perfectly. I have tried it both on an Intel and an M2 MacBookPro. Does anyone have a similar problem?Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1266r12430, some assertions are localized at Cabs2cil_start:0 (csmith)2023-06-16T10:43:05ZPascal Cuoqr12430, some assertions are localized at Cabs2cil_start:0 (csmith)ID0000770:
**This issue was created automatically from Mantis Issue 770. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000770:
**This issue was created automatically from Mantis Issue 770. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000770 | Frama-C | Kernel | public | 2011-03-30 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
bin/toplevel.opt -val -slevel 70000 -unspecified-access dummy_loc.i
Result:
...
Cabs2cil_start:0:[kernel] warning: Unspecified sequence with side effect:
...
Cabs2cil_start:0:[kernel] warning: undefined multiple accesses in expression. assert \separated(l_934,& l_922);
...
The attached file is pre-processed but it was made from ordinary .c and .h files on a Linux system (computation server).
## Attachments
- [dummy_loc.i](/uploads/fdd12914c765bf9e2a12f0e7fd438798/dummy_loc.i)https://git.frama-c.com/pub/frama-c/-/issues/19suspicious Coq code for ACSL lemma in Frama-C 212023-06-05T07:47:25ZJens Gerlachsuspicious Coq code for ACSL lemma in Frama-C 21Thank 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 confirm (by adding a X...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 confirm (by adding a X in the [ ]):
- [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 [BTS](https://bts.frama-c.com);
- [x] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: opam
- Frama-C version: *21.0 (Scandium)*
- Plug-in used: *WP*
- OS name: *macOS*
- OS version: *10.15.5*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
The following ACSL lemma in file `a.c`
```
/*@
lemma C_Division_Two:
\forall integer a; 0 <= a ==> 0 <= a/2 <= a;
*/
```
is verified by Alt-Ergo when calling it with
```
frama-c-gui -wp -wp-prover alt-ergo -wp-prover native:coq a.c
```
However, in Frama-C 21, the **coq representation** of the lemma looks wrong to me since it reads
```
Goal
forall (i : Z),
((0 <= i)%Z) ->
(((((Cdiv i 2)) <= i)%Z) /\ (((-1) <= i)%Z)).
```
The `-1` does not seem to be right.
In `Frama-C 20`, on the other hand, the coq representation looks like this
```
Goal
forall (i : Z),
let x := ((Cdiv i 2))%Z in
((0 <= i)%Z) ->
(((x <= i)%Z) /\ ((0 <= x)%Z)).
```
Am I missing something here?https://git.frama-c.com/pub/frama-c/-/issues/13Compilation fails after E-ACSL plugin with -g option2023-06-05T07:47:25ZNikolai KosmatovCompilation fails after E-ACSL plugin with -g optionAs far as I know,
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- I installed Frama-C as prescribed in the [in...As far as I know,
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- I installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *E-ACSL*
- OS name: *Ubuntu*
- OS version: *19.10*
# Steps to reproduce the issue
Run with:
e-acsl-gcc.sh -omonitored_test.c -g -c test.c
See the attached file for a minimal example.
# Expected behaviour
The generation file is compiled and executed.
[test.c](/uploads/ff66f5d6118a8406a8cdab1d09686a5f/test.c)
# Actual behaviour
A compilation failure of the file generated file by the E-ACSL plugin.Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/12Frama-C/WP (21 Beta) does not recognise provers2023-06-05T07:47:25ZJens GerlachFrama-C/WP (21 Beta) does not recognise proversI have install Frama-C 21 (Beta) including `Why3 1.3.1`.
I also called `why3 config --detect` but when running WP on an example I receive the following messages
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function ...I have install Frama-C 21 (Beta) including `Why3 1.3.1`.
I also called `why3 config --detect` but when running WP on an example I receive the following messages
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] User Error: Prover 'cvc3' not found in why3.conf
[wp] User Error: Prover 'cvc4' not found in why3.conf
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
```
Attached is my `why3.conf` file
[why3.conf](/uploads/4027dedd8b95842f6e9e37b1a39e8184/why3.conf)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/46Question: Dump why3 file generated by frama-c2023-06-05T07:47:25ZLeo ViezensQuestion: Dump why3 file generated by frama-cHey, <br>
if I proove a file with the wp plugin, the C code gets transpiled into WhyML, is that right? <br>
If so, is it already possible, to dump the generated WhyML into a file? <br>
Thank you for your help.Hey, <br>
if I proove a file with the wp plugin, the C code gets transpiled into WhyML, is that right? <br>
If so, is it already possible, to dump the generated WhyML into a file? <br>
Thank you for your help.https://git.frama-c.com/pub/frama-c/-/issues/2660[Eva] The plugin doesn't terminate on this program2023-05-17T08:21:52ZCharles Babu M[Eva] The plugin doesn't terminate on this program### Steps to reproduce the issue
I ran ```dune exec -- frama-c loop_nla.c -eva```
```
/* Compute the floor of the square root, by Dijkstra */
extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int...### Steps to reproduce the issue
I ran ```dune exec -- frama-c loop_nla.c -eva```
```
/* Compute the floor of the square root, by Dijkstra */
extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
void reach_error() { __assert_fail("0", "dijkstra-u.c", 5, "reach_error"); }
extern unsigned int __VERIFIER_nondet_uint(void);
extern void abort(void);
void assume_abort_if_not(int cond) {
if(!(cond)) { abort();}
return;
}
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR:
{reach_error();}
}
return;
}
int counter = 0;
int main() {
unsigned int n, p, q, r, h;
n = __VERIFIER_nondet_uint();
assume_abort_if_not(n < 4294967295 / 4); // Avoid non-terminating loop
p = 0;
q = 1;
r = n;
h = 0;
while (counter++<1) {
if (!(q <= n))
break;
q = 4 * q;
}
//q == 4^n
while (counter++<1) {
__VERIFIER_assert(r < 2 * p + q);
__VERIFIER_assert(p*p + r*q - n*q == 0);
__VERIFIER_assert(h * h * h - 12 * h * n * q + 16 * n * p * q - h * q * q - 4 * p * q * q + 12 * h * q * r - 16 * p * q * r == 0);
__VERIFIER_assert(h * h * n - 4 * h * n * p + 4 * (n * n) * q - n * q * q - h * h * r + 4 * h * p * r - 8 * n * q * r + q * q * r + 4 * q * r * r == 0);
__VERIFIER_assert(h * h * p - 4 * h * n * q + 4 * n * p * q - p * q * q + 4 * h * q * r - 4 * p * q * r == 0);
__VERIFIER_assert(p * p - n * q + q * r == 0);
if (!(q != 1))
break;
q = q / 4;
h = p + q;
p = p / 2;
if (r >= h) {
p = p + q;
r = r - h;
}
}
__VERIFIER_assert(h*h*h - 12*h*n + 16*n*p + 12*h*r - 16*p*r - h - 4*p == 0);
__VERIFIER_assert(p*p - n + r == 0);
__VERIFIER_assert(h*h*p - 4*h*n + 4*n*p + 4*h*r - 4*p*r - p == 0);
return 0;
}
```
### Expected behaviour
It should terminate
### Actual behaviour
It does not terminate.
But if I change the ```assume_abort_if_not``` function by replacing the condition as below, it terminates
```
void assume_abort_if_not(int cond) {
if((cond)==0) { abort();}
return;
}
```
### Contextual information
- Frama-C installation mode: from source
- Frama-C version: 25.0~beta (Manganese)
- Plug-in used: EVA
- OS name: Ubuntu
- OS version: 20.04.6 LTSAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/1209Interpretation of @ assigns \result;2023-05-16T12:35:51Zmantis-gitlab-migrationInterpretation of @ assigns \result;ID0001448:
**This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001448:
**This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001448 | Frama-C | Plug-in > Eva | public | 2013-06-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Sorry for the title which is not very informative, but here is the problem :
in this example :
//@ assigns \result;
extern char * get_ptr (void);
int main (void) { char * p = get_ptr (); int x = p ? 0 : 1; return x; }
The value analysis tells me that the else branch is dead, so x is always 0.
If I change the assigns property into :
//@ assigns \result \from \nothing;
The problem disappears.