frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:35:41Zhttps://git.frama-c.com/pub/frama-c/-/issues/68unbound logic variable warning for local variable2021-02-22T13:35:41ZJens Gerlachunbound logic variable warning for local variableID0002500:
**This issue was created automatically from Mantis Issue 2500. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002500:
**This issue was created automatically from Mantis Issue 2500. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002500 | Frama-C | Kernel > ACSL implementation | public | 2020-03-10 | 2020-03-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | linux, macOS | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When processing the following lines
/*@
requires 0 < n;
requires \valid(a + (0..n-1));
*/
void foo(int* a, int n)
{
int m = 0;
//@ assert a[m] == \at(a[m],Pre);
}
with 'frama-c -wp label_pointer.c ', I obtain the following error message for the assertion.
[kernel] Parsing label_pointer.c (with preprocessing)
[kernel:annot-error] label_pointer.c:9: Warning:
unbound logic variable m. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "label_pointer.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
To me this looks like a bug or am I missing something crucial here?
(The message does NOT appear when 'Pre' is replaced by 'Here'.)
## Attachments
- [label_pointer.c](/uploads/ef51b56f81d231eaedc46a0d2aea401e/label_pointer.c)https://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/70munmap() breaks WP analysis2023-07-21T13:28:43Zmantis-gitlab-migrationmunmap() breaks WP analysisID0002498:
**This issue was created automatically from Mantis Issue 2498. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002498:
**This issue was created automatically from Mantis Issue 2498. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002498 | Frama-C | Plug-in > wp | public | 2020-02-10 | 2020-02-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | adbq | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | Linux Debian | **OS Version** | Buster (10) |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using unmap() glib function, WP stops analysis with a fatal error "User Error: Invalid infinite range p_1+(0..)".
### Steps To Reproduce :
make frama-c, with appended code snippet.
## Attachments
- [Makefile](/uploads/b3d3d3c48e97cef222db70c65ef942aa/Makefile)
- [test4.c](/uploads/0aa351f38d2e0b1d6c56ae148a58164a/test4.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/91quantifiers over logic types do not restrict to valid instances2021-04-15T09:37:11Zmantis-gitlab-migrationquantifiers over logic types do not restrict to valid instancesID0002497:
**This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002497:
**This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002497 | Frama-C | Plug-in > wp | public | 2020-01-30 | 2020-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amosr | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
When I quantify over an unsigned char, the resulting formula uses the is_uint8 predicate to ensure that it only considers valid uint8s. However, if I define a logic type that contains an unsigned char, there is no corresponding is_ predicate for the logic type:
> //@ type logic_type_with_u8 = value(unsigned char);
This type is represented in the generated formula as an unbounded int rather than an unsigned char. This means that quantifying over the logic type includes more values than are allowed - for example, `\forall logic_type_with_u8 l` has to prove that the predicate is true even for values that won't fit in a u8.
As a concrete example, I expect the following to hold, but it does not:
> lemma u8_is_valid: \forall logic_type_with_u8 n; \exists unsigned char u; n == value(u);
Thanks,
Amos
### Additional Information :
PS. I could not test on the latest version from git - how do I get (read-only) access to the git repository?
### Steps To Reproduce :
Download file logic_type_is_valid.c and run with WP:
> frama-c -wp logic_type_is_valid.c
The lemma in this file should hold, but does not.
## Attachments
- [logic_type_is_valid.c](/uploads/ec550b694fa472b8bd9d08dc35a76d72/logic_type_is_valid.c)Loïc CorrensonLoïc Corrensonhttps://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/100Left pan (file tree and plugin views) inaccessible upon resize in frama-c-gui2022-09-28T11:26:03Zmantis-gitlab-migrationLeft pan (file tree and plugin views) inaccessible upon resize in frama-c-guiID0002486:
**This issue was created automatically from Mantis Issue 2486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002486:
**This issue was created automatically from Mantis Issue 2486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002486 | Frama-C | Graphical User Interface | public | 2019-11-16 | 2019-11-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Nanoboss | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | immediate | **Severity** | major | **Reproducibility** | always |
| **Platform** | Mac | **OS** | MacOS | **OS Version** | 10.15 (19A583) |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I tried to remove the file tree and the plugin view using the slider (the little dots on the left) to have more space. But impossible to access it again as it's positioned really close from the border. Can't click and drag anymore.
Tested on 2 Macs, rebooting the laptop, restarting Frama-c-gui, a complete reinstallation of opam and brew didn't solve the issue. The windows keeps the same dimensions when we restart frama-c. Might come from gtk, but can't find where the windows properties are stored.
### Steps To Reproduce :
Click on the dots on the left pan, drag to the left until it disappears completely and try to drag it back. I suspect that the issue might be similar for the right pan
## Attachments
- ![Capture_d_____cran_2019-11-16____09.13.42](/uploads/18ce155f416a4ce1efb041889022bb08/Capture_d_____cran_2019-11-16____09.13.42.png)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/103Eprover in Frama-C 20 beta2021-04-15T09:36:20ZJens GerlachEprover in Frama-C 20 betaID0002483:
**This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002483:
**This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002483 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
I played a bit with various automatic provers in the beta
alt-ergo (2.3.0), native:alt-ergo (2.3.0), cvc4 (1.6), cvc3 (2.4.1), z3 (4.8.6) are recognized.
Eprover (2.4), on the other hand, is not recognized.
To be honest, Eprover is not such a great prover, but it has helped us discovering inconsistencies in our specifications.
Is there a specific reason, Eprover is not supported?
Attached is the error message.
### Steps To Reproduce :
$ frama-c -wp -wp-rte -wp-prover eprover -wp-out abs.wp abs.c
[kernel] Parsing abs.c (with preprocessing)
[rte] annotating function abs_int
[wp] 6 goals scheduled
[wp] [Eprover 2.4] Goal typed_abs_int_ensures_3 : Failed
[Why3 Error] Unknown printer 'tptp-fof'
[wp] [Cache] not used
[wp] Proved goals: 5 / 6
Qed: 5 (0.60ms-3ms-6ms)
Eprover 2.4: 0 (failed: 1)
## Attachments
- [abs.c](/uploads/07380fd95e05b2515b8f7dec3a1bad41/abs.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/102alt-ergo support in Frama-C 20 beta2021-04-14T07:30:38ZJens Gerlachalt-ergo support in Frama-C 20 betaID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002484 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a hint to (better) describe the transition from using alt-ergo in Frama-C 19 and 20.
If it is already described, then I apologize.
In Frama-C 19 and before one uses
-wp-prover alt-ergo for the native interface and
-wp-prover why3:alt-ergo for the Why3 interface
In Frama-C 20 the respective options are
-wp-prover native:alt-ergo for the native interface and
-wp-prover alt-ergo
I propose that it is described with other things in a short transition document.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/101-wp-out missing output for Why3 provers in Frama-C 20 beta2023-07-21T13:31:03ZJens Gerlach-wp-out missing output for Why3 provers in Frama-C 20 betaID0002485:
**This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002485:
**This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002485 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the attached programme is processed with
frama-c -wp -wp-rte -wp-prover native:alt-ergo -wp-out abs.wp abs.c
then the output directory 'abs.wp/typed' contains three files
abs_ensures_3_Alt-Ergo.mlw
abs_ensures_3_Alt-Ergo.out
abs_ensures_3.ergo
When using the command line
frama-c -wp -wp-rte -wp-prover alt-ergo -wp-out abs.wp abs.c
then the output directory 'abs.wp/typed' contains only the generated proof obligation
abs_ensures_3_Why3_Alt_Ergo_2_3_0.why
(similiarly when using another Why3 prover, such as cvc4)
Is there a way to output also the result for Why3 provers?
## Attachments
- [abs.c](/uploads/9fd4b3dcc0cf8490758da51b696be918/abs.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/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/128Syntax error in reorder_defs.ml after running make2022-09-28T11:13:02Zmantis-gitlab-migrationSyntax error in reorder_defs.ml after running makeID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002480 | Frama-C | Plug-in > clang | public | 2019-10-03 | 2019-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gpajela | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | have not tried |
| **Platform** | Linux x86_64 | **OS** | Ubuntu | **OS Version** | 18.04.3 LTS |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am trying to follow the instructions at https://frama-c.com/frama-clang.html to install Frama-Clang. However, I get a "Syntax error" after I run make:
$ make
Generating .Makefile.plugin.generated
Ocamlc intermediate_format.cmi
Ocamlc intermediate_format_parser.cmi
Ocamlc intermediate_format_parser.cmo
Ocamlc frama_Clang_option.cmi
Ocamlc frama_Clang_option.cmo
Ocamlc fclang_datatype.cmi
Ocamlc fclang_datatype.cmo
Ocamlc reorder_defs.cmi
Ocamlc reorder_defs.cmo
File "reorder_defs.ml", line 310, characters 6-10:
Error: Syntax error
/data/loewenheim/a/gpajela/.opam/default/share/frama-c/Makefile.generic:77: recipe for target 'reorder_defs.cmo' failed
make: *** [reorder_defs.cmo] Error 2
### Additional Information :
I am using Frama-C 19.0 Potassium, which I installed using opam pin. I am using version 2.0.4 of opam. I am using the default versions of OCaml and Clang for this version of Ubuntu: OCaml 4.05.0 and clang version 6.0.0.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/130FieldEngineer2021-02-22T12:54:23Zmantis-gitlab-migrationFieldEngineerID0002476:
**This issue was created automatically from Mantis Issue 2476. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002476:
**This issue was created automatically from Mantis Issue 2476. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002476 | Frama-C | Kernel > ACSL implementation | public | 2019-09-23 | 2019-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | michal | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | random |
| **Platform** | windows7 | **OS** | windows7 | **OS Version** | windows7 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm staff at fieldengineer.com,we have a technical support of telecom engineers.We created the FE Platform to streamline engagement between field engineers and businesses looking for them.https://git.frama-c.com/pub/frama-c/-/issues/129Freelance2021-02-22T12:54:22Zmantis-gitlab-migrationFreelanceID0002477:
**This issue was created automatically from Mantis Issue 2477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002477:
**This issue was created automatically from Mantis Issue 2477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002477 | Frama-C | Kernel > ACSL implementation | public | 2019-09-23 | 2019-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | michal | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | immediate | **Severity** | text | **Reproducibility** | sometimes |
| **Platform** | windows7 | **OS** | windows7 | **OS Version** | windows7 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm staff at fieldengineer.com,we have a technical support of telecom engineers.We created the FE Platform to streamline engagement between field engineers and businesses looking for them.https://git.frama-c.com/pub/frama-c/-/issues/131Can't view publications on the wiki2022-05-09T13:31:47Zmantis-gitlab-migrationCan't view publications on the wikiID0002474:
**This issue was created automatically from Mantis Issue 2474. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002474:
**This issue was created automatically from Mantis Issue 2474. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002474 | Frama-C | Documentation > website | public | 2019-09-10 | 2019-09-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abutterfield | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Clicking the link low down on https://frama-c.com/support.html to acess the wiki to
see list of publications results in a "404 not found" error.
That link is: https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:publications
The shorter link https://bts.frama-c.com/dokuwiki/ also fails with a 404
### Steps To Reproduce :
Try to visit https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:publications
or https://bts.frama-c.com/dokuwiki/François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/134Bytecode only build fail with error 1272021-02-22T13:33:25Zmantis-gitlab-migrationBytecode only build fail with error 127ID0002473:
**This issue was created automatically from Mantis Issue 2473. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002473:
**This issue was created automatically from Mantis Issue 2473. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002473 | Frama-C | Kernel > Makefile | public | 2019-08-23 | 2019-08-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | bobot | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 bytecode only | **OS** | OpenBSD | **OS Version** | -current |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C build fine with native code compilers available, but fails to build
bytecode-only with the following error. I suspect the relevant clue is the _DEP_REDO suffix ?
Generating src/plugins/callgraph/.Makefile.plugin.generated
Generating src/plugins/metrics/.Makefile.plugin.generated
gmake[1]: Entering directory '/usr/obj/pobj/frama-c-19.0/Frama-C-snapshot-19.0'
Ocamldep src/plugins/metrics/.depend
gmake[1]: *** [src/plugins/metrics/.Makefile.plugin.generated:901: src/plugins/metrics/Metrics_DEP_REDO] Error 127
gmake[1]: Leaving directory '/usr/obj/pobj/frama-c-19.0/Frama-C-snapshot-19.0'
Ocamlc src/plugins/aorai/bool3.cmo
gmake: *** [share/Makefile.generic:78: src/plugins/aorai/bool3.cmo] Error 127
### Steps To Reproduce :
Install OCaml without native-code compilers, install dependencies, try to build Frama-C.https://git.frama-c.com/pub/frama-c/-/issues/135E-ACSL: segmentation fault on a simple strlen function2021-02-22T13:33:18Zmantis-gitlab-migrationE-ACSL: segmentation fault on a simple strlen functionID0002472:
**This issue was created automatically from Mantis Issue 2472. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002472:
**This issue was created automatically from Mantis Issue 2472. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002472 | Frama-C | Plug-in > E-ACSL | public | 2019-08-19 | 2019-08-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
E-ACSL successfully generates executable for this example and fails at runtime with segmentation fault error in shadow_alloca function at initialization stage.
<pre>
#include <stddef.h>
#include <stdint.h>
#include <stdio.h>
/*@ requires \exists size_t i; s[i] == '\0' && \valid_read(s+(0..i));
assigns \nothing;
ensures s[\result] == '\0';
ensures \forall size_t j; 0 <= j < \result ==> s[j] != '\0';
*/
size_t strlen(char *s)
{
size_t len;
/*@ loop invariant \forall size_t i; i < len ==> s[i] != '\0';
loop assigns len;
loop variant SIZE_MAX - len;
*/
for(len = 0; s[len] != '\0'; ++len);
return len;
}
int main(int argc, char *argv[])
{
for(int i = 0; i < argc; ++i) {
printf("%s: %d\n", argv[i], strlen(argv[i]));
}
return 0;
}
</pre>
### Additional Information :
$ gdb ./a.out.e-acsl
Temporary breakpoint 1, main (argc=1, argv=0x7fffffffd3e8) at a.out.frama.c:278
278 __e_acsl_memory_init(& argc,& argv,8UL);
Program received signal SIGSEGV, Segmentation fault.
shadow_alloca (ptr=ptr@entry=0x7fffffffd298, size=size@entry=8) at /home/work/.opam/framac/bin/../share/frama-c/e-acsl//segment_model/e_acsl_segment_tracking.h:562
562 prim_shadow[i] = (code << 2);
main function could be simple. For example, fails also in this case:
int main(void)
{
char *str = "0123456789";
printf("%s: %d\n", str, strlen(str));
return 0;
}
### Steps To Reproduce :
$ e-acsl-gcc.sh -c ./strlen.c
$ ./a.out.e-acsl
[1] 26340 segmentation fault (core dumped) ./a.out.e-acsl
## Attachments
- [strlen.c](/uploads/8cc47a4d07786ef1a83cc2d83a9ef725/strlen.c)https://git.frama-c.com/pub/frama-c/-/issues/87frama-c/wp generates invalid why32021-02-22T13:35:23Zmantis-gitlab-migrationframa-c/wp generates invalid why3ID0002471:
**This issue was created automatically from Mantis Issue 2471. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002471:
**This issue was created automatically from Mantis Issue 2471. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002471 | Frama-C | Plug-in > wp | public | 2019-08-13 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abakst | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | macOS | **OS Version** | 10.14 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
There appears to be an issue with some of the `why3` files that get generated from user axiomatic definitions. I've installed `frama-c` using the `nix-pkgs` on the master branch, and hence have version `19.0`, and `why3` version `1.2.0`.
```c
/*@ axiomatic maps { type model_digit = octet | sextet;
logic integer foo(model_digit i);
}
*/
int foo() {
//@assert \forall int i; i == foo(octet);
return 0;
}
```
Given the (silly) program above in `simple.c`, I get the following behavior
```bash
$ frama-c -wp -wp-prover z3-ce simple.c
[kernel] Parsing simple.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] WPOUT/typed/A_maps.why:13: User Error: why3 syntax error
[wp] [z3-ce] Goal typed_foo_assert : Failed
why3 syntax error
[wp] Proved goals: 0 / 1
Why3 (z3-ce): 0 (failed: 1)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
The A_maps.why file contains:
```
(* ---------------------------------------------------------- *)
(* --- Axiomatic 'maps' --- *)
(* ---------------------------------------------------------- *)
theory A_maps
use bool.Bool
use int.Int
use int.ComputerDivision
use real.RealInfix
use Qed.Qed
use int.Abs as IAbs
use map.Map
type a_model_digit | c_octet | c_sextet
function l_foo a_model_digit : int
end
```
The error seems to be on the line (I'd imagine there should be an '=' but I am not a why3 user)
```
type a_model_digit | c_octet | c_sextet
```
### Steps To Reproduce :
Copy the C source into a new file, simple.c, and attempt to run the command:
frama-c -wp -wp-prover z3-ce simple.c
## Attachments
- [bug.c](/uploads/8df040c765825ec3d66d84e371757e44/bug.c)https://git.frama-c.com/pub/frama-c/-/issues/83wrong test path given in Compiling from source - Quick Start"2021-02-22T13:07:21Zmantis-gitlab-migrationwrong test path given in Compiling from source - Quick Start"ID0002469:
**This issue was created automatically from Mantis Issue 2469. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002469:
**This issue was created automatically from Mantis Issue 2469. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002469 | Frama-C | Documentation > website | public | 2019-08-07 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abutterfield | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
In
https://frama-c.com/install-19.0-Potassium.html#compiling-from-source
step 6 suggests a test involving "tests/misc/CruiseControl*.c".
In the Potassium distribution, that needs to be "tests/value/CruiseControl*.c".
I installed from source as a non-superuser, which works
### Steps To Reproduce :
Follow the Quick Start instructions - or simple look at the contents of tests/misc and tests/value in the source distribution.https://git.frama-c.com/pub/frama-c/-/issues/136Crash at "hashtbl.ml", line 4622021-02-22T13:35:08Zmantis-gitlab-migrationCrash at "hashtbl.ml", line 462ID0002467:
**This issue was created automatically from Mantis Issue 2467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002467:
**This issue was created automatically from Mantis Issue 2467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002467 | Frama-C | Kernel | public | 2019-07-26 | 2019-08-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Victor Sverdlin | **Assigned To** | signoles | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | opensuse-tumbleweed | **OS Version** | 20190723 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Raised at file "hashtbl.ml", line 462, characters 17-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
### Additional Information :
(* Frama-C journal generated at 16:46 the 26/07/2019 *)
exception Unreachable
exception Exception of string
[@@@ warning "-26"]
(* Run the user commands *)
let run () =
Project.set_keep_current false;
File.init_from_cmdline ();
Dynamic.Parameter.String.set ""
"/media/sf_home/temp/gps_try/sent_LDRA/src/main.c";
begin try
(* exception Log.AbortError("kernel") raised on: *)
File.init_from_cmdline ();
raise Unreachable
with
| Unreachable as exn -> raise exn
| exn (* Log.AbortError("kernel") *) ->
(* continuing: *)
begin try
(* exception Log.AbortError("kernel") raised on: *)
File.prepare_from_c_files ();
raise Unreachable
with
| Unreachable as exn -> raise exn
| exn (* Log.AbortError("kernel") *) ->
(* continuing: *) raise (Exception (Printexc.to_string exn))
end
end
(* Main *)
let main () =
Journal.keep_file "./.frama-c/frama_c_journal.ml";
try run ()
with
| Unreachable -> Kernel.fatal "Journal reaches an assumed dead code"
| Exception s -> Kernel.log "Journal re-raised the exception %S" s
| exn ->
Kernel.fatal
"Journal raised an unexpected exception: %s"
(Printexc.to_string exn)
(* Registering *)
let main : unit -> unit =
Dynamic.register
~plugin:"Frama_c_journal.ml"
"main"
(Datatype.func Datatype.unit Datatype.unit)
~journalize:false
main
(* Hooking *)
let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
### Steps To Reproduce :
Just open new project and add at least one .c (or .h) file
## Attachments
- [main.c](/uploads/337a510fa380eff8f13edf74a7a7db10/main.c)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)