frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-04-15T06:54:30Zhttps://git.frama-c.com/pub/frama-c/-/issues/413Implicit casting from integer to real causes failure in WP proof generation2021-04-15T06:54:30Zmantis-gitlab-migrationImplicit casting from integer to real causes failure in WP proof generationID0002241:
**This issue was created automatically from Mantis Issue 2241. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002241:
**This issue was created automatically from Mantis Issue 2241. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002241 | Frama-C | Plug-in > wp | public | 2016-07-29 | 2016-07-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL defines the integer type as a subset of the real type. Therefore, it states, implicit casting from integers to reals is allowed, because one is the subset of another. However, when this is done in practice, the WP plugin will generate goals that provers cannot parse, giving a type error.
### Additional Information :
This is confirmed to occur with the alt-ergo and why3 provers.
Tested on both Frama-C Sodium and Aluminum. Sodium produces slightly different errors than Aluminum, but both produce errors.
### Steps To Reproduce :
== Input file (bug.c):
/*@
axiomatic Bug {
logic integer ibug;
logic real rbug = ibug;
}
*/
/*@
requires i == rbug;
*/
void foo(int i);
void main() {
foo(42);
}
== Command to reproduce
frama-c -wp bug.c
== Output
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:13:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
/tmp/wp714796.dir/typed/A_Bug.ergo:7:[wp] user error: Alt-Ergo error:
characters 1-34:typing error: real and int cannot be unified
[wp] [Alt-Ergo] Goal typed_main_call_foo_pre : Failed
characters 1-34:typing error: real and int cannot be unified
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1)
## Attachments
- [bug.c](/uploads/24ea9349eeb21558e55d63d94453b416/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/410Logic with read clauses can have their values invalidated by writes to separa...2021-08-05T09:15:39Zmantis-gitlab-migrationLogic with read clauses can have their values invalidated by writes to separated memory locationsID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002244 | Frama-C | Plug-in > wp | public | 2016-08-08 | 2016-08-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
In some cases, axiomatic logic using reads clauses can be true for a certain memory location, and then become unknown once an unrelated memory location is assigned to. You can even prove the memory locations as separate, but it does not fix the issue.
### Additional Information :
This bug is present on both Frama-C versions Sodium and Aluminum.
### Steps To Reproduce :
== File bug.c:
/*@
axiomatic Axiomatic {
logic boolean property_of_buffer(char *buffer) reads *buffer;
}
*/
/*@
assigns *buffer;
ensures property_of_buffer(buffer);
*/
void foo(char *buffer);
/*@
requires property_of_buffer(buffer);
assigns *buffer;
ensures property_of_buffer(buffer);
*/
int bar(char *buffer);
char buf1[1];
char buf2[1];
void main() {
foo(buf1);
bar(buf1);
foo(buf2);
bar(buf1);
}
== Command to run:
frama-c -wp bug.c
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_main_call_bar_pre : Valid
[wp] [alt-ergo] Goal typed_main_call_bar_pre_2 : Unknown (562ms)
[wp] Proved goals: 1 / 2
Qed: 1
alt-ergo: 0 (unknown: 1)
== Expected behavior: For typed_main_call_bar_pre_2 to prove valid.
## Attachments
- [bug.c](/uploads/40ef28c81962575b7520fa0642241586/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/409Nested scopes may cause issues with the validity of created pointers2021-04-15T08:57:59Zmantis-gitlab-migrationNested scopes may cause issues with the validity of created pointersID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002245 | Frama-C | Plug-in > wp | public | 2016-08-17 | 2016-08-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Upon entering a nested scope (caused by conditional blocks, or even just wrapping parts of code in {}), pointers once known as valid may become unknown in validity. This only seems to occur when more than 1 pointer is being reasoned about in the scope.
### Additional Information :
This bug occurs on both Sodium in Cygwin and Aluminum on Linux.
### Steps To Reproduce :
== Program bug.c:
/*@
ensures \valid(\result);
*/
int* foo();
void main() {
int* x = foo();
{
int y;
//@ assert \valid(x);
//@ assert \valid(&y);
}
}
== Command to run:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:6:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Unknown (51ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
== Expected output:
Both assertions to pass, since x is ensures to be valid, and the & operator always returns a valid pointer.
== Real output:
The pointer we ensure to be valid could not be proven to be valid.
Moving the definition of y to the outer scope fixes this issue, as well as moving the definition of x inside.
## Attachments
- [bug.c](/uploads/cfc99feea8974ba3cb5097bed4bfb3d3/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/405error in Coq file generation2021-04-15T08:59:05ZAlain Giorgettierror in Coq file generationID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002260 | Frama-C | Plug-in > wp | public | 2016-12-03 | 2016-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | giorgetti | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When an ACSL axiomatic in a C file main.c contains a type declaration, say
type t;
the command
frama-c .. -wp main.c -wp-prover coqide ..
generates a wrong line
Parameter fct : Type.
in the file typed_fct/A_coq_.v.
### Additional Information :
Noticed during a meeting with L. CorrensonLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/403workaround for coq-8.5.1 issue?2021-02-22T13:01:28ZJochen Burghardtworkaround for coq-8.5.1 issue?ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002233 | Frama-C | Plug-in > wp | public | 2016-06-16 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Aluminium-20160501 | **OS** | xubuntu16.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
We ran the command
frama-c-gui -cpp-extra-args='-I.' -pp-annot -no-unicode -wp -wp-rte -wp-script wp0.script -wp-model Typed+ref -wp-prop AdjacentDifferenceInverse -wp-coq-timeout 5 -wp-prover coq -wp-par 1 -wp-out adjacent_difference_inverse.wp adi.c
on the attached file "adi.c", using the attached Coq-script "wp0.script".
The goal isn't proven, and when manually starting the Coq Ide, it complains:
Error: The reference Q_UnchangedSection was not found in the current
environment.
However, the lemma "UnchangedSection" is present in lines 28-33 of file "adi.c", and a "Hypothesis Q_UnchangedSection" is present in lines 33-36 of the generated file "adjacent_difference_inverse.wp/typed_ref/Axiomatic.v", which is included in line 33 of file "adjacent_difference_inverse.wp/typed_ref/lemma_AdjacentDifferenceInverse_Coq.v" (i.e. of the file shown in the Coq Ide).
For these reasons, we believe that the behavior is a Coq-8.5.1 problem, not a Frama-c problem. Moreover, the same files cause no problems when Coq-8.5.1 is replaced by Coq-8.4.6.
Nevertheless, in an e-mail to Jens, Loic encouraged us to report the issue here, since Frama-C might provide a workaround for it.
## Attachments
- [adi.c](/uploads/c4c8150d300c94e05ae4078a54bb0388/adi.c)
- [wp0.script](/uploads/7a7bb805cc9c8332faccefd8ebe42e5d/wp0.script)
- [Axiomatic.v](/uploads/9ab08c5dc84284dc5f8412c7ddc95f09/Axiomatic.v)
- [lemma_AdjacentDifferenceInverse_Coq.v](/uploads/d61593407465c9df0f749dc04240e6ea/lemma_AdjacentDifferenceInverse_Coq.v)
- [adi.script](/uploads/9ab0f4bd54640d060c2292833e1bcd01/adi.script)https://git.frama-c.com/pub/frama-c/-/issues/398"Builtin already registered" after Reparse2021-02-22T13:37:10Zmantis-gitlab-migration"Builtin already registered" after ReparseID0002242:
**This issue was created automatically from Mantis Issue 2242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002242:
**This issue was created automatically from Mantis Issue 2242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002242 | Frama-C | Plug-in > wp | public | 2016-07-30 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | khar | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | lubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using frama-c-gui to analyze code that uses arrays or pointers to structs, after a Reparse, the GUI fails to perform further analysis.
### Additional Information :
Step 2 (selecting the function "Foo" rather than the file "repro.c") is needed to work around a possibly unrelated bug where the source viewer doesn't update properly after a Reparse. To reproduce that bug, simply click "repro.c" instead of "Foo" in step 2.
### Steps To Reproduce :
$ cat repro.c:
//@ ensures foo[1] == 1;
void Foo(int* foo) {
foo[1] = 1;
}
$ frama-c-gui repro.c
1. Expand "repro.c" on the file panel.
2. Click "Foo" on the file panel.
3. Right-click the "ensures" annotation in the source panel.
4. Click "Prove property by WP".
5. On the toolbar, click the "Reparse source files, and replay analyses" button.
6. Click "repro.c" on the file panel.
7. Right-click the "ensures" annotation in the source panel.
8. Click "Prove property by WP".
Results: an error dialog with the following text:
Current source was: repro.c:2
The full backtrace is:
Raised at file "hashtbl.ml", line 328, characters 23-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Unexpected error (Failure("Builtin already registered for 'shift_sint32'")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Aluminium-20160501.
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
- [repro.c](/uploads/5cc283fba4536bd3c0702a8ca68141b5/repro.c)https://git.frama-c.com/pub/frama-c/-/issues/397Switch statements seem to be unsound2021-02-22T13:01:13Zmantis-gitlab-migrationSwitch statements seem to be unsoundID0002246:
**This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002246:
**This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002246 | Frama-C | Plug-in > wp | public | 2016-08-19 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ghulette | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | Ubuntu 16.04 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
// Run the following to see the problem:
// $ frama-c -wp -wp-rte bad.c
//
// Frama-C does not detect the error in the ensures condition. You
// can cause WP to report the error by commenting out the case 0 line,
// or by passing the -simplify-cfg option. Maybe a problem with
// switch statements?
int x;
/*@
requires x != 1;
assigns x;
ensures x != 1;
*/
void bad (int e) {
switch (e) {
case 0: break;
case 1: x = 1; break;
}
}
### Additional Information :
$ frama-c --version
Aluminium-20160501
### Steps To Reproduce :
See comments in description.
## Attachments
- [bad.c](/uploads/c873fd1a6a052a79d2354129467bc6fe/bad.c)https://git.frama-c.com/pub/frama-c/-/issues/394Frama-C is unsound when employing both alt-ergo and cvc42021-02-22T13:01:06ZJochen BurghardtFrama-C is unsound when employing both alt-ergo and cvc4ID0002237:
**This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002237:
**This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002237 | Frama-C | Plug-in > wp | public | 2016-06-30 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | xubuntu |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-out out -wp-prover alt-ergo -wp-prover cvc4 bug.c" on the attached file "bug.c" proves both lemmas, although they are both obviously false. A look at file "lemma_Two_Alt-Ergo.mlw" shows that Alt-ergo proved in fact One==>Two, while a look at file "Axiomatic.why" indicates that cvc4 proved in fact Two==>One.
Apparently, the order of lemmas is reversed when piping through "why" - the output generated for coq amounts to "prove One" and "prove One==>Two", similar to that for Alt-ergo.
The problem disappeared when the type of the bound variable "x" was changed to "integer".
## Attachments
- [bug.c](/uploads/4c15388a22c29202e6cb9736f3dc73c9/bug.c)
- [lemma_Two_Alt-Ergo.mlw](/uploads/f03a7de730f37671825be7aed7c67b57/lemma_Two_Alt-Ergo.mlw)
- [Axiomatic.why](/uploads/1dcfeb3bf5a2935354dd3cae6d5c5e0a/Axiomatic.why)
- [0001-WP-Fix-definition-order.patch](/uploads/58c12a1488d50b4d416869447762e3e4/0001-WP-Fix-definition-order.patch)https://git.frama-c.com/pub/frama-c/-/issues/388more prover processes run than expected2021-04-15T08:59:30ZJens Gerlachmore prover processes run than expectedID0002262:
**This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002262:
**This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002262 | Frama-C | Plug-in > wp | public | 2016-12-15 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I start WP with '-wp-par 4' (for example) I often observe that more than 4 prover processes are actually running.
### Additional Information :
I am not sure this is related but:
It happens from time to time that a proof obligations that is verified with '-wp-par 1' and given timeout T
is not verified when using a greater number of processes and the same timeout T.
### Steps To Reproduce :
run WP on example with a sufficiently large number of proof obligations that require more than one theorem prover
## Attachments
- ![screen-shot](/uploads/64bc6ecf07003613b00fa43be854d6b3/screen-shot.png)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/387Why3 warning2021-04-15T09:00:01ZJens GerlachWhy3 warningID0002263:
**This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002263:
**This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002263 | Frama-C | Plug-in > wp | public | 2016-12-16 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running WP I observe the following warning
[Config] reading extra configuration file /Users/jens/.opam/4.04.0/share/frama-c/wp/why3/why3.conf
File "/Users/jens/.opam/4.04.0/share/why3/drivers/smt-libv2.drv", line 34, characters 7-14:
Library file not found: int
The problem occurs both under Linux and macOS.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/385WP inserts unwanted new lines into Coq proofs2021-04-15T09:00:28ZJens GerlachWP inserts unwanted new lines into Coq proofsID0002266:
**This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002266:
**This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002266 | Frama-C | Plug-in > wp | public | 2017-01-02 | 2017-01-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have noticed (since Aluminium) that whenever I work on a Coq proof, then WP adds a newline to all the other Coq proofs in wp0.script (right before "Qed.").
In the long run, it is a bit annoying to have all these empty lines in the coq proofs...Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/384coq 8.5: cannot find Memory.v2021-02-22T13:00:50ZJens Gerlachcoq 8.5: cannot find Memory.vID0002208:
**This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002208:
**This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002208 | Frama-C | Plug-in > wp | public | 2016-02-11 | 2017-01-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
After updating my Frama-C installation through opam to coq.8.5 and why3.0.86.3 I observe the following error. When compiling the attached file with
coqc -R /Users/jens/.opam/system/share/frama-c/wp/coqwp -as "" WP_basics.v
I receive the following error message:
File "./WP_basics.v", line 3, characters 15-21:
Error: Unable to locate library Memory.
With coq.8.4.6 and earlier I did not observe this error.
### Additional Information :
The path '/Users/jens/.opam/system/share/frama-c' points to my Frama-C share.
ls -l /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v
produces
-rw-r--r-- 1 jens staff 10160 11 Feb 10:38 /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v
## Attachments
- [WP_basics.v](/uploads/e9bbf929a84471fcc0ca1d0a5755739b/WP_basics.v)https://git.frama-c.com/pub/frama-c/-/issues/371translation to why3 of int* argument to logic function2021-04-15T08:10:47ZJochen Burghardttranslation to why3 of int* argument to logic functionID0002275:
**This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002275:
**This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002275 | Frama-C | Plug-in > wp | public | 2017-02-02 | 2017-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu 16.04.1 LTS | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover eprover foo.c" proves lemma "foo" in line 7, although it essentially says that no objects of type "int*" exist at all.
The problem disappears if either
(1) the result type "int" of "deref" is changed to "integer" in line 3,
(2) "deref" is inlined at line 5,
(3) "large" is inlined at line 7, or
(4) "large(s) && !large(s)" is simplified to "\false" in line 7.
Using option "-wp-out", and comparing the files "Axiomatic.why" before and after change (1), see attached files "Axiomatic_int.why" and "Axiomatic_integer.why", reveals that the former has an "axiom Q_TL_deref" while the latter does not. This axiom essentially says that any value fetched from an integer array (i.e. a "map addr int" in why3 language) is already an int (i.e. satisfies "is_sint32" in why3 language), which imho is wrong.
When using "-wp alt-ergo" instead of "-wp eprover", the generated mlw files before and after change (1) literally agree, see attached file "lemma_foo_Alt-Ergo_int.mlw" and "lemma_foo_Alt-Ergo_integer.mlw"; they contain no occurrence of "deref" or "large".
The input given to eprover has been intercepted and boiled down as far as possible, resulting in file "foo_eprover_input.p" which is attached for convenience. Its axiom "q_TL_deref" in line 18 is a boiled-down translation of axiom "Q_TL_deref" from the why3 file, and is wrong as argued above.
## Attachments
- [foo.c](/uploads/820f364a77e732e708ee0a21ae3d0123/foo.c)
- [Axiomatic_int.why](/uploads/10f847d1cf681d6ecde0ea21bab12d96/Axiomatic_int.why)
- [Axiomatic_integer.why](/uploads/3493da1d13894db1a171428f9e5c269e/Axiomatic_integer.why)
- [lemma_foo_Alt-Ergo_int.mlw](/uploads/ffc94494f9b1a25f6bc9ff99c712ec1e/lemma_foo_Alt-Ergo_int.mlw)
- [lemma_foo_Alt-Ergo_integer.mlw](/uploads/ee7e41ba4da81b0485dc5e5cc5d53a89/lemma_foo_Alt-Ergo_integer.mlw)
- [foo_eprover_input.p](/uploads/c00d2b593bcbd384b5bc9781d696e9b7/foo_eprover_input.p)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/369Frama-C sleeps too much when discharging trivial goals2021-04-15T09:08:16Zmantis-gitlab-migrationFrama-C sleeps too much when discharging trivial goalsID0002280:
**This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002280:
**This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002280 | Frama-C | Plug-in > wp | public | 2017-02-13 | 2017-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pkhuong | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Linux/x86_64 | **OS** | Linux | **OS Version** | 4.9.0-1-amd64 #1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have a largish C functions that generates ~70K goals (that I'm refactoring away). Verification with WP and RTE assertions succeeds, but takes ~14 minutes of real time. strace shows the majority of that time is spent executing *no syscall* (i.e., not calling external solvers) except printing the progress on stderr, getrusage, and nanosleeping for half a second. I LD_PRELOADed a shared object to turn usleep into a no-op, and that improved the runtime from 14 minutes to 3 minutes.
Could Frama-C sleep less when Qed does all the work?
### Steps To Reproduce :
frama-c slow_qed.c -cpp-gnu-like -no-asm-contracts -constfold -machdep x86_64 -implicit-function-declaration error -wp -wp-rte -wp-extensional -wp-split -wp-init-const -wp-prop="-trustme,-freeable,-@assigns,-@lemma,-@variant" -wp-prover=alt-ergo,Z3:4.5.0
## Attachments
- [slow_qed.c](/uploads/df95dd235b294d5f24c6ca57181db9d4/slow_qed.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/368applicability of Coq proof script depends on order of include files2021-04-15T08:02:31ZJochen Burghardtapplicability of Coq proof script depends on order of include filesID0002282:
**This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002282:
**This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002282 | Frama-C | Plug-in > wp | public | 2017-02-16 | 2017-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
We run "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prop HeapMaximum -wp-prover coq make_heap_cpp.c" on the attached files. In the current form, the Coq proof script "wp0.script" works fine and proved the lemma "HeapMaximum" from file "make_heap_cpp.c".
However, when that lemma is moved after the "axiomatic Count", which is completely unrelated, the same command doesn't work any longer. Using "-wp-out" shows that both versions differ in the location where lemma "HeapBounds" is available in Coq; this make it necessary to change the names used in the proof.
The problem originated from lemma "HeapMaximum" being used for the verification of two different function contracts. For software engineering reasons, the order of #include files was different (since different files were preferred to be included in the ".c", rather than already in the ".h" file). This resulted in "lemma HeapMaximum" appearing before and after an "axiomatic", making "wp0.script" work and not work, respectively.
## Attachments
- [make_heap_cpp.c](/uploads/256c2042ed0e2b08fc7901c42cdcbb49/make_heap_cpp.c)
- [wp0.script](/uploads/7277fc9a7ed0386527de3694d96817e5/wp0.script)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/367lemma tacitly omitted from prover assumptions2021-08-05T09:00:11ZJochen Burghardtlemma tacitly omitted from prover assumptionsID0002286:
**This issue was created automatically from Mantis Issue 2286. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002286:
**This issue was created automatically from Mantis Issue 2286. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002286 | Frama-C | Plug-in > wp | public | 2017-02-27 | 2017-02-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-prop=addIncAdd -wp-prover z3 bug1.c" on the attached file verifies the given goal "addIncAdd" in 40ms. However, when the closing brace is moved from line 35 up to line 30, no proof is found in 10s.
A "diff -r" on the wp-out directories shows that the translation of lemma "incAdd" is put into file "A_addAxioms.why" in the former, but into "Axiomatic2.why" in the latter case.
Intercepting the input if "z3" shows that only in the former case the translation is included in the input of "z3"; in the latter case it is missing.
I couldn't find the reason for just omitting "incAdd": exchanging lemmas "incAdd" and "addAdd" in the C source and comparing the "z3" inputs again shows that still "incAdd" is omitted; so the reason could be in it's name of form, but not in it place in source.
## Attachments
- [bug1.c](/uploads/506733bc64b39e2ab7b3c2d585f33515/bug1.c)
- [why_495d09_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/1b12fd854a0d7471daf0f12f795dc5b4/why_495d09_Axiomatic2-T-Q_addIncAdd.smt2)
- [why_767c25_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/8fbe26071875fc21dea8cfbef1aa6f8d/why_767c25_Axiomatic2-T-Q_addIncAdd.smt2)
- [why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/d92a6c680802a47e1e35e8cd3c5810ad/why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2)Loï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/360suggestion: translate axioms and implication premises in forward order to coq2021-04-15T09:12:22ZJochen Burghardtsuggestion: translate axioms and implication premises in forward order to coqID0002291:
**This issue was created automatically from Mantis Issue 2291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002291:
**This issue was created automatically from Mantis Issue 2291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002291 | Frama-C | Plug-in > wp | public | 2017-03-13 | 2017-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover coq -wp-out wp-out coqtest.c" on the attached file generates two Coq files, viz. "A_eqAxioms.v" and "lemma_goal_Coq.v".
The former contains the translation of "axiomatic eqAxioms", with the axioms ("eqRefl" and "eqTrns") appearing in the same order as in the source. The file "lemma_goal_Coq.v" contains the translation of "axiomatic incAxioms", however, with the axioms ("incLf" and "incRg") appearing in reverse order, compared to the source.
A similar issue concerns the translation of the body formula of axiom "eqTrns", where the first and second premise, viz. "eq(x,y)" and "eq(y,z)" in the source, appear in reverse order in the Coq translation.
(As a side remark: names of locally bound variables could be translated such that a target name closely resembles its source name; for example the source name could appear as a prefix of the target name.)
While probably easy to implement, these suggestions would considerably lower the overall complexity of the user's task.
## Attachments
- [coqtest.c](/uploads/74070de0221ca10812d16c76f7136c21/coqtest.c)
- [A_eqAxioms.v](/uploads/069306903f4c37b11f8f97b4a7df853c/A_eqAxioms.v)
- [lemma_goal_Coq.v](/uploads/231b70565ab0de2adf794e9662aae91e/lemma_goal_Coq.v)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/359Provide an option to run Coq from Frama-C2021-02-22T13:00:10ZJens GerlachProvide an option to run Coq from Frama-CID0001686:
**This issue was created automatically from Mantis Issue 1686. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001686:
**This issue was created automatically from Mantis Issue 1686. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001686 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2017-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
When proving external Coq-lemma for WP it might be interesting to run Coq from Frama-C, e.g.,
frama-c -wp-coq Foo.vhttps://git.frama-c.com/pub/frama-c/-/issues/356Axiomatic is recompiled when using severalprocesses2021-02-22T13:00:08ZJens GerlachAxiomatic is recompiled when using severalprocessesID0001685:
**This issue was created automatically from Mantis Issue 1685. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001685:
**This issue was created automatically from Mantis Issue 1685. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001685 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2017-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When verifying with alt-ergo and coq the file Axiomatic seems to be compiled again and again.
As far as I understood, alt-ergo seems to kill the coq process.
### Steps To Reproduce :
In fact, I noticed this problem in Neon.