frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-03-14T22:21:49Zhttps://git.frama-c.com/pub/frama-c/-/issues/2609WP - unsoundness with union2024-03-14T22:21:49ZGeoff HuletteWP - unsoundness with union```
/* bug.c */
#include <assert.h>
typedef union {
int a[2];
struct {
int a0, a1;
} s;
} T;
/*@
requires \valid(t);
requires t->a[0] == 0;
requires t->s.a0 == 0;
assigns *t;
ensures t->a[0] == 1;
ensures t->s.a0 == 0;
*/
voi...```
/* bug.c */
#include <assert.h>
typedef union {
int a[2];
struct {
int a0, a1;
} s;
} T;
/*@
requires \valid(t);
requires t->a[0] == 0;
requires t->s.a0 == 0;
assigns *t;
ensures t->a[0] == 1;
ensures t->s.a0 == 0;
*/
void foo(T *t) { t->a[0] = 1; }
/*@
assigns \nothing;
*/
int main() {
T t;
t.a[0] = 0;
t.s.a0 = 0;
foo(&t);
//@ assert t.s.a0 == 0;
assert(t.s.a0 == 0);
return 0;
}
```
In a shell:
```
$ frama-c --version
24.0 (Chromium)
$ frama-c -wp -wp-rte bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 18 goals scheduled
[wp] Proved goals: 18 / 18
Qed: 17 (0.74ms-2ms-3ms)
Alt-Ergo 2.3.3: 1 (20ms) (63)
$ clang bug.c
$ ./a.out
a.out: bug.c:29: int main(): Assertion `t.s.a0 == 0' failed.
Aborted (core dumped)
```Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/414suggest to make pdf document searchable again2024-02-21T09:26:46ZJochen Burghardtsuggest to make pdf document searchable againID0002008:
**This issue was created automatically from Mantis Issue 2008. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002008:
**This issue was created automatically from Mantis Issue 2008. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002008 | Frama-Clang | Documentation > ACSL | public | 2014-12-01 | 2016-07-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | - | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the current version of e.g. "acsl-implementation-Neon-20140301.pdf", it is not possible to search for a string: although "the" appears on almost every page, my viewer, "xpdf" doesn't find it. Without the search feature, a user needs to waste a lot of time with scanning though the document to find what (s)he is looking for.
I set the priority to "urgent" since I guess that it is easy to allow for string search again.https://git.frama-c.com/pub/frama-c/-/issues/1310ACSL pretty-printer2023-11-21T14:40:58Zmantis-gitlab-migrationACSL pretty-printerID0000859:
**This issue was created automatically from Mantis Issue 859. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000859:
**This issue was created automatically from Mantis Issue 859. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000859 | Frama-C | Kernel > ACSL implementation | public | 2011-06-09 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ckunz | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Inductive predicates are not printed correctly:
predicates of the form:
inductive .... ( ... ) {
case ...;
case ...;
}
are printed as:
predicate .... ( ... ) {
case ...;
case ...;
}
### Additional Information :
A quick fix consists of modifying cil/src/cil.ml as follows:
*** 5676,5682 ****
fprintf fmt "@[<hov 2>logic %a"
(self#pLogic_type None) rt
| None ->
! fprintf fmt "@[<hov 2>predicate"
end;
fprintf fmt " %a%a%a%a"
self#pLogic_var li.l_var_info
--- 5676,5688 ----
fprintf fmt "@[<hov 2>logic %a"
(self#pLogic_type None) rt
| None ->
! begin
! match li.l_body with
! | LBinductive _ ->
! fprintf fmt "@[<hov 2>inductive"
! | _ ->
! fprintf fmt "@[<hov 2>predicate"
! end
end;
fprintf fmt " %a%a%a%a"
self#pLogic_var li.l_var_infohttps://git.frama-c.com/pub/frama-c/-/issues/982Wrong localisation of not yet supported constructs2023-10-09T13:44:38ZJulien SignolesWrong localisation of not yet supported constructsID0001692:
**This issue was created automatically from Mantis Issue 1692. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001692:
**This issue was created automatically from Mantis Issue 1692. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001692 | Frama-C | Plug-in > E-ACSL | public | 2014-03-13 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | AMD 64 | **OS** | Linux | **OS Version** | Ubuntu |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
===== t.c =====
int main(void) {
//@ assert 2 >> 2 == 0;
return 1;
}
===========
$ frama-c -e-acsl t.c
t.c:1:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
Ignoring annotation.
The warning should be located at line 2, not at line 1.
### Additional Information :
Reported by P.-L. Garoche on Frama-C discuss.https://git.frama-c.com/pub/frama-c/-/issues/2664Tuples are not supported2023-08-08T06:13:21ZAdharsh KamathTuples are not supported## Error while using types and predicates with the WP plugin
### Steps to reproduce the issue
Copy the code snippet from Example 2.35 in Section 2.5.3 in the latest ACSL manual (https://frama-c.com/download/frama-c-acsl-implementation.p...## Error while using types and predicates with the WP plugin
### Steps to reproduce the issue
Copy the code snippet from Example 2.35 in Section 2.5.3 in the latest ACSL manual (https://frama-c.com/download/frama-c-acsl-implementation.pdf) and run Frama-C on this code file, with the WP plugin.
### Expected behaviour
Frama-C should not throw any errors and verify the given method using the predicate.
### Actual behaviour
Multiple errors are reported as follows in the Kernel logs: <br>
[kernel:annot-error] /code.c:4: Warning: unexpected token '('<br>
[kernel:annot-error] /code.c:7: Warning: unexpected token '('<br>
[kernel:annot-error] /code.c:16: Warning: unexpected token ','<br>
which corresponds to the lines:<br>
line 4: //@ type intpair = (integer,integer);<br>
line 7: @ \let (x1,y1) = p1 ;<br>
line 16: @ loop variant (x, y) for lexico;<br>
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.1 (Cobalt)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
### Additional comments
I'm not sure what I'm missing here? Is there some flag I'm supposed to switch on, while using these features? Or use a different plugin?
**Is there any other way of specifying lexicographically ordered terms as a variant in Frama-C?**Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/1028Extend smoke tests to incoherent specification of declared functions2023-07-21T13:48:46ZDillon ParienteExtend smoke tests to incoherent specification of declared functionsID0001537:
**This issue was created automatically from Mantis Issue 1537. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001537:
**This issue was created automatically from Mantis Issue 1537. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001537 | Frama-C | Plug-in > wp | public | 2013-10-28 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[STANCE]
The following code:
```
//@ assigns \result \from p; ensures sizeof(\result)==5;
char*g(char*p);
void f()
{
char *p=g(p);
//@ assert sizeof(p)==5;
//@ assert \false;
}
```
analyzed by:
frama-c foo.c -no-unicode -wp
Qed proves the 2nd assert in f():
[wp] [Qed] Goal typed_f_assert_2 : ValidLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1147Generate proof obligation for drivers when driver instantiate a logic acsl de...2023-07-21T13:21:41ZJens GerlachGenerate proof obligation for drivers when driver instantiate a logic acsl declarationID0001694:
**This issue was created automatically from Mantis Issue 1694. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001694:
**This issue was created automatically from Mantis Issue 1694. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001694 | Frama-C | Plug-in > wp | public | 2014-03-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This would be helpful for proving (in coq) that a model of an ACSL logic function actually exists.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/32Known WP limitation: Dynamic allocation is not supported2023-07-21T13:06:10ZBob RubbensKnown WP limitation: Dynamic allocation is not supportedHello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program...Hello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program.c
[kernel] Parsing program.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint8*) (target: sint32*)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
```
Frama-c version (for completeness, I'm using the version from nixpkgs unstable):
```bash
[nix-shell:~]$ frama-c --version
21.1 (Scandium)
```
The warning seems strange, as I use only ints in this program. With my limited knowledge of C, I'd say this program does no such casting. Is this a bug or is this somehow a subtle edge case in C? Or is it benign and can it be ignored?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/365Why3ide cannot be opened in this version2023-07-21T13:01:20ZPierre Yves PiriouWhy3ide cannot be opened in this versionID0002289:
**This issue was created automatically from Mantis Issue 2289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002289:
**This issue was created automatically from Mantis Issue 2289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002289 | Frama-C | Plug-in > wp | public | 2017-03-01 | 2017-03-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Pierre-Yves Piriou | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | linux 3.2.0-4-amd64 | **OS** | Debian | **OS Version** | 7.11 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I try to open the Why3 IDE from the GUI to edit a proof (right-click on Why3 column, then 'open why3ide'), the "running icon" is displayed but the IDE does not open.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1252the input file should be the first argument to ptests2023-04-21T13:20:33ZJulien Signolesthe input file should be the first argument to ptestsID0000736:
**This issue was created automatically from Mantis Issue 736. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000736:
**This issue was created automatically from Mantis Issue 736. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000736 | Frama-C | ptests | public | 2011-02-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | high | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
all in the title... Required in order to use -then* in tests.https://git.frama-c.com/pub/frama-c/-/issues/1201syntax error in value binary assignment2023-01-31T17:32:45Zmantis-gitlab-migrationsyntax error in value binary assignmentID0000929:
**This issue was created automatically from Mantis Issue 929. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000929:
**This issue was created automatically from Mantis Issue 929. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000929 | Frama-C | Kernel | public | 2011-08-18 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | inti | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I am developing a microcontroller, My code is like this assignment:
LPC_IOCON->PIO0_1=0b00000000000000000000000000000000;
and all of this kind of assignment cause this error in frama-c value analysis
[kernel] preprocessing with "gcc -C -E -I. peripheral-gpio.c"
peripheral-gpio.c:28:[kernel] user error: syntax error
[kernel] user error: skipping file "peripheral-gpio.c" that has errors.
I think the problem is the binary value because when I assign a integer or hexa value the problem disappear.https://git.frama-c.com/pub/frama-c/-/issues/2636[WP] Builtin \sign(float64) is not defined2022-12-14T12:36:37ZNiksonber[WP] Builtin \sign(float64) is not defined<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Description
Built-in \\sign is not defined in WP.
`Builtin \sign(float64) not defined`
`[wp] Failure: Logic type 'sign' undefined`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Steps To Reproduce
Run: `frama-c -wp -wp-out . -wp-prover coq -wp-model +float -wp-interactive update just_sign.c`
Where `just_sign.c` is:
```
#include <math.h>
/*@
predicate is_same_sign(double X, double Y) = \sign(X) == \sign(Y);
*/
/*@
ensures (is_same_sign(a_double, \result)) ;
assigns \nothing;
*/
double dummy (double a_double) {
return a_double;
}
```
I got the following output:
```
[wp] Warning: Missing RTE guards
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] 2 goals scheduled
[wp] Failure: Logic type 'sign' undefined
```
### Expected behaviour
Expected a definition for \sign.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
WP reports:
```
[wp] Failure: Logic type 'sign' undefined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
```
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0, 25.0 (Manganese), 26.0+dev (Iron) (I tried Several versions)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 22.04 LTS
<!--
### Additional information (optional)
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/918Value analysis generates incorrect Imperative outputs for arrays2022-10-06T14:57:24Zmantis-gitlab-migrationValue analysis generates incorrect Imperative outputs for arraysID0002030:
**This issue was created automatically from Mantis Issue 2030. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002030:
**This issue was created automatically from Mantis Issue 2030. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002030 | Frama-C | Plug-in > Eva | public | 2014-12-12 | 2015-01-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In case, the size of an array is not known, value analysis generated array[0..1] as Imperative outputs of a function updating array.
### Additional Information :
In above example I tried adding some bound on variable count using requires clause as below:
/*@
requires 0 < count < 8;
*/
void copy(int* src, int* dest, int count) {
for(int i=0; i<count; i++) {
dest[i] = src[i];
}
}
Even then imperative output of function copy generated was S_dest[0..1]
### Steps To Reproduce :
For example: Consider a file f.c has below copy function:
void copy(int* src, int* dest, int count) {
for(int i=0; i<count; i++) {
dest[i] = src[i];
}
}
Execute: frama-c -val -out-external -lib-entry -main copy f.c
Result: [inout] Out (external) for function copy:
S_dest[0..1]
S_dest[0..1] is not a over-estimation of location which can be modified by function copy.https://git.frama-c.com/pub/frama-c/-/issues/581Nested VLA are not supported2022-09-28T14:37:05ZPascal CuoqNested VLA are not supportedID0001718:
**This issue was created automatically from Mantis Issue 1718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001718:
**This issue was created automatically from Mantis Issue 1718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001718 | Frama-C | Kernel | public | 2014-03-25 | 2015-11-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Note that I have never seen this feature actually used, but it appears to be supported by GCC and Clang.
To reiterate, I have never seen code that does int t[a][a];
This report is only for the sake of completeness.
### Steps To Reproduce :
```
~/gitlab/frama-c $ bin/toplevel.opt -print t.c
[kernel] warning: cannot load plug-in `Aorai' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Obfuscator' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Report' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Security_slicing' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Wp' (incompatible with Neon-20140301+dev).
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:4:[kernel] user error: Length of array is not a constant: a
t.c:4:[kernel] warning: Variable-sized local variable t
[kernel] user error: skipping file "t.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
~/gitlab/frama-c $ cat t.c
int main(int c, char **v)
{
int a = 3;
int t[a][a];
t[a-1][a-1] = 1;
}
~/gitlab/frama-c $ gcc -pedantic -std=c99 t.c
~/gitlab/frama-c $
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/372It is impossble to change log file without kinds of message changing.2022-09-28T14:06:22Zmantis-gitlab-migrationIt is impossble to change log file without kinds of message changing.ID0002274:
**This issue was created automatically from Mantis Issue 2274. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002274:
**This issue was created automatically from Mantis Issue 2274. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002274 | Frama-C | Kernel | public | 2017-01-19 | 2017-01-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I wanted to explore how the analysis settings affect the output messages.
I changed settings and name of log file. But output messages were copied in the file that was pointed firstly.
Only if kinds of messages are changed a new file is created.
### Steps To Reproduce :
In GUI do follows:
1. Set -kernel-log rw:kernel.log
2. Run analysis
3. Verify that a file kernel.log was created.
4. Set -kernel-log rw:kernel2.log
5. Run analysis
6. Verify that a file kernel2.log was not created, but the time of last modification of the kernel.log was changed.
7. Set -kernel-log ruw:kernel2.log
8. Run analysis
9. Verify that a file kernel2.log was created.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/1828r24600: confusing error message when t[] is used where t* is expected2022-09-28T12:00:27ZPascal Cuoqr24600: confusing error message when t[] is used where t* is expectedID0001582:
**This issue was created automatically from Mantis Issue 1582. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001582:
**This issue was created automatically from Mantis Issue 1582. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001582 | Frama-C | Kernel > ACSL implementation | public | 2013-12-03 | 2013-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
TO REPRODUCE:
```
~ $ cat t.c
char t[5];
/*@ requires t <= p <= t+5; */
void f(char *p);
~ $ frama-c t.c
```
OBTAINED BEHAVIOR:
[kernel] warning: cannot load plug-in `Kitgen' (incompatible with Fluorine-20130601+dev).
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:3:[kernel] user error: comparison of incompatible types: char * and char * in annotation.
[kernel] user error: skipping file "t.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
EXPECTED BEHAVIOR:
comparison of incompatible types: char * and char[] in annotation.
DESCRIPTION:
I am fine with t <= p being rejected, since it is possible to write &t[0] which is a pointer to char in a stricter sense, or t+0 which is even shorter. However, the error message “ incompatible types: char * and char * ” is misleading.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2569Known WP limitations on statement contract2022-09-28T11:42:56ZAllan BlanchardKnown WP limitations on statement contractSince [Frama-C 23.0](https://git.frama-c.com/pub/frama-c/-/releases/23.0), statement contract are not supported anymore. Related issues are closed (as duplicates) and listed here.
- pub/frama-c#625
- pub/frama-c#1912
- pub/frama-c#511Since [Frama-C 23.0](https://git.frama-c.com/pub/frama-c/-/releases/23.0), statement contract are not supported anymore. Related issues are closed (as duplicates) and listed here.
- pub/frama-c#625
- pub/frama-c#1912
- pub/frama-c#511Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/318Duplicates are created on the tab "Messages"2022-09-28T11:26:37Zmantis-gitlab-migrationDuplicates are created on the tab "Messages"ID0002276:
**This issue was created automatically from Mantis Issue 2276. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002276:
**This issue was created automatically from Mantis Issue 2276. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002276 | Frama-C | Graphical User Interface | public | 2017-02-03 | 2017-11-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | maroneze | **Resolution** | reopened |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
New messages append to old messages on the tab "Messages" if an analysis are rerun with new options.
### Steps To Reproduce :
1. Run Value analysis.
2. Change any option.
3. Run Value analysis.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/427Path for 'make install-doc-code' for external plug-in2022-09-28T11:10:32Zmantis-gitlab-migrationPath for 'make install-doc-code' for external plug-inID0001278:
**This issue was created automatically from Mantis Issue 1278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001278:
**This issue was created automatically from Mantis Issue 1278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001278 | Frama-C | Kernel > Makefile | public | 2012-09-26 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I do `make install-doc-code` for my XXX plug-in, it installs the documentation in `/usr/local/share/frama-c/doc/XXX` instead of `/usr/local/share/frama-c/doc/code/XXX` like the other plug-ins. So the links to Frama-C documentation are broken.François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/429Namespace through packs - packing frama-c cmx into a cmxa2022-09-28T11:09:00Zmantis-gitlab-migrationNamespace through packs - packing frama-c cmx into a cmxaID0002163:
**This issue was created automatically from Mantis Issue 2163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002163:
**This issue was created automatically from Mantis Issue 2163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002163 | Frama-C | Kernel | public | 2015-09-16 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
It would be great if you could add an extra -for-pack FramaC to each byte/native code file compilation.
A way to do it, is to call the makefile with
FRAMAC_USER_FLAGS="-for-pack FramaC" make
But the Makefile.plugin has to be modified to name its pack FramaC.PLUGIN_NAME
This would enable the construction of a packed framaC.cmx and then a library framaC.cmxa.François BobotFrançois Bobot