frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2020-10-15T08:53:29Zhttps://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/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/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)https://git.frama-c.com/pub/frama-c/-/issues/88explicitly mention operator precedences when referring to Fig.2.1 "Grammar of...2021-02-22T12:53:14ZJochen Burghardtexplicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manualID0002200:
**This issue was created automatically from Mantis Issue 2200. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002200:
**This issue was created automatically from Mantis Issue 2200. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002200 | Frama-C | Documentation > ACSL | public | 2016-01-04 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Running "frama-c xac2.c" on the attached program results in an error message:
xac.c:20:[kernel] user error: unexpected token ':'
The message disappears if the named subterm "A:1" is put in parantheses.
However, from Fig.2.1 "Grammar of terms" (p.16) in the manual "acsl-implementation-Sodium-20150201.pdf" the derivation
term -----> unary-op term -----> unary-op id : term -----> - A : 1
seems to be perfectly valid.
I suggest that, when referring to Fig.2.1, a note should be added that the grammar should be taken cum grano salis rather than literally, and that operator precedences (probably those shown in Fig.2.4, p.19) apply that aren't reflected in Fig.2.1. A similar note could be added for Fig.2.2 "Grammar of predicates", and maybe also at later places in the manual.
## Attachments
- [xac2.c](/uploads/94352314f819785ca8f8423b18c9805b/xac2.c)https://git.frama-c.com/pub/frama-c/-/issues/105suggest boolean expressions for "-wp-prop" arguments2021-02-22T12:53:37ZJochen Burghardtsuggest boolean expressions for "-wp-prop" argumentsID0002285:
**This issue was created automatically from Mantis Issue 2285. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002285:
**This issue was created automatically from Mantis Issue 2285. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002285 | Frama-C | Plug-in > wp | public | 2017-02-27 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | low | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the semantics of "-wp-prop" arguments is unexplained and difficult to understand, when negation and more than one label is used.
For example, using the attached file, "-wp=prop=A,B,-C" selects l4,l5,l6, whereas "-wp-prop=-C,B,A" selects all but l3, and so does "-wp-prop=A,B,c" (although the set of "C"-labelled lemmas is the complement of that of the "c"-labelled lemmas).
I think, parsing arbitrary boolean expressions (built from "!", "&&", "||") isn't more difficult that the current mechanism, but is easier to describe in the manual and to understand.
Alternatively, "-" could be kept as negation, "," could be used for cunjunction only, and the results of multiple args "-wp-prop=X -wp-prop=Y" could be or-ed together; this would at least allow to express arbitrary sets in disjunctive normal form.
### Additional Information :
Complex set expressions arise when labels are used during proof development to attach prover names (and even options) to properties. Using calls like "frama-c -wp -wp-prop=PROVE_WITH_CVC4 -wp-prover=cvc4 ..." can save a lot of proving time that is normally wasted by unsuccessful attempts by unsuitable provers. Other labels that can save time are "TODO", "NEEDS_LONG_TIMEOUT", etc. This way, boolean expressions arise in a natural way; and the user needs to be sure about their semantics, in order not to overlook proof obligations due to splitting by prover.
## Attachments
- [proptest.c](/uploads/969a6dcaeb4f45e418845f21976d9cb7/proptest.c)
- [bbb.c](/uploads/5672cfb09ff165d83ff4c8efc35aacbd/bbb.c)https://git.frama-c.com/pub/frama-c/-/issues/106suggest unique term normalization for lemmas and goals2021-02-22T12:53:39ZJochen Burghardtsuggest unique term normalization for lemmas and goalsID0002329:
**This issue was created automatically from Mantis Issue 2329. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002329:
**This issue was created automatically from Mantis Issue 2329. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002329 | Frama-C | Plug-in > wp | public | 2017-10-09 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501 | **OS** | - | **OS Version** | xubuntu 17.04 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prop g aaa.c" on the attached file fails to prove the assertion "g", although it obviously follows from "f" by applying lemma "lem". One reason for that is of course the inherent incompleteness of SMT provers like Alt-Ergo and Cvc4. However, another reason is that Frama-C's term normalization(1) swaps some arguments of "+", and
(2) performs swaps in the lemma that differ from those performed in the goal.
As a result, in the attached mlw file,
"(L_Foo(a,b+c)=true) -> (L_Bar(a,c+d)=true)"
appears in the lemma, while "(L_Foo(a,i_1+i_2)=true) -> (L_Bar(a,i+i_1)=true)" appears in the goal. The latter is equivalent to
"(L_Foo(a,c+b)=true) -> (L_Bar(a,d+c)=true)"
when expressed in a notation closer to the source-code. Variable "c" is common to L_Foo and L_Bar; note its different positions in the lemma vs. in the goal.
If the goal is changed to "(L_Foo(a,i_2+i_1)=true) -> (L_Bar(a,i_1+i)=true)", it syntactically matches the lemma, and Alt-Ergo proves it in a few milliseconds.
Unless there are good reasons to swap the arguments of "+", they should be kept in their source-code order; this way, the user has a chance to control what is given to the provers.
However, if there *are* good reasons to include argument swapping in term normalization, it should be performed in the same way both in lemmas and in goals.
A possible explanation for the above behavior of Frama-C is that, for some
reason, source-code variable names are transformed to unrelated internal names
in goals, but not in lemmas, and that term normalization just orders arguments
of commutative functions lexicographically (cf. issue #2100).
## Attachments
- [aaa.c](/uploads/86f4cf4ef5586dff6d49e1d6d35ff66e/aaa.c)
- [main_assert_g_Alt-Ergo.mlw](/uploads/4875bf8644ee1246e06bb880e675a7ad/main_assert_g_Alt-Ergo.mlw)