frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:57:55Zhttps://git.frama-c.com/pub/frama-c/-/issues/266e-acsl-gcc failes on macOS2021-02-22T12:57:55ZJens Gerlache-acsl-gcc failes on macOSID0002369:
**This issue was created automatically from Mantis Issue 2369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002369:
**This issue was created automatically from Mantis Issue 2369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002369 | Frama-C | Plug-in > E-ACSL | public | 2018-02-23 | 2018-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to process the example 'true.i' from http://frama-c.com/eacsl.html
the `e-acsl-gcc.sh` script fails and reports
e-acsl-gcc: fatal error: unexpected output of system getopt
### Additional Information :
This problem does not occur on my Linux installation.Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/264Expose ACSL annotations through host language pragmas2021-04-14T15:05:37Zmantis-gitlab-migrationExpose ACSL annotations through host language pragmasID0002370:
**This issue was created automatically from Mantis Issue 2370. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002370:
**This issue was created automatically from Mantis Issue 2370. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002370 | Frama-C | Kernel > ACSL implementation | public | 2018-03-08 | 2018-03-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pini | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Instead of using comments, that are non-specific constructs and may be mixed with non-ACSL comments from a parser or renderer point of view, would it be possible to use the C standard pragma construct?
Instead of e.g.
```
/*@ requires R: \valid(ptr); @*/
```
this would give either (pragma directive):
```
#pragma ACSL requires R: \valid(ptr);
```
or (pragma operator):
```
_Pragma("ACSL requires R: \valid(ptr);")
```
This would help specify ACSL annotations in a specific language construct and as such expose them properly to outside programs (IDE, editors, documentation generators, etc.)
This could of course co-exist along with the current comment form.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/263frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined size...2021-04-20T17:20:20Zmantis-gitlab-migrationframa-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002376 | Frama-C | Plug-in > jessie | public | 2018-05-29 | 2018-05-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | foo | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi all,
I'm very new to the frama-c and why ecosystem. I hope it's really a bug with frama-c and not jessie.
The C input is:
#include<stdlib.h>
int main(void) {
char *p =malloc(5);
p[0] = 4;
return 3;
}
I'd like to verify that the write to p[0] goes toa valid address.
$ Frama-c -val -jessie t.c
[kernel] Parsing t.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_mblen_state ∈ [--..--]
__fc_mbtowc_state ∈ [--..--]
__fc_wctomb_state ∈ [--..--]
t.c:4:[value] allocating variable __malloc_main_l4
t.c:5:[value] warning: out of bounds write. assert \valid(p + 0);
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
p ∈ {{ &__malloc_main_l4[0] }}
__retres ∈ {3}
__malloc_main_l4[0] ∈ {4}
[1..4] ∈ UNINITIALIZED
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/stdlib.h:389
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/cil.ml", line 5238, characters 9-67
Called from file "common.ml", line 329, characters 27-46
Called from file "norm.ml", line 1551, characters 11-55
Called from file "norm.ml", line 1571, characters 37-71
Called from file "norm.ml", line 1614, characters 22-47
Called from file "norm.ml", line 1685, characters 19-43
Called from file "src/kernel_services/ast_queries/cil.ml", line 2239, characters 15-31
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 3543, characters 17-35
Called from file "src/kernel_services/ast_queries/cil.ml", line 3572, characters 12-19
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 3576, characters 23-50
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3613, characters 14-38
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3602, characters 5-80
Called from file "src/kernel_services/ast_queries/cil.ml", line 3840, characters 16-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 2323, characters 24-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 3808, characters 5-53
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 6463, characters 17-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 6468, characters 24-33
Called from file "src/kernel_services/ast_queries/cil.ml", line 6470, characters 3-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 6487, characters 15-39
Called from file "common.ml", line 580, characters 2-13
Called from file "norm.ml", line 1959, characters 2-26
Called from file "register.ml", line 158, characters 4-23
Called from file "register.ml", line 278, characters 6-12
Called from file "src/kernel_services/plugin_entry_points/journal.ml", line 442, characters 19-22
Re-raised at file "src/kernel_services/plugin_entry_points/journal.ml", line 457, characters 10-17
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sulfur-20171101.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[kernel] writing journal in file `./.frama-c/frama_c_journal.ml'.
### Additional Information :
I'm using
frama-c Sulfur-20171101
why 2.40
Why3 0.88.3
ocaml 4.06.1
## Attachments
- [frama_c_journal.ml](/uploads/d55e08324ce8dc26fa7317cab9a5d1be/frama_c_journal.ml)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/262Strange difference in generated Coq code between Chlorine and Sulfur2021-02-22T13:37:10ZJens GerlachStrange difference in generated Coq code between Chlorine and SulfurID0002374:
**This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002374:
**This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002374 | Frama-C | Plug-in > wp | public | 2018-05-09 | 2018-06-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This report refers to the BETA-release of Chlorine and affects a couple of Coq-proofs in ACSL by Example:
The problem is like this: If the attached file 'foo.c' is processed with the command line
frama-c -wp -wp-prover coq -wp-out foo.wp foo.c
then it produces in foo.wp among other files the Coq file A_Count.v.
The only difference when using with Frama-C-Sulfur or Frama-C-Chlorine is the following:
diff A_Count.sulfur.v A_Count.chlorine.v
28,32c28,32
< Hypothesis Q_CountSectionHit: forall (i_2 i_1 i : Z),
< forall (t : farray addr Z), forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
< (((t.[ (shift_sint32 a x) ]) = i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
< (((1 + ((L_Count t a i%Z x i_2%Z))) = ((L_Count t a i%Z i_1%Z i_2%Z)))%Z).
---
> Hypothesis Q_CountSectionHit: forall (i_1 i : Z), forall (t : farray addr Z),
> forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((i < i_1)%Z) ->
> ((is_sint32 x_1)) ->
> (((1 + ((L_Count t a i%Z x x_1))) = ((L_Count t a i%Z i_1%Z x_1)))%Z).
It looks like as if the argument 'v' of axiom 'CountSectionHit' has not been translated into Coq.
## Attachments
- [foo.c](/uploads/53423ef104c4f86e7469ef5bb783ec52/foo.c)
- [A_Count.sulfur.v](/uploads/774888275fb8101cef0293aaee7dafa5/A_Count.sulfur.v)
- [A_Count.chlorine.v](/uploads/878201905680422222e1b2e12a40293d/A_Count.chlorine.v)https://git.frama-c.com/pub/frama-c/-/issues/261WP: internal error: only the kernel should set the status of property assumes2021-02-22T12:57:46Zmantis-gitlab-migrationWP: internal error: only the kernel should set the status of property assumesID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002383 | Frama-C | Plug-in > wp | public | 2018-07-04 | 2018-07-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Example:
<pre>
int test(void)
{
int a = 1;
/*@ behavior ok:
assumes a > 0;
ensures \true;
*/
return 3;
}
</pre>
Command:
<pre>
frama-c -wp test.c
</pre>
Log:
<pre>
[wp] [CFG] Goal test_stmt_ok_post : Valid (Unreachable)
[wp] [CFG] Goal test_stmt_ok_assume : Valid (Unreachable)
[kernel] failure: only the kernel should set the status of property assumes
a > 0
[kernel] Current source was: test.c:1
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 568, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 939, characters 6-44
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 9-16
Called from file "src/kernel_services/ast_data/property_status.ml", line 538, characters 4-109
Called from file "src/kernel_services/ast_data/property_status.ml" (inlined), line 551, characters 42-80
Called from file "src/plugins/wp/wpAnnot.ml", line 81, characters 4-71
Called from file "list.ml", line 85, characters 12-15
Called from file "list.ml", line 85, characters 12-15
Called from file "src/plugins/wp/wpAnnot.ml", line 1243, characters 10-38
Called from file "src/plugins/wp/wpAnnot.ml", line 1258, characters 12-28
Called from file "src/plugins/wp/wpAnnot.ml", line 1271, characters 16-68
Called from file "src/plugins/wp/Generator.ml", line 108, characters 4-67
Called from file "map.ml", line 270, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
</pre>
## Attachments
- [test.c](/uploads/2597c1f73c5b7b83511f003173086460/test.c)https://git.frama-c.com/pub/frama-c/-/issues/260Frama-C incompatible with Coq 8.8.02021-02-22T12:57:44Zmantis-gitlab-migrationFrama-C incompatible with Coq 8.8.0ID0002377:
**This issue was created automatically from Mantis Issue 2377. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002377:
**This issue was created automatically from Mantis Issue 2377. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002377 | Frama-C | Opam | public | 2018-05-30 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ramsdell | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i686 | **OS** | Fedora | **OS Version** | 28 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Installation with opam worked well except that it deleted my modern version of Coq!
### Steps To Reproduce :
Install Coq and then install frama-chttps://git.frama-c.com/pub/frama-c/-/issues/259Invalid sizeof(struct) calculation in Sulfur2021-02-22T12:57:43Zmantis-gitlab-migrationInvalid sizeof(struct) calculation in SulfurID0002344:
**This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002344:
**This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002344 | Frama-C | Plug-in > wp | public | 2018-01-19 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abustany | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
FramaC version: Sulfur-20171101 (cannot select it in BTS because of #0002343)
With the following C code:
-------------------------------
#include <stdint.h>
#include <string.h>
typedef struct {
uint8_t a;
uint8_t b;
uint8_t c;
uint16_t d;
uint16_t e;
uint16_t f;
char g[4086];
uint16_t h;
} message_t;
/*@ requires \valid(msg);
@*/
void reset_message(message_t *msg) {
memset(msg, 0, sizeof(message_t));
}
-------------------------------
Running: frama-c -wp -wp-fct reset_message -wp-rte -wp-print err.c
produces the following unprovable goal:
-------------------------------
Assume {
(* Heap *)
Have: (region(msg_0.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, msg_0, 4093).
}
Prove: valid_rw(Malloc_0, shift_sint8(w, 0), 4098).
-------------------------------
Using the Typed+cast model doesn't help.
I'm not really sure how the size of the struct is computed (with regard to alignment or padding), but somehow two different parts of the code seem to disagree here.https://git.frama-c.com/pub/frama-c/-/issues/258opam install why3 failed2021-02-22T12:57:42Zmantis-gitlab-migrationopam install why3 failedID0002373:
**This issue was created automatically from Mantis Issue 2373. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002373:
**This issue was created automatically from Mantis Issue 2373. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002373 | Frama-C | Opam | public | 2018-04-09 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | agrcs | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Mac | **OS** | Mac OS | **OS Version** | 10.13.3 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Following opam installation instructions at http://frama-c.com/install-sulfur-20171101.html#installing-frama-c-on-mac-os-x
all ok when: opam install altgr-ergo why3=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[ERROR] The compilation of conf-gtksourceview failed at "pkg-config --short-errors --print-errors gtksourceview-2.0".
#=== ERROR while installing conf-gtksourceview.2 ==============================#
# opam-version 1.2.2
# os darwin
# command pkg-config --short-errors --print-errors gtksourceview-2.0
# path /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2
# compiler system (4.06.1)
# exit-code 127
# env-file /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2/conf-gtksourceview-1291-1872ec.env
# stdout-file /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2/conf-gtksourceview-1291-1872ec.out
# stderr-file /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2/conf-gtksourceview-1291-1872ec.err
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
The following actions were aborted
∗ install altgr-ergo 1.30
∗ install lablgtk 2.18.6
∗ install ocamlgraph 1.8.8
∗ install why3 0.88.3
∗ install why3-base 0.88.3
The following actions failed
∗ install conf-gtksourceview 2
No changes have been performed
=-=- conf-gtksourceview.2 troobleshooting -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
=> This package relies on external (system) dependencies that may be missing. `opam depext conf-gtksourceview.2' may help
you find the correct installation for your system.
ocaml is 4.06.1
opam is 1.2.2https://git.frama-c.com/pub/frama-c/-/issues/257Issues while installation of Frama-C using OPAM2021-02-22T12:57:40Zmantis-gitlab-migrationIssues while installation of Frama-C using OPAMID0002375:
**This issue was created automatically from Mantis Issue 2375. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002375:
**This issue was created automatically from Mantis Issue 2375. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002375 | Frama-C | Opam | public | 2018-05-23 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Mac OS | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
I am having trouble while installation of frame-C on MacOS. I am trying to install it via OPAM.
I have installed all the dependencies also e.g
(brew install gmp gtk+ gtksourceview libgnomecanvas) but still it is not working.
please see the attached file for detailed error message
## Attachments
- [Terminal_Saved_Output](/uploads/7082f81c36f02c3d9c9831398809ace4/Terminal_Saved_Output)
- [framaC_Output](/uploads/a5124f3a2af8c58f9b21d67edb0a40be/framaC_Output)
- [Frama-CUpgrade](/uploads/2f7687f8cab2e31c03be170677f4b396/Frama-CUpgrade)https://git.frama-c.com/pub/frama-c/-/issues/256Crash on attempt to start framaCIRGen when libs are linked statically and dyn...2021-02-22T12:57:36Zmantis-gitlab-migrationCrash on attempt to start framaCIRGen when libs are linked statically and dynamically.ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002368 | Frama-C | Plug-in > clang | public | 2018-02-15 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DeMaze | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | GNU/Linux | **OS** | Debian | **OS Version** | 9.3 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
On the attempt to install Frama-Clang regularly as described (see
attached file installation.txt), the executable framaCIRGen exits with
an error when executed. The error message points to a problem with
LLVM. In fact, it depicts one commandline option to be registered more
than once. This occurs on the attempt of using Frama-C to parse C++
source code and when the executable framaCIRGen is invoked manually on
the commandline. I get the following error:
<output nr="0" command="./frama-clang-0.0.4/bin/framaCIRGen">
: CommandLine Error: Option 'asm-macro-max-nesting-depth' registered more than once!
LLVM ERROR: inconsistency in registered CommandLine options
</output>
However, this has only been observed ith llvm-5.0 on Debian GNU/Linux
9.3 (my system, see lsb_release_3ffbf_2018-02-10000905) for now. With
llvm 3.9, no such errors happen. Presumably, versions of llvm > 5.0
could also be affected. This seems to be a problem many people have
experienced with llvm related programs [2][3][4][5]. In fact, it has
even been reported for frama-clang [6].
### Additional Information :
Root Cause
==========
As far as my investigations revealed, this problem occurs because of
the linking mechanism on Debian GNU/Linux. On this distribution,
libraries of LLVM are built two-fold:
Static archives (lib*.a):
clangFrontend, clangDriver, clangTooling, clanParse, clangSema,
clangAnalysis, clangEdit, clangAST, clangLex, clangSerialization,
clangBasic, LLVMTransformUtils, LLVMBitReader, LLVMMCParser,
LLVMOption
Shared object (lib*.so):
LLVM-5.0
Therefore, it is tried to link them according to their type (lines 74-77, 82-85):
<output nr="1" command="cat frama-clang-0.0.4/Makefile.clang -n | grep 'USEDLIBS' -A 5 -B 5 ">
69 CFLAGS+=-g
70 CLANG_LINKFLAGS+=-g
71 endif
72
73 #LINK_COMPONENTS := $(TARGETS_TO_BUILD) asmparser support mc
74 USEDLIBS = clangFrontend \
75 clangDriver clangTooling clangParse clangSema \
76 clangAnalysis clangEdit clangAST clangLex clangSerialization \
77 clangBasic LLVMTransformUtils LLVMBitReader LLVMMCParser LLVMOption
78
79 # for use in main Makefile
80 default: $(PLUGIN_DIR)/bin/$(TOOLNAME)
81
82 $(PLUGIN_DIR)/bin/$(TOOLNAME): $(OBJS) $(PLUGIN_DIR)/bin
83 $(PRINT_LINKING) $@
84 $(CXX) $(CLANG_LINKFLAGS) -o $@ \
85 $(OBJS) $(addprefix -l,$(USEDLIBS)) $(LLVM_LIBS) $(CLANG_SYSLIBS) $(CLANG_LINKFLAGS)
86
87 $(PLUGIN_DIR)/bin:
88 $(MKDIR) $@
89
90 clean:
</output>
This results in the following dependencies on dynamic libraries as follows:
<output n="2" command="ldd ./frama-clang-0.0.4/bin/framaCIRGen">
linux-vdso.so.1 (0x00007ffe31ff5000)
libLLVM-5.0.so.1 => /usr/lib/x86_64-linux-gnu/libLLVM-5.0.so.1 (0x00007fb4c4825000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb4c44a3000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb4c419f000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb4c3f88000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb4c3be9000)
libffi.so.6 => /usr/lib/x86_64-linux-gnu/libffi.so.6 (0x00007fb4c39e0000)
libedit.so.2 => /usr/lib/x86_64-linux-gnu/libedit.so.2 (0x00007fb4c37a8000)
librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007fb4c35a0000)
libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb4c339c000)
libtinfo.so.5 => /lib/x86_64-linux-gnu/libtinfo.so.5 (0x00007fb4c3172000)
libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb4c2f55000)
libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x00007fb4c2d3b000)
/lib64/ld-linux-x86-64.so.2 (0x00007fb4c9431000)
libncurses.so.5 => /lib/x86_64-linux-gnu/libncurses.so.5 (0x00007fb4c2b18000)
libbsd.so.0 => /lib/x86_64-linux-gnu/libbsd.so.0 (0x00007fb4c2902000)
</output>
From this output, this assumption can be confirmed because
ligcc_s.so.1 as well as libLLVM-5.0.so.1 occurs. A response on a bug
report of LLVM considers this as rather bad practice
however. Moreover, this is mentioned as a classical problem of LLVM's
"global object-based commandline switch registration" [1]:
"The command line option error is the classical problem one gets due
to the LLVM's global object-based command line switch registration. If
you somehow link the same global object (that registers the command
line option) twice via dynamic loading of the LLVM library twice or
more to the same process, it registers the same command line object
again (when calling the global object initializer), resulting in this
error." [1]
The aforementioned symbol 'asm-macro-max-nesting-depth' occurs both in
libLLVMMCParser.a and libLLVM-5.0.so.1 . Hence, I conjecture these are
the files in conflict.
My Solution
===========
Just link without libLLVMMCParser.a or more precisely, remove
LLVMMCParser from USEDLIBS in Makefile.clang. This seems to work as
C++ code is analyzable again. Please find patches for Makefile.clang
attached which circumvent this problem according to my proposal
(Makefile.clang.patch / Makefile.clang.patch.better). Feel free to
contacting me in case of any further quesions / comments.
References
==========
[1] https://bugs.llvm.org/show_bug.cgi?id=30587#c6
[2] https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=768185
[3] https://bugs.llvm.org/show_bug.cgi?id=31571
[4] http://llvm.1065342.n5.nabble.com/llvm-dev-LLD-and-LLVM-LINK-LLVM-DYLIB-td104570.html
[5] https://github.com/zig-lang/zig/issues/67
[6] https://stackoverflow.com/questions/45647503/errors-when-using-the-frama-clang-plugin
### Steps To Reproduce :
1. Manually install llvm-5.0 as described on https://apt.llvm.org/
2. Download and build frama-clang as described officially with llvm-5.0
3. Execute ./bin/framaCIRGen
## Attachments
- [logs_and_more.tar.xz](/uploads/d2a4d0490b88cd4c21961e8a55ab0ca2/logs_and_more.tar.xz)https://git.frama-c.com/pub/frama-c/-/issues/254Crash when trying to analyse a file with jessie2021-04-15T09:16:54Zmantis-gitlab-migrationCrash when trying to analyse a file with jessieID0002334:
**This issue was created automatically from Mantis Issue 2334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002334:
**This issue was created automatically from Mantis Issue 2334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002334 | Frama-C | Plug-in > jessie | public | 2017-12-06 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abustany | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | 4.7.9 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
When running "frama-c -jessie jessie-crash.c" on the attached file, I get the following crash:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing encoding.c (with preprocessing)
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/__fc_string_axiomatic.h:35
The full backtrace is:
Raised at file "interp.ml", line 2383, characters 5-24
Called from file "interp.ml", line 2644, characters 22-41
Called from file "list.ml", line 70, characters 22-25
Called from file "interp.ml", line 2731, characters 27-66
Called from file "register.ml", line 175, characters 16-32
Called from file "register.ml", line 278, characters 6-12
Re-raised at file "register.ml", line 251, characters 29-103
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (File "interp.ml", line 2383, characters 5-11: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
My packages are at the following version:
frama-c 20170501
why 2.39
why3 0.87.3
ocaml 4.03.0
## Attachments
- [jessie-crash.c](/uploads/d0c7ce11aeaa47a5db5fcf2126955551/jessie-crash.c)https://git.frama-c.com/pub/frama-c/-/issues/253Cannot compile variable length arrays2021-02-22T14:01:19ZArvid JakobssonCannot compile variable length arraysID0001834:
**This issue was created automatically from Mantis Issue 1834. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001834:
**This issue was created automatically from Mantis Issue 1834. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001834 | Frama-C | Plug-in > E-ACSL | public | 2014-07-15 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
The resulting C-code from running Frama-C with E-ACSL on the following program (same as attached):
int main(int argc, char **argv) {
int len = 4;
int data[len];
return 0;
}
cannot be compiled, giving the following error:
bug-vla.c:(.text+0xa74): undefined reference to `alloca'
the code generated is:
[...]
void *alloca(unsigned long);
[...]
int len;
int *data;
unsigned long __lengthofdata;
len = 4;
{
/*sequence*/
__lengthofdata = (unsigned long)len;
data = (int *)alloca(sizeof(*data) * __lengthofdata);
}
[...]
This code does not compile with GCC and the flag -std=c99.
## Attachments
- [bug-vla.c](/uploads/1c4f45e3e9069be2db558c88138b286a/bug-vla.c)https://git.frama-c.com/pub/frama-c/-/issues/252E-ACSL: vla handling2021-02-22T14:01:19Zmantis-gitlab-migrationE-ACSL: vla handlingID0002381:
**This issue was created automatically from Mantis Issue 2381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002381:
**This issue was created automatically from Mantis Issue 2381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002381 | Frama-C | Plug-in > E-ACSL | public | 2018-07-01 | 2018-07-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The code:
<pre>
int main(void)
{
int size = 10;
int array[size];
return 0;
}
</pre>
<pre>
a.out.frama.c:141: undefined reference to `__fc_vla_alloc'
a.out.frama.c:143: undefined reference to `__fc_vla_free'
collect2: error: ld returned 1 exit status
e-acsl-gcc: fatal error: fail to compile/link instrumented code
</pre>https://git.frama-c.com/pub/frama-c/-/issues/251request of clarification about using the address of a formal argument2021-02-22T13:48:48ZJens Gerlachrequest of clarification about using the address of a formal argumentID0002392:
**This issue was created automatically from Mantis Issue 2392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002392:
**This issue was created automatically from Mantis Issue 2392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002392 | Frama-C | Documentation > ACSL | public | 2018-07-25 | 2018-07-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | suspended |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
In #2390 the issue was raised whether functions contracts such as
/*@ requires
\valid(&a);
ensures \false; */
void f(int a) {
return ;
}
are meaningful.
More specifically, the ACSL manual should clarify whether using the address of a formal argument in a precondition is illegal.
(When I see that WP uses such a precondition to verify \false, them I am all in for disallowing it.)
Of course, it would also be nice if Frama-C (the kernel?) would issue a diagnostics.
### Additional Information :
The question also came up about using the address of a formal argument in a postcondition.
For the time being, I don't see it as a meaningful feature.https://git.frama-c.com/pub/frama-c/-/issues/250cast error with reference fields2021-03-30T08:44:29Zmantis-gitlab-migrationcast error with reference fieldsID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002396 | Frama-C | Plug-in > clang | public | 2018-08-24 | 2018-08-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abhishek.anand.iitg@gmail.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | manjaro | **OS Version** | 8/23/3018 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
```
class B {
};
template <typename T>
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
B b;
B & y=b;
A<B> a(y);
}
```
I get the following error:
```
root@27db7a69b96a:/hostshare# frama-c -print refFieldBug.cpp
[kernel] Parsing refFieldBug.cpp (external front-end)
Now output intermediate result
[kernel] refFieldBug.cpp:8: Failure: castTo struct _Z1B -> struct _Z1B *
[kernel] User Error: stopping on file "refFieldBug.cpp" that has errors.
[kernel] Frama-C aborted: invalid user inp
```
I don't see what could be the problem because the following succeeds:
```
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
int x=0;
int & y=x;
A<int> a(y);
}
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/249Model Variables in Frama C2021-02-22T13:33:10Zmantis-gitlab-migrationModel Variables in Frama CID0002397:
**This issue was created automatically from Mantis Issue 2397. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002397:
**This issue was created automatically from Mantis Issue 2397. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002397 | Frama-C | Kernel > ACSL implementation | public | 2018-08-27 | 2018-08-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The model variables in FramaC are giving errors whenever I tried to use them in specification
e.g the following code in ACSL manual complaints at line 3 (unexpected token 'forbidden'):
/* public interface */
//@ model set<integer> forbidden = \empty;
/*@ assigns forbidden;
ensures ! ( \result \in \old(forbidden)) &&
\result \in forbidden && \subset(\old(forbidden),forbidden);
*/
int gen();
p.s: please share if any further examples of model variables available in FramaC?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/248Frama-C GUI manual2021-02-22T12:57:24Zmantis-gitlab-migrationFrama-C GUI manualID0002393:
**This issue was created automatically from Mantis Issue 2393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002393:
**This issue was created automatically from Mantis Issue 2393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002393 | Frama-C | Documentation > manuals | public | 2018-08-09 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | maroneze | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Is there any detailed (stepwise) manual about GUI of Drama-C?
May be I'm missing some points but Could we edit/write new files within GUI interface? GUI seems to be not very user friendly...https://git.frama-c.com/pub/frama-c/-/issues/247Can't compile2021-02-22T13:35:44Zmantis-gitlab-migrationCan't compileID0002391:
**This issue was created automatically from Mantis Issue 2391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002391:
**This issue was created automatically from Mantis Issue 2391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002391 | Frama-C | Kernel > Makefile | public | 2018-07-25 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yurichev | **Assigned To** | virgile | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x64 | **OS** | Ubuntu Linux | **OS Version** | 16.04 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Got this file: https://frama-c.com/download/frama-c-Chlorine-20180502.tar.gz
Unpacked, typed "./configure", then "make" and got:
======================================================================
...
Ocamlc src/libraries/datatype/type.cmi
Ocamlc src/kernel_services/plugin_entry_points/log.cmi
Ocamlc src/libraries/project/project_skeleton.cmi
Ocamlc src/libraries/utils/pretty_utils.cmi
Ocamlc src/libraries/stdlib/integer.cmi
File "src/libraries/stdlib/integer.mli", line 26, characters 9-12:
Error: Unbound module Z
share/Makefile.generic:70: recipe for target 'src/libraries/stdlib/integer.cmi' failed
make: *** [src/libraries/stdlib/integer.cmi] Error 2
======================================================================
## Attachments
- [make_stdout](/uploads/401d9f44f320b484e178a6155274ee0d/make_stdout)
- [make_stderr](/uploads/8ecf375aceb48adc242fde2b25e103a0/make_stderr)
- [config.log](/uploads/cd25941939119614209fbc318815d10f/config.log)https://git.frama-c.com/pub/frama-c/-/issues/246WP is not able to validate a statically declared structure followed by a memset2021-02-22T12:57:18ZPatricia MouyWP is not able to validate a statically declared structure followed by a memsetID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002387 | Frama-C | Plug-in > wp | public | 2018-07-11 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pmo | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
By using a clean way to declare the structure, WP fails to validate the structure but by using a "dirty" way, it works !
#include <string.h>
typedef struct {
int i;
float f;
} stest;
void notclean_but_valid() {
char b[sizeof(stest)];
stest *s = b;
memset(s, 0, sizeof(stest));
}
void clean_but_invalid() {
stest s;
memset(&s, 0, sizeof(stest));
}
### Steps To Reproduce :
frama-c -wp-model typed_cast_ref -wp struc.chttps://git.frama-c.com/pub/frama-c/-/issues/245Losing some cmdline option settings when loading2021-02-22T14:01:18ZJulien SignolesLosing some cmdline option settings when loadingID0000687:
**This issue was created automatically from Mantis Issue 687. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000687:
**This issue was created automatically from Mantis Issue 687. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000687 | Frama-C | Kernel | public | 2011-01-25 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "./bin/viewer.opt -val t.c", then clicking on "Execute": ok -val is correctly set.
BUT running "./bin/toplevel.opt -val -save t.sav t.c" followed by "./bin/viewer.opt -load t.sav", then clicking on "Execute": KO -val is not set anymore.
This behavior only exists for (what is internally called) 'action' parameters. Actually we must precise the exact semantics, and then implement it consistently.