frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T14:01:18Zhttps://git.frama-c.com/pub/frama-c/-/issues/241Newer releases of FramaC produce apparent WP plug-in bug2021-02-22T14:01:18Zmantis-gitlab-migrationNewer releases of FramaC produce apparent WP plug-in bugID0002403:
**This issue was created automatically from Mantis Issue 2403. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002403:
**This issue was created automatically from Mantis Issue 2403. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002403 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2018-10-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached code base is a small example in which a reactive program interacts with peripherals via memory mapped I/O through a constant address. While earlier releases of framaC (Phosphorous) was able to generate full and faithful altergo for our proofs, the new version produces syntactically malformed altergo for the following boolean logic function defined in our example's ACSL:
mac.h line 35:
logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_\
packet.object_low == 0x0A) && (mac->mac_packet.payload_length == 0x00));
Whereas such boolean logic functions were correctly axiomatized in the older (Phosphorous) release, the current version is axiomatizing such a function as :
function L_isAMessage
() :
bool =
andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))
note that the argument to the logic function is absent, and the fields of hte mac_t referenced in the logic function are rendered as "#{w_i}", about which altergo then complains. These malformed altergo expressions seem to have been generated by the pretty printer's find_var function.
### Steps To Reproduce :
tar -xvf framaBug.tar.gz
make wp
## Attachments
- [framaBug.tar.gz](/uploads/54add4d4c38c4a03cb21e9dd404eef64/framaBug.tar.gz)
- [frmaBug.tar.gz](/uploads/fccae63bbfa3517b0d9bc45326a5f0e6/frmaBug.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/225Some issues related to Frama-C 18.0 (beta) "Argon"2021-02-22T13:33:32ZJens GerlachSome issues related to Frama-C 18.0 (beta) "Argon"ID0002408:
**This issue was created automatically from Mantis Issue 2408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002408:
**This issue was created automatically from Mantis Issue 2408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002408 | Frama-C | Plug-in > wp | public | 2018-11-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **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 18-Argon |
### Description :
This entry serves to link my GitHub issues on Argon (beta) to the BTS. The issues are
https://github.com/Frama-C/Frama-C-snapshot/issues/12
https://github.com/Frama-C/Frama-C-snapshot/issues/13
https://github.com/Frama-C/Frama-C-snapshot/issues/14https://git.frama-c.com/pub/frama-c/-/issues/224`strlen` used from code makes it no longer possible to prove `assigns \nothing`.2021-02-22T12:56:40Zmantis-gitlab-migration`strlen` used from code makes it no longer possible to prove `assigns \nothing`.ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002380 | Frama-C | Plug-in > wp | public | 2018-06-23 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | namin | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
`strlen` used from code makes it no longer possible to prove `assigns \nothing`. The definition in the Frama-C library has `@ assigns \result \from indirect:s[0..];`, but this should not prevent check?
### Steps To Reproduce :
$ cat bug.c
#include <string.h>
/*@
requires strlen(s)>=0 && \valid(s+(0..strlen(s)));
assigns \nothing;
*/
int len(char *s) {
return strlen(s);
}
$ frama-c -wp -wp-rte -wp-prover CVC4,alt-ergo bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function len
[wp] 5 goals scheduled
[wp] [Failed] Goal typed_len_assign_normal_part1
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (324ms)
[wp] [Failed] Goal typed_len_assign_exit
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (322ms)
[wp] Proved goals: 3 / 5
Qed: 2 (0.35ms-0.85ms-2ms)
Alt-Ergo: 1 (15ms) (20) (unknown: 2)
CVC4: 0 (interrupted: 2)https://git.frama-c.com/pub/frama-c/-/issues/169One \valid seems sufficient to write in a whole array.2021-02-22T12:55:31Zmantis-gitlab-migrationOne \valid seems sufficient to write in a whole array.ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002426 | Frama-C | Plug-in > wp | public | 2019-02-12 | 2019-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | VincentPenelle | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Linux Manjaro | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am on Chlorine version.
When I try to verify the following function with RTE guard enabled, WP succeeds. However, I think it should not, as only the first cell is specified to be valid, the rest is just specified to have valid read.
/*@ requires \valid(a);
@ requires \valid_read(a + (0 .. n-1));
@ requires 0 <= n <= INT_MAX;
*/
void foo(int *a, int n){
/*@ loop invariant 0 <= i <= n;
@ loop invariant \valid(a + (0 .. n-1));
*/
for (int i = 0; i<n;i++) a[i] = i;
}
Note: that works as well without any loop.
It doesn't work if you declare to pointers with different names, and declare one to be \valid and the other to be \valid_read (like in swap function for example).
It looks like the loop invariant \valid is simplified to true by Qed.
If that's normal, please explain me why.
Thanks,
--
Vincent Penelle.
### Steps To Reproduce :
Specify an array as being \valid_read, and one of its cells to be \valid.
Then, try to write in any cell.
Generate the RTE guards. WP should succeed to prove that the cells you're writing in are \valid.https://git.frama-c.com/pub/frama-c/-/issues/168Division by zero doesn't increase the number of VC in console output2021-02-22T12:55:28Zmantis-gitlab-migrationDivision by zero doesn't increase the number of VC in console outputID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002428 | Frama-C | Plug-in > wp | public | 2019-02-17 | 2019-02-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Obvious division by zero doesn't increase the total number of proof obligations:
Test2:
<pre>
/*@ assigns \nothing;
*/
int test2(int a)
{
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test2.c (with preprocessing)
[rte] annotating function test2
[rte] test2.c:5:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
Proved goals line is the same as in the case without division:
Test1:
<pre>
/*@ assigns \nothing;
*/
int test1(int a)
{
return a;
}
</pre>
Frama-C output:
<pre>
[kernel] Parsing test1.c (with preprocessing)
[rte] annotating function test1
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
From my point of view this is an incorrect behavior and the proved goals like should be 'Proved goals: 1 / 2' as in this case:
Test3:
<pre>
/*@ assigns \nothing;
*/
int test3(int a)
{
//@ assert 0 != 0;
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test3.c (with preprocessing)
[rte] annotating function test3
[rte] test3.c:6:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_test3_assert : Unknown (109ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
</pre>
## Attachments
- [test2.c](/uploads/6a8a966174608d26a4e3aaca44d430f1/test2.c)https://git.frama-c.com/pub/frama-c/-/issues/159Ambiguous path error using why32021-02-22T12:55:18Zmantis-gitlab-migrationAmbiguous path error using why3ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002454 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
### Steps To Reproduce :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
## Attachments
- [example.c](/uploads/ba254a88318716a5e0665ff9fe46d1f4/example.c)https://git.frama-c.com/pub/frama-c/-/issues/151number of generated files in Frama-C 18 vs 19. beta(2)2021-02-22T12:54:59ZJens Gerlachnumber of generated files in Frama-C 18 vs 19. beta(2)ID0002453:
**This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002453:
**This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002453 | Frama-C | Plug-in > wp | public | 2019-06-14 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
This entry references issue
https://github.com/Frama-C/Frama-C-snapshot/issues/21
in order to be able to easily add files.
### Steps To Reproduce :
Run the command
frama-c -pp-annot -no-unicode -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast -wp-model Typed+ref -wp-out rc.wp rc.c
on the attached files.
As mentioned in the github issue, both 18.0 and 19.beta(2) report 17 VC of which 5 are discharged by Qed and the remaining 12 are verified by Alt-Ergo.
However, Frama-C 18.0 generates 12 .mlw and .out files, respectively.
Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files, respectively.
The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged by Alt-Ergo.
## Attachments
- [rc.c](/uploads/12c6518483a56dad661d3ee7feabf59b/rc.c)https://git.frama-c.com/pub/frama-c/-/issues/126Prove of \false2021-04-15T06:50:23ZJens GerlachProve of \falseID0002427:
**This issue was created automatically from Mantis Issue 2427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002427:
**This issue was created automatically from Mantis Issue 2427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002427 | Frama-C | Plug-in > wp | public | 2019-02-16 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the attached program foo.c is analysed with the command line
frama-c -pp-annot -no-unicode -wp -wp-prover alt-ergo -wp-prover eprover foo.c
then the assertion "\false" is verified with "eprover" (2.2).
To me the axiomatics and the lemma look fine which would mean that it is a problem of "eprover".
However, I would like that an WP expert has a look at it before I contact the developer of "eprover".
Thanks in advance.
### Steps To Reproduce :
I am using Frama-C 18.0, Why3 0.88.3, alt-ergo 2.2.0, eprover 2.2.
## Attachments
- [foo.c](/uploads/96dbe2588b177df6328014404f4b189f/foo.c)Loïc CorrensonLoïc Corrensonhttps://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/124incomplete loading of saved state when using WP?2021-02-22T14:00:16ZJens Gerlachincomplete loading of saved state when using WP?ID0002290:
**This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002290:
**This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002290 | Frama-C | Plug-in > wp | public | 2017-03-09 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux/macOS | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I run the line
frama-c -save swap.sav -wp -wp-rte swap.c
on the attached line and then load the saved sate with
frama-c-gui -load swap.sav
I observe the following:
1.) a message in the Frama-C-GUI:"1 state in saved file ingnored. It is invalid in this Frama-C configuration."
2.) the GUI shows which proof obligations have been verified but the tab "WP Goals" does not show any information about which prover was successful
### Additional Information :
I am not sure whether this a problem of the kernel or of the WP plug-in.
## Attachments
- [swap.c](/uploads/68eb8d47535f4c84d136f65f15dec59a/swap.c)https://git.frama-c.com/pub/frama-c/-/issues/122malloc breaks reasoning about assigns2021-02-22T13:34:49Zmantis-gitlab-migrationmalloc breaks reasoning about assignsID0002455:
**This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002455:
**This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002455 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
If a function contains a call to malloc, WP fails to verify its assigns clause.
This could be because malloc does assign to variables in order to track allocation state, but if so there should be a way of specifying that the function assigns to only the listed variables, as well as whatever malloc assigns to. Even duplicating the annotation on malloc will not verify, which includes assigns clauses for the malloc state variables.
### Steps To Reproduce :
# Verify a function with a call to malloc and assigns \nothing
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c -wp-fct f
# Verify a function with the same contract as malloc, which only calls malloc
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c wp-fct malloc_wrapper
## Attachments
- [example.c](/uploads/419009a078988ed9875d2ded26c9f430/example.c)https://git.frama-c.com/pub/frama-c/-/issues/121floating-point support is somwhat incomplete2021-02-22T12:56:27Zmantis-gitlab-migrationfloating-point support is somwhat incompleteID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002459 | Frama-C | Plug-in > wp | public | 2019-07-02 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | florian | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | any | **OS** | any | **OS Version** | any |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi!
Maybe I am doing something fundamentally wrong, but I've tried some simple programs and I don't get anywhere. For example:
/*@ requires x >= 0.0f && x <= 100.0f;
*/
void float_fun(float x)
{
float y = x + 1.0f;
//@ assert y >= 1.0f;
}
I've had a look in share/frama-c/wp/why3/Cfloat.why and I'm not surprised nothing works, the axiomatisation is very incomplete, compared to the current stuff in why3. Could you please port to https://gitlab.inria.fr/why3/why3/blob/master/stdlib/ieee_float.mlw and then use a SMT solver by default that supports it natively (i.e. CVC4 or Z3)?
I know this is a bit of a drastic change, but as it stands WP is not overly useful for anyone trying to do anything with floats (e.g. control systems)...https://git.frama-c.com/pub/frama-c/-/issues/118Mk_addr not defined in Memory.v (coqwp via why3ide)2021-02-22T12:54:05Zmantis-gitlab-migrationMk_addr not defined in Memory.v (coqwp via why3ide)ID0002414:
**This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002414:
**This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002414 | Frama-C | Plug-in > wp | public | 2018-12-07 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | visq | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Memory.Mk_addr is needed for Coq proofs but not in Memory.v (it *is* present in Memory.why).
As a consequence, Coq fails to compile the generated proof scripts for a null pointer check:
> Error: The reference Memory.Mk_addr was not found in the current environment.
### Additional Information :
Frama-c Argon 18.0
Coq 8.6
why3 0.88.3
### Steps To Reproduce :
cat <<EOF >id.c
/*@ requires \valid(p);
ensures *p == \old(*p);
*/
void id(int* p)
{
int tmp;
if (p == (int*)0) return;
tmp = *p;
*p = ~~tmp;
}
EOF
frama-c -wp -wp-rte -wp-split -wp-prover why3ide id.c
# Select Postcondition Line 2
# Coq
# Edit
# Replay
# => Error: The reference Memory.Mk_addr was not found in the current environment.https://git.frama-c.com/pub/frama-c/-/issues/117contracts about memory mapped I/O through volatile memory locations2021-02-22T12:54:04Zmantis-gitlab-migrationcontracts about memory mapped I/O through volatile memory locationsID0002407:
**This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002407:
**This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002407 | Frama-C | Plug-in > wp | public | 2018-10-31 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
We've attached a small example in which a state machine communicates a peripheral through a volatile variable , on line 6 of constants.h:
volatile uint32_t rxBuffer;
The state of the machine is held by a struct mac, declared on line 21 of mac.h:
struct mac {
mac_packet_t mac_packet;
MessageType latestMessage;
mac_bridge_t MAC_BRIDGE_A;
}
the mac_bridge_t represents the machine's memory mapped I/O interface, as declared on line 15 of mac_bridge.h:
struct mac_bridge
{
volatile uint32_t *cmd_rx_buffer;
}
on line 13 of main.c,
mac_t mac = the_mac();
mac becomes a pointer to singleton_mac instance of struct mac declared on line 8 of mac.c and returned by the function the_mac() defined on line 17 of mac.c. On line 14 of main.c,
mac->MAC_BRIDGE_A = theMacBridge();
mac's IO interface MAC_BRIDGE_A becomes the singletonMacBridgeA instance of struct mac_bridge returned by the function theMacBridge() defined on line 11 of mac.c
mac_bridge_t theMacBridge() {
singletonMacBridgeA.cmd_rx_buffer = &rxBuffer;
return &singletonMacBridgeA;
}
thus, mac has as MAC_BRIDGE_A singletonMacBridgeA whose cmd_rx_buffer is a reference to the volatile rxBuffer. The volatile rxBuffer reads and writes from ghost state as given on line 7 of constants.h:
//@ ghost uint32_t injectorAPBBuffer[4294967296];
//@ ghost uint32_t injectorAPBBufferCount=0;
/*@ ghost //@ requires buffer == &(rxBuffer);
@ uint32_t readsBuffer(volatile uint32_t *buffer) {
@ static uint32_t injectorAPBBufferCount = 0;
@ for (int i=0; i<4294967296; i++) {
@ injectorAPBBuffer[i%4294967296]=i%42949967296;
@ }
@ if (buffer == &(rxBuffer)) {
@ return injectorAPBBuffer[injectorAPBBufferCount++];
@ }
@ else
@ return 0;
@ }
@ */
//@ ghost uint32_t bufferAPBCollector[4294967296];
//@ ghost uint32_t bufferAPBCollectorCount = 0;
/*@ ghost //@ requires buffer == &(rxBuffer);
@ uint32_t writesBuffer(volatile uint32_t *buffer, uint32_t v) {
@ if (buffer == &(rxBuffer)){
@ return bufferAPBCollector[(bufferAPBCollectorCount++)%64] = v;
@ }
@ else {
@ return 0;
@ }
@ }
@*/
//@ volatile (rxBuffer) reads readsBuffer writes writesBuffer;
mac implements a transition system driven by an alphabet of labels obtained through calls to macbridge_get_packet, defined on line 3 of mac_bridge.c
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge)
{
mac_packet_t received_packet={0};
received_packet.object_high=(uint8_t)(*(mac_bridge->cmd_rx_buffer));
return(received_packet);
}
when the given macbridge_t is the reference to the singletonMacBridgeA, we want this function to have as postcondition that the packet this function returns has the value found in the appropriate ghost state
/*@
behavior A:
assumes mac_bridge == &singletonMacBridgeA;
ensures \result.object_high == (uint8_t)injectorAPBBuffer[(injectorAPBBufferCount-1)%4294967296];
*/
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge);
The resulting Alt-ergo doesn't seem to capture the post-condition.
(* ---------------------------------------------------------- *)
(* --- Post-condition (file mac_bridge.h, line 24) in 'macbridge_get_packet' --- *)
(* ---------------------------------------------------------- *)
goal macbridge_get_packet_post:
forall t : int farray.
forall t_1 : (addr,int) farray.
forall t_2 : (addr,addr) farray.
forall a : addr.
let a_1 = shiftfield_F7_mac_bridge_cmd_rx_buffer(a) : addr in
let a_2 = t_2[a_1] : addr in
let x = t_1[a_2] : int in
(region(a.base) <= 0) ->
framed(t_2) ->
linked(t) ->
valid_rd(t, a_1, 1) ->
is_uint32(x) ->
valid_rd(t, a_2, 1) ->
(x = to_uint8(x))
## Attachments
- [framaExample.tar.gz](/uploads/ab7c400254275ad87e4710a1a81cafe6/framaExample.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/116crash2021-02-22T12:54:02Zmantis-gitlab-migrationcrashID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002409 | Frama-C | Plug-in > wp | public | 2018-11-13 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.gimbert | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | macosx | **OS** | mojave | **OS Version** | 10.14.1 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp somme.c
with somme.c containing
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
leads to crash
Trace below
### Additional Information :
[kernel] Parsing somme.c (with preprocessing)
[wp] Failure: Unbound logic variable 'f'
[kernel] Current source was: somme.c:4
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 531, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 998, characters 12-50
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 524, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 527, characters 9-16
Called from file "src/plugins/wp/LogicSemantics.ml", line 205, characters 18-38
Called from file "src/plugins/wp/LogicSemantics.ml", line 238, characters 16-32
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "list.ml", line 88, characters 20-23
Called from file "list.ml", line 88, characters 32-39
Called from file "list.ml", line 88, characters 32-39
Called from file "src/plugins/wp/LogicSemantics.ml", line 594, characters 23-52
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "src/plugins/wp/LogicSemantics.ml", line 361, characters 16-35
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 434, characters 28-51
Called from file "src/plugins/wp/LogicSemantics.ml", line 735, characters 39-62
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml", line 399, characters 21-32
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/LogicCompiler.ml", line 485, characters 6-60
Called from file "src/plugins/wp/LogicCompiler.ml", line 741, characters 6-104
Called from file "src/plugins/wp/LogicCompiler.ml", line 758, characters 24-46
Called from file "src/plugins/wp/cfgWP.ml", line 1351, characters 31-42
Called from file "map.ml", line 295, characters 20-25
Called from file "src/plugins/wp/cfgWP.ml", line 1435, characters 19-59
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml" (inlined), line 73, characters 21-47
Called from file "src/plugins/wp/Model.ml" (inlined), line 127, characters 21-45
Called from file "src/plugins/wp/Model.ml" (inlined), line 129, characters 18-36
Called from file "src/plugins/wp/cfgWP.ml", line 1433, characters 14-202
Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 19-28
Called from file "src/plugins/wp/Model.ml" (inlined), line 126, characters 19-36
Called from file "src/plugins/wp/cfgWP.ml", line 1431, characters 10-1023
Called from file "src/plugins/wp/register.ml", line 689, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 301, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 301, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
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 791, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Chlorine-20180502.
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
hugo-9:TP3 gimbert$ cat somme.c
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
## Attachments
- [somme.c](/uploads/5ef73e24f859da4da063d6d4e135ea99/somme.c)https://git.frama-c.com/pub/frama-c/-/issues/115dubious discharge of postcondition2021-02-22T14:00:51ZJens Gerlachdubious discharge of postconditionID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002390 | Frama-C | Plug-in > wp | public | 2018-07-24 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following function
/*@
assigns \nothing;
ensures a == 0;
*/
void foo(int a)
{
a = 0;
}
The postcondition can of course not be verified because the assignment happens to a copy "a" and furthermore nothing is known about the value of "a" in the pre-state.
If I add, however, the admittedly weird looking precondition "requires \valid(&a);" as shown here
/*@
requires \valid(&a);
assigns \nothing;
ensures a == 0;
*/
void bar(int a)
{
a = 0;
}
then Qed discharges the postcondition.
I am not sure this a bug or rather caused by taking the address of a formal argument in the precondition
but in any case it would be nice if someone could have a look at it.
### Steps To Reproduce :
Call
frama-c -wp -wp-rte foo.c
on the attached file.
## Attachments
- [foo.c](/uploads/59eb64f1e1b8ca2563cbfa0bcbb63a83/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/114Newer releases of FramaC produce apparent WP plug-in bug2021-02-22T14:01:18Zmantis-gitlab-migrationNewer releases of FramaC produce apparent WP plug-in bugID0002401:
**This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002401:
**This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002401 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The code in the attached example models a reactive program which interacts with peripherals via memory mapped I/O through an address defined by a constant. While an older version of frama-C (Phosphorus) successfully produced Altergo axiomatizations of boolean logic functions like the "logic boolean isAMessage(mac_t mac)" defined in mac.h,
"
logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_packet.object_low == 0x0A) && (mac->\
mac_packet.payload_length == 0x00));
"
the newer versions produce as AltErgo axiomatization (see out/typed/Axiomatic11.ergo in the attached)
"
function L_isAMessage
() :
bool =
andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))
"
Note that the argument to the boolean logic function is absent and the mac_t fields referenced in the ACSL definition of the logic function have. become "#{w_i}" - this malformed AltErgo (# is illegal in AltErgo) seems to originates from WP's QED module's pretty printer, whose find_var_env function returns these malformed names when it fails to find a given name in its environment.
### Steps To Reproduce :
tar -xvf framaBug.tar.gz
make wp
## Attachments
- [framaBug.tar.gz](/uploads/f07e549fb7296718c7ae0d86fb99b96e/framaBug.tar.gz)
- [frmaBug.tar.gz](/uploads/a43835306fcfcff1aef5bd28e09e0b4d/frmaBug.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/113Auto-generated assigns clause for a void* argument crashes wp2021-02-22T13:34:40Zmantis-gitlab-migrationAuto-generated assigns clause for a void* argument crashes wpID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002385 | Frama-C | Plug-in > wp | public | 2018-07-05 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | schollet | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using an unspecified function with an void* argument from an external file, the default generated assigns clause for that argument crashes frama-c and WP miss-attributes the error to the user.
Specifically, for an unspecified function foo(void* p), the auto generated assigns clause states that the function assigns *((char *)p+(0 .. )), which is then picked up by WP as an invalid user input.
Version : Frama-C 17 Chlorine
### Additional Information :
The command run :
frama-c -wp test2.c
Error log :
[kernel] Parsing test2.c (with preprocessing)
[kernel:annot:missing-spec] test2.c:7: Warning:
Neither code nor specification for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] test2.c:11: User Error: Invalid infinite range i_0+(0..)
[kernel] Plug-in wp aborted: invalid user input.
The auto-generated assigns clause (found with frama-c-gui):
/*@ assigns *((char *)thing + (0 ..));
assigns *((char *)thing + (0 ..)) \from *((char *)thing + (0 ..));
*/
Removing the assigns clause for create stops WP from crashing
### Steps To Reproduce :
run `frama-c -wp test2.c` with those 3 provided files
OR:
Write a function and its specification with at least an assigns clause.
Write in it a call to another function.
Write in another file that 2nd function which takes as an argument an void*.
Write the header and include it in the first file.
For the header and the 2nd file, do not write any specification for the function.
run frama-c -wp on the first file
## Attachments
- [assigns.tar.gz](/uploads/7d8c7280dce8dde42f8cce1f86cbef35/assigns.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/112alt-ergo goals generated directly / via why3 differ in provability2021-02-22T12:53:52ZJochen Burghardtalt-ergo goals generated directly / via why3 differ in provabilityID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002353 | Frama-C | Plug-in > wp | public | 2018-02-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
I generated an Alt-Ergo proof obligation for the ensures clause "xxx" (line 1140) of the attached program "search_n_standalone.c" (which was obtained from "search_n" in "Acsl by example" by "gcc -E -C"). When I did this directly (see attached script "fd"), it was proven without problems. However, when I did this via Why3 (see script "fw"), Alt-Ergo responded "Don't know" after 0.1 seconds.
In order to compare both mlw files given to Alt-Ergo, I moved the goal of the via-Why3 file into the direct file; it became provable there. Removing as many axioms and definitions as possible while keeping the (non-)provability, I obtained the files "xxx_direct.mlw" and "xxx_via_why3.mlw". It seems that the former defines and uses "shift_sint32", while the latter does not (it uses "shift" instead). Probably, this is the reason for the different outcomes of Alt-Ergo.
Although the observed issue may not be bug (both mlw files may be semanically equivalent), it might be desirable to unify the proof obligations given to Alt-Ergo on different pathways.
## Attachments
- [search_n_standalone.c](/uploads/79defa5986c7ebb10060cb2d8013dd27/search_n_standalone.c)
- [fd](/uploads/2325b1feb2a0e2c6bc2768f1552ecbf9/fd)
- [fw](/uploads/ade985efb5f8ea0601fa91f90ec1f340/fw)
- [xxx_direct.mlw](/uploads/49efc095c1124c4e87c110c2b7a10bb7/xxx_direct.mlw)
- [xxx_via_why3.mlw](/uploads/28204d54407af26ed64d8841005b5cef/xxx_via_why3.mlw)https://git.frama-c.com/pub/frama-c/-/issues/111Coq translation of predicate name changes when additional files are processed...2021-02-22T14:00:22ZJochen BurghardtCoq translation of predicate name changes when additional files are processed by Frama-CID0002340:
**This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002340:
**This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002340 | Frama-C | Plug-in > wp | public | 2018-01-04 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | Ubuntu | **OS Version** | Ubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prover coq -wp-prop LowerBoundShift equal_range2_cpp.c" succeeds in proving the lemma in line 16 of "equal_range2_cpp.c", using the Coq proof in file "wp0.script".
However, when "lower_bound_cpp.c" is appended as another command line argument to the same call, the lemma is no longer proven.
Using "wp-out" arguments and running a "diff -r" on the resulting directories reveals that the ACSL predicate name "LowerBound" is translated as "P_LowerBound_1_" for the first (succeeding) run, but as "P_LowerBound_2_" for the second (failing) run.
Note that the definitions of the "LowerBound" predicates literally agree in both C files.
The problem disappears when the overloaded 3-argument version of predicate "LowerBound" is omitted in both C files, or when the contract (i.e. the only use of "LowerBound" in that file) is omitted in file "lower_bound_cpp.c".
## Attachments
- [equal_range2_cpp.c](/uploads/a7f339a24fa1ad2c67458331246b61a8/equal_range2_cpp.c)
- [lower_bound_cpp.c](/uploads/1b5c79b560a67c3ba096b9ce8462c3fc/lower_bound_cpp.c)
- [wp0.script](/uploads/a549eb877d73af8f17c7be0a3cad6d0c/wp0.script)