frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2020-10-02T11:00:15Zhttps://git.frama-c.com/pub/frama-c/-/issues/30Wanted features related to Why3-Coq2020-10-02T11:00:15ZAllan BlanchardWanted features related to Why3-CoqThis is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
...This is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
1. drivers that are only applied to Coq (or any prover), an that can be verified,
2. user defined (restricted) context for the proof of lemmas in Coq.
### Drivers
This shall be the job of the driver. We probably need to a way to refine the why3 context *per prover*. Then, it is easy to enrich the Task generated by `ProverWhy3`, which is already « prepared » in a specific way for each prover.
Currently, the supported import directives for WP drivers are:
```
why3.file="mydir/foo.why"
why3.file="mydir/foo.why:Bar"
why3.file="mydir/foo.why:Bar:T"
why3.import="foo.Bar"
why3.import="foo.Bar:T"
```
@lcorrenson suggests to reformulate all of them into something fully understandable from why3 users:
```
[for "myProver",...] loadpath "path/to/dir";
[for "myProver",...] import foo.Bar [as T];
```
This is indeed more flexible than using our custom `meta` directives.
### Restricted context
If we have two files like:
```c
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
```c
lemma Bar: // ...
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
The two files generate different proof contexts for lemmas, because even if `To_Prove` only needs `Foo`, WP collects all lemmas that appear before `To_Prove`. This is why I suggest to provide the user with a way to specify precisely the proof context so that it can remain the same from a file to another.
I think we could create an ACSL extension like:
```c
/*@
lemma Foo: ...
lemma Bar: ...
lemma Proved_with_Coq: ...
lemma_dependencies Proved_with_Coq: Foo ;
*/
```
So that the user can restrict the proof context of the lemma can be as simple and predictable as possible. Note that we should check that it compatible with the `RefUsage` analysis.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/34Frama-C should exit with non-zero if proving failed2020-10-15T08:53:29ZlibguestfsFrama-C should exit with non-zero if proving failed```
$ frama-c -wp -wp-rte snippets/range_size.c
[kernel] Parsing snippets/range_size.c (with preprocessing)
[rte] annotating function range_size
[wp] 4 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_range_size_ensures : Timeout (Qed:2...```
$ frama-c -wp -wp-rte snippets/range_size.c
[kernel] Parsing snippets/range_size.c (with preprocessing)
[rte] annotating function range_size
[wp] 4 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_range_size_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 3 / 4
Qed: 1 (0.50ms-0.78ms)
Alt-Ergo 2.2.0: 2 (13ms-15ms) (80) (interrupted: 1)
```
Proving failed, but frama-c still exits with a zero exit code:
```
$ echo $?
0
```
This problem makes it harder to use frama-c from automated CI systems.https://git.frama-c.com/pub/frama-c/-/issues/28[wp] Infinite loop related to WP cache.2020-10-22T07:22:50ZVeenstra[wp] Infinite loop related to WP cache.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...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.1 (Scandium)*
- Plug-in used: *WP*
- OS name: *Ubuntu 20.04.1 LTS (Focal)*
- OS version: *Linux xxxxx 5.4.0-47-generic #51-Ubuntu SMP Fri Sep 4 19:50:52 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
* Extract the attached zip file: [pillow_src.zip](/uploads/37620f35fc603a9347a7748c54263389/pillow_src.zip)
* Run the following command in the root of the extracted folder: `rm -rf .frama-c/wp/cache; frama-c-gui -verbose 5 -debug 5 -wp -wp-rte -wp-out wp_out -wp-log a:wp.log -wp-timeout 10 -wp-cache update -wp-status-all -wp-par 8 -wp-model "+cast" -wp-prover coq,cvc4,alt-ergo,z3,script,tip "-cpp-extra-args=-I .frama-c-build " libImaging/FliDecode.c`
* Wait for the verification to run.
* In the file list, scroll down to `libImaging/FLIDecode.c` and open it. (maybe also click on a contract in the left source pane)
* Click `Configure and run analyses`.
* Activate the `WP` plugin.
* Click `Cancel`.
* Click `Reparse source files, and replay anayses`.
* The progress bar should appear and disappear right after.
* Check the `Console` tab and scroll down for the repeating messages. Example contents: [console_contents.txt](/uploads/7ba7ee5e95e74948b9412bd6a6605021/console_contents.txt)
* Bonus steps:
* Wait. Check out all those messages!
* Wait longer. Get bored by all the messages.
* Now click the `Console` tab contents, press `ctrl+a`, and press `ctrl+c`.
* If nothing happens wait for more text to appear and try again (work within a minute for me).
* The terminal states something like:
```
The program 'frama-c-gui' received an X Window System error.
This probably reflects a bug in the program.
The error was 'BadWindow (invalid Window parameter)'.
(Details: serial 19490411 error_code 3 request_code 18 minor_code 0)
(Note to programmers: normally, X errors are reported asynchronously;
that is, you will receive the error a while after causing it.
To debug your program, run it with the --sync command line
option to change this behavior. You can then get a meaningful
backtrace from your debugger if you break on the gdk_x_error() function.)
```
It is quite hard to reproduce this consistently, so let me know if I need to try harder to create a proper example.
# Expected behaviour
The analyses upon opening should be executed again upon hitting the replay button.
It should however be faster as most results should be cached.
# Actual behaviour
The verifier goes into an infinite loop after solving a few problems.
Not sure if the bonus steps are related to Frama-C, GTK, or my WM.
# Fix ideas
None, sorry.
I suspect the WP cache is at fault, because deleting that made the crash more consistent.
Also there might be a difference between the `Configure and run analyses` + `Execute` and the `Reparse source files, and replay analyses`, as the program only seems to crash when running the analyses using the reparse button. Also the number of goals generally differs between the two.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/50[Why3 Error] Type mismatch between ieee float.Float32.t and real2021-01-07T13:14:10ZBaptistePollien[Why3 Error] Type mismatch between ieee float.Float32.t and real# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0 (Titanium)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *Ubuntun 20.04.1 LTS*
*Please add specific information deemed relevant with regard...# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0 (Titanium)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *Ubuntun 20.04.1 LTS*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
1. Downloads the [test_frama-c.c](/uploads/b740dd6546da025a730cb737d15ea96b/test_frama-c.c) file. This file contains 3 functions
(`test_1, test2` and `test_3`) which are functionally identical but
differ by the added asserts.
2. Run the command : `frama-c-gui -wp -wp-model real -wp-prover alt-ergo,z3-ce,cvc4-strings-ce -rte test_frama-c.c`
# Expected behaviour
All the goals should be proved.
# Actual behaviour
Only the function `test_2` is verified, but the functions `test_1` and `test_3` are not verified and I get from Why3 the error:
`[Why3 Error] Type mismatch between ieee_float.Float32.t and real`
I also tested with the `-wp-prover native:alt-ergo` and `-wp-model` with the same result.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/33z3 ERROR: unknown parameter 'model_compress'2021-02-22T12:52:03Zlibguestfsz3 ERROR: unknown parameter 'model_compress'Apparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258
Use z3 4.8.9, turn on debugging.
```
<6.827036,ca...Apparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258
Use z3 4.8.9, turn on debugging.
```
<6.827036,call_prover>Call_provers: actual command is: z3 -smt2 -t:10000 sat.random_seed=42 model_compress=false nlsat.randomize=false smt.random_seed=42 -st /tmp/why_b9efc2_zilch-T-wp_goal.smt2
ERROR: unknown parameter 'model_compress'
```https://git.frama-c.com/pub/frama-c/-/issues/55z3 ERROR: unknown parameter 'model_compress'2021-02-22T12:52:03Zrwmjonesz3 ERROR: unknown parameter 'model_compress'ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002509 | Frama-C | Plug-in > wp | public | 2020-10-15 | 2020-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rwmjones | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Apparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258
### Steps To Reproduce :
Use z3 4.8.9, turn on debugging.
<6.827036,call_prover>Call_provers: actual command is:
z3 -smt2 -t:10000 sat.random_seed=42
model_compress=false nlsat.randomize=false
smt.random_seed=42 -st
/tmp/why_b9efc2_zilch-T-wp_goal.smt2
ERROR: unknown parameter 'model_compress'https://git.frama-c.com/pub/frama-c/-/issues/56Frama-C reports “invalid ghost in extern linkage specification” while loading...2021-02-22T12:52:05Zmantis-gitlab-migrationFrama-C reports “invalid ghost in extern linkage specification” while loading filesID0002507:
**This issue was created automatically from Mantis Issue 2507. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002507:
**This issue was created automatically from Mantis Issue 2507. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002507 | Frama-C | Kernel | public | 2020-06-06 | 2020-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dgenin | **Assigned To** | AllanBlanchard | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | x86 | **OS** | Ubuntu | **OS Version** | 19.10 |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
As I try to load my project files Frama-C reports the following error in the Console window and stops processing
[kernel] FRAMAC_SHARE/libc/__fc_alloc_axiomatic.h:30:
invalid ghost in extern linkage specification:
Location: between lines 30 and 45, before or at token: }
28 #include "__fc_define_wchar_t.h"
29
30 __BEGIN_DECLS
31
32 /*@ ghost extern int __fc_heap_status __attribute__((FRAMA_C_MODEL)); */
33
34 /*@ axiomatic dynamic_allocation {
35 @ predicate is_allocable{L}(integer n) // Can a block of n bytes be allocated?
36 @ reads __fc_heap_status;
37 @ // The logic label L is not used, but it must be present because the
38 @ // predicate depends on the memory state
39 @ axiom never_allocable{L}:
40 @ \forall integer i;
41 @ i < 0 || i > __FC_SIZE_MAX ==> !is_allocable(i);
42 @ }
43 */
44
45 __END_DECLS
46
47 __POP_FC_STDLIB
### Steps To Reproduce :
not surehttps://git.frama-c.com/pub/frama-c/-/issues/57cabs2cil fails with statements in expression in a question2021-02-22T12:52:05Zmantis-gitlab-migrationcabs2cil fails with statements in expression in a questionID0002508:
**This issue was created automatically from Mantis Issue 2508. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002508:
**This issue was created automatically from Mantis Issue 2508. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002508 | Frama-C | Kernel | public | 2020-06-10 | 2020-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | JoGi | **Assigned To** | AllanBlanchard | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 18.04 LTS |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When you have a statement in expression ( https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html ) in a question expression for example « 0 ? ({ printf("1"); }): ({ printf("1"); }); », the type-checker fails.
### Additional Information :
If the question expression is not a statement itself (but, for example, a right-value) then the type checking doesn't fail.
### Steps To Reproduce :
frama-c ex_stmt_exp.c -kernel-debug 1
Should do the trick.
## Attachments
- [ex_stmt_expr.c](/uploads/2d4741c184558b10f5cdc5845bea5ed8/ex_stmt_expr.c)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/59error in generated proof obligation2021-02-22T12:52:08ZJens Gerlacherror in generated proof obligationID0002501:
**This issue was created automatically from Mantis Issue 2501. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002501:
**This issue was created automatically from Mantis Issue 2501. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002501 | Frama-C | Plug-in > wp | public | 2020-03-10 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | AllanBlanchard | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, macOS | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
The attached file 'issue.c' contains a simplified (but still not very small) example of an issue I have within ACSL by Example.
There is lemma R_2 for the logic function R.
The definition of R uses the logic function F contained in the axiomatic block A.
When trying to verify R_2 with the command line below I obtain the message
[Why3 Error] anomaly: Failure("Can't find 'L_F' in why3 namespace")
frama-c -wp -wp-prover alt-ergo -wp-prover native:coq issue.c
[kernel] Parsing issue.c (with preprocessing)
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
[wp] [Failed] Goal typed_lemma_R_2
Alt-Ergo 2.3.1: Failed
[Why3 Error] anomaly: Failure("Can't find 'L_F' in why3 namespace")
Coq: Unknown
[wp] [Cache] found:1
[wp] Proved goals: 1 / 2
Qed: 0
Coq: 0 (unknown: 1)
Alt-Ergo 2.3.1: 1 (10ms) (23) (cached: 1) (failed: 1)
When looking at the generated verification condition with Coq I found the following:
The generated hypothesis 'FixL_R' uses of course the function 'L_F'.
However, the necessary import clause 'Require Import A_A.' comes only AFTER the definition of 'FixL_R'.
### Additional Information :
There is a work-around by calling the helper function 'Fix' in the definition of R (see the comment in the code).
The problem also "disappears' if lemma 'R_1' is removed (but I don't have this option).
While looking at this problem, I noticed that in general coq definitions and import clauses are interspersed in the verification conditions...
## Attachments
- [issue.c](/uploads/e4b3b207592281459b4d9e552d904f4a/issue.c)https://git.frama-c.com/pub/frama-c/-/issues/62development version2021-02-22T12:52:13Zmantis-gitlab-migrationdevelopment versionID0002502:
**This issue was created automatically from Mantis Issue 2502. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002502:
**This issue was created automatically from Mantis Issue 2502. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002502 | Frama-C | Plug-in > Eva | public | 2020-03-12 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | puccetti2 | **Assigned To** | buhler | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | MacOS X | **OS** | - | **OS Version** | 10.15.3 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
Running EVA on the small example leads to a cash
### Additional Information :
<pre>
$ frama-c max_array2.c -val
[kernel] Parsing max_array2.c (with preprocessing)
[kernel:parser:decimal-float] max_array2.c:26: Warning:
Floating-point constant 4.6 is not represented exactly. Will use 0x1.2666666666666p2.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] max_array2.c:28: Warning:
function max_array: precondition ∀ ℤ j;
0 ≤ j < n ⇒ \valid_read(t + j) got status unknown.
[kernel] Current source was: max_array2.c:15
The full backtrace is:
Raised at file "src/plugins/value/legacy/eval_terms.ml", line 1264, characters 9-21
Called from file "src/plugins/value/legacy/eval_terms.ml", line 1030, characters 13-41
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2127, characters 18-66
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2308, characters 4-20
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 284, characters 10-49
Called from file "src/plugins/value/engine/transfer_logic.ml", line 663, characters 25-61
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_logic.ml", line 660, characters 10-488
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 377, characters 8-69
Called from file "src/plugins/value/engine/iterator.ml", line 381, characters 17-61
Called from file "src/plugins/value/engine/partition.ml", line 481, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 469, characters 8-57
Called from file "src/plugins/value/engine/iterator.ml", line 556, characters 12-45
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 542, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 604, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 774, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 210, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 230, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 307, characters 10-43
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 445, characters 22-60
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 26-75
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 745, characters 10-447
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 760, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 733, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 277, characters 6-47
Called from file "src/plugins/value/engine/partition.ml", line 481, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 498, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 545, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 542, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 604, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 774, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 210, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 343, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (File "src/plugins/value/legacy/eval_terms.ml", line 1264, characters 9-15: Assertion failed).
</pre>
### Steps To Reproduce :
frama-c-gui max_array2.c -val
## Attachments
- [max_array2.c](/uploads/c74e3cd843af6300cad5464a4aa9d6cc/max_array2.c)https://git.frama-c.com/pub/frama-c/-/issues/63unistd.h declares __fc_ttyname but it has no definition2021-02-22T12:52:15Zmantis-gitlab-migrationunistd.h declares __fc_ttyname but it has no definitionID0002489:
**This issue was created automatically from Mantis Issue 2489. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002489:
**This issue was created automatically from Mantis Issue 2489. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002489 | Frama-C | Kernel > libc | public | 2020-01-08 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vkraus | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | opam | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
When compiling __fc_runtime.c, I get
/usr/bin/ld: __fc_runtime.o:(.data.rel+0x0): undefined reference to `__fc_ttyname'
collect2: error: ld returned 1 exit status
### Additional Information :
gcc version 8.3.0 (debian buster)
frama-c version 20.0 (Calcium)
### Steps To Reproduce :
gcc -I$(frama-c -print-share-path)/libc -nostdinc -D__FC_MACHDEP_X86_64 -o __fc_runtime.o -c $(frama-c -print-share-path)/libc/__fc_runtime.c
(ignore the warnings)
echo "int main () { return 0; }" > main.c
gcc main.c __fc_runtime.o
You should get the error.https://git.frama-c.com/pub/frama-c/-/issues/64Unable to right-click on MacOS to drive GUI2021-02-22T12:52:17Zmantis-gitlab-migrationUnable to right-click on MacOS to drive GUIID0002506:
**This issue was created automatically from Mantis Issue 2506. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002506:
**This issue was created automatically from Mantis Issue 2506. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002506 | Frama-C | Graphical User Interface | public | 2020-06-03 | 2020-06-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | markrtuttle | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | MacOS | **OS** | MacOS | **OS Version** | 10.14 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm unable to use the GUI on MacOS.
I have installed Frama-C on MacOS 10.14 with opam using the instructions in Section 2.2.2.2 of the tutorial https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf. The only exception is that the instructions say "brew install gtk+ --with-jasper" and brew says --with-jasper is no longer supported.
I can start the gui with "frama-c-gui main.c" with the abs function from the tutorial, I can browse the abs function, but I'm unable to right click (control click) on anything in the function to start the verification. I'm following the instructions described in Section 2.2.3 of the tutorial.
Can you give me any guidance on how to proceed or how to debug?
Running frama-c from the command line works just fine.https://git.frama-c.com/pub/frama-c/-/issues/71Outdated -rte-all option in RTE manual2021-02-22T12:52:26Zmantis-gitlab-migrationOutdated -rte-all option in RTE manualID0002418:
**This issue was created automatically from Mantis Issue 2418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002418:
**This issue was created automatically from Mantis Issue 2418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002418 | Frama-C | Documentation > manuals | public | 2018-12-14 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jaseg | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | low | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 20-Calcium | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
The frama-c v18.0 RTE manual[1] linked from the RTE website[0] in ch. 3 claims RTE has options -rte-all and -rte-no-all that the actual command line tool does not seem to recognize. I guess this is just outdated info. Note that the option is also mentioned in the text which I guess would have to be updated as well.
Thanks for the great work,
jaseg
[0] https://frama-c.com/rte.html
[1] https://frama-c.com/download/frama-c-rte-manual.pdf
### Steps To Reproduce :
(this is one of the example command lines from the manual)
> dev~/r/l/src <3 frama-c -rte -rte-select f,g -rte-all -rte-mem
> [kernel] User Error: option `-rte-all' is unknown.
> use `frama-c -help' for more information.
> [kernel] Frama-C aborted: invalid user input.
> dev~/r/l/src <3 frama-c -v
> 18.0 (Argon)https://git.frama-c.com/pub/frama-c/-/issues/72opam fails to install frama-c2021-02-22T12:52:32Zmantis-gitlab-migrationopam fails to install frama-cID0002468:
**This issue was created automatically from Mantis Issue 2468. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002468:
**This issue was created automatically from Mantis Issue 2468. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002468 | Frama-C | Opam | public | 2019-07-26 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abutterfield | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Macbook Pro | **OS** | OS X Mojave | **OS Version** | 10.14.5 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
~> opam install frama-c
The following dependencies couldn't be met:
- frama-c → frama-c-base → ocaml < 4.06
base of this switch (use `--unlock-base' to force)
- frama-c → ocaml < 4.08.0
base of this switch (use `--unlock-base' to force)
No solution found, exiting
### Steps To Reproduce :
Followed instructions on https://frama-c.com/install-19.0-Potassium.html#installing-frama-c-on-macos
after doing update/upgraders for both brew and opam - opam and Ocaml already installed.
Attached file shows complete OS X Terminal transcript
## Attachments
- [2019-07-26-frama-c-install-fail.txt](/uploads/bb0f2fb68238e4c4f015d85ff29bf381/2019-07-26-frama-c-install-fail.txt)
- [2019-07-26-retry-after-switch-4-06-1.txt](/uploads/6bbe1ed0e8dd2a9c8eaa9fd01def1538/2019-07-26-retry-after-switch-4-06-1.txt)
- [2019-07-26-retry-after-caveats.txt](/uploads/92013a1d30bfb430a9d76f2ed50e289c/2019-07-26-retry-after-caveats.txt)https://git.frama-c.com/pub/frama-c/-/issues/73Bytecode only compilation fails when linking to stdlib2021-02-22T12:52:37Zmantis-gitlab-migrationBytecode only compilation fails when linking to stdlibID0002378:
**This issue was created automatically from Mantis Issue 2378. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002378:
**This issue was created automatically from Mantis Issue 2378. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002378 | Frama-C | ptests | public | 2018-06-18 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | bytecode-only | **OS** | OpenBSD | **OS Version** | 6.3 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Compiling bytecode only fails with this error:
ocamlfind ocamlc -I ptests -dtypes -vmthread -g -o bin/ptests.byte unix.cma threads.cma str.cma dynlink.cma ptests/ptests_config.ml ptests/ptests.ml
File "ptests/ptests.ml", line 1:
Error: Required module `Uchar' is unavailable
### Steps To Reproduce :
Compile OCaml >=4.03 without optimizing compilers.
Use this compiler to build frama-c
## Attachments
- [patch-configure_in](/uploads/bf282dbc3c08065b0ff2a13f4fb83464/patch-configure_in)
- [patch-Makefile](/uploads/8465ce62432109e8765f692552e038a5/patch-Makefile)
- [patch-configure_in_2](/uploads/0fc49374e72889fac876d95a3de5dd71/patch-configure_in_2)
- [patch-Makefile_2](/uploads/568208604221bf782f915ed5f2ccf1b0/patch-Makefile_2)
- [patch-Makefile_3](/uploads/c238c03a2a9a0c54e559a994b4448f87/patch-Makefile_3)https://git.frama-c.com/pub/frama-c/-/issues/75Failure to detect qed libraries when running wp2021-02-22T12:52:46Zmantis-gitlab-migrationFailure to detect qed libraries when running wpID0002389:
**This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002389:
**This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002389 | Frama-C | Plug-in > wp | public | 2018-07-17 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 17-Chlorine | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
This is not a problem with this particular code, but I will include it anyways for the sake of completeness and reproducibility.
With the following C code "average.c"
=============================================
/*@ ensures \result == \abs(x); */
double abs(double x) {
if (x >= 0) return x;
else return (-x);
}
/*@ requires 0x1p-967 <= C <= 0x1p970;
@ ensures \result == \round_double(\NearestEven, (x+y)/2);
@ */
double average(double C, double x, double y) {
if (C <= abs(x)) return x/2+y/2;
else return (x+y)/2;
}
=============================================
running the command
>frama-c -wp -wp-model +float -wp-prover "why3:coq" -wp-print average.c
produces the following output
=============================================
[kernel] Parsing average.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] average.c:9: Warning:
Builtin \NearestEven not defined
[wp] 2 goals scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
... (less relevant output) ...
=============================================
the line referenced in coq.drv is
"theory qed.Qed meta "realized_theory" "qed.Qed", "Qed" end
### Additional Information :
Product Version: Frama-C-Chlorine-20180501 **not an option in reporting tool**
I reported this here because the error seems to be with the configurations files generated by frama-c in the frama-c/wp directory, but I can't be sure that the problem isn't with why3 itself. I'm still very new to using these tools.
Note: the "Builtin \NearestEven not defined" seems to be a separate bug, referenced here: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-July/005117.html
### Steps To Reproduce :
Installed the following via OPAM
coq 8.8.0 (because 8.8.1+ reports not supported by why3)
why3-coq 1.0.0
frama-c-chlorine-20180501
error persists after uninstalling and re-installing all of the above
## Attachments
- [coq.drv](/uploads/7d46c6d1e6ee9a9a0ee6e60e0dbb72f7/coq.drv)
- [wp.driver](/uploads/9801629381f7c222b5f698622a1d6551/wp.driver)https://git.frama-c.com/pub/frama-c/-/issues/76conditional input annotations result in why3 type errors2021-02-22T12:52:48Zmantis-gitlab-migrationconditional input annotations result in why3 type errorsID0002394:
**This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002394:
**This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002394 | Frama-C | Plug-in > wp | public | 2018-08-23 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | GNU/Linux | **OS Version** | Debian 9 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
I am trying to put conditions on my function specification that specify return values conditioned on special input values. A minimal example is as follows:
/*@ requires 0 <= t <= 1;
@ ensures t == 1.f ==> \result == b;
@ assigns \nothing
*/
float interpolate(float a, float b, float t) { ... }
Why3 (stderr) reports:
===================================================================================
File "/tmp/wp0a3ed9.dir/typed/interpolate_Why3_ide.why", line 20, characters 11-26:
This term has type real -> real, but is expected to have type real
===================================================================================
The "problem line" is "ensures t == 1.f ==> \result == b;"
This seems to be a problem between wp and why3. The error persists with every external prover I use with why3. The list of provers I've tried is [Z3,CVC3,CVC4,Alt-Ergo,Gappa], and the only exception is why3:coq (see issue 0002389).
### Additional Information :
why3 0.88.3
frama-c chlorine 20180502
### Steps To Reproduce :
see attached file "buggy.c"
run:
> frama-c -wp -wp-prover "why3:XXX" buggy.c
where XXX is any prover installed with why3
## Attachments
- [buggy.c](/uploads/323bd028ec39d43d549eae1d88957797/buggy.c)https://git.frama-c.com/pub/frama-c/-/issues/77suggest to provide results of commandl-line "-wp-prop" evaluation in a file i...2021-02-22T12:52:49ZJens Gerlachsuggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directoryID0002371:
**This issue was created automatically from Mantis Issue 2371. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002371:
**This issue was created automatically from Mantis Issue 2371. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002371 | Frama-C | Plug-in > wp | public | 2018-03-22 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
I ran
"frama-c -wp -wp-out without_lemma -wp-gen -wp-prover why3 -wp-prop=-@lemma aaa.c"
and then
"frama-c -wp -wp-out with_lemma -wp-gen -wp-prover why3 aaa.c"
on the attached file.
After that, "diff -r without_lemma with_lemma" reports no difference between both generated directories.
It is clear that Frama-C needs to generate why3 code for the lemma in both cases, since it might be *used* in some proof.
However, as a consequence, there is no information in the generated directories about which lemmas should be proven. It would be nice if in the long run such information could be provided, e.g. in a separate file.
### Additional Information :
Our application scenario is the following:
We run (one of) the above command(s) on a local computer to generate why3 files; then we transfer them to a more powerful remote computer, and run the provers there. On the remote computer, we would like to have the list of lemmas-to-be-proven available.
Note that arbitrarily complex combinations of "-wp-prop" could exclude some lemmas from being proven and include others. Therefore, we don't want to perform the evaluation of command-line args "-wp-prop=..." ourselves again (this is difficult, anyway, cf. #2285).
## Attachments
- [aaa.c](/uploads/ef6c959b3687621110ddcbd77ab2b906/aaa.c)https://git.frama-c.com/pub/frama-c/-/issues/80known, but inferrable, yet not inferred, property not given as precodition to...2021-02-22T12:52:55ZJochen Burghardtknown, but inferrable, yet not inferred, property not given as precodition to proversID0002330:
**This issue was created automatically from Mantis Issue 2330. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002330:
**This issue was created automatically from Mantis Issue 2330. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002330 | Frama-C | Plug-in > wp | public | 2017-10-26 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501 | **OS** | - | **OS Version** | xubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Running "frama-c -wp foo.c -wp-out wp-out -wp-prop=D" on the attached program fails to prove the property D, although it follows immediately from A and C.
A look at the generated file "foo_assert_D_Alt-Ergo.mlw" reveals that the condition "y<=15" from C is not given to Alt-Ergo, while "0<=y" is.
If the former is inserted into the mlw file, Alt-Ergo proves the goal without problems.
Probably, "y<=15" is considered a trivial consequence of "y==(x&0xf)" by Qed; however, it shouldn't, since (e.g.) Alt-Ergo is unable to to infer this: goal C cannot be proven by Alt-Ergo.
### Steps To Reproduce :
Name translation c -> mlw for convenience:
x -> i
y -> x
z -> x_1
## Attachments
- [foo.c](/uploads/2114c61520580b96d2b67fca503e569d/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/86WP warning not clear2021-02-22T12:53:10ZJens GerlachWP warning not clearID0002482:
**This issue was created automatically from Mantis Issue 2482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002482:
**This issue was created automatically from Mantis Issue 2482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002482 | Frama-C | Plug-in > wp | public | 2019-10-22 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, macOS | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
When I run
frama-c -wp -wp-rte -wp-model Typed f.c
on the attached file, I obtain the warning
[wp] Warning: Memory model hypotheses for function 'f':
/*@ behavior typed: requires \separated(p+(..),a); */
void f(int *a);
However, when I add this requirement by removing the corresponding comment in the contract,
then the warning still occurs.
What can I do to make this warning disappear?
## Attachments
- [f.c](/uploads/bec418c0cc734cf361d31b115a8835b1/f.c)