pub issueshttps://git.frama-c.com/groups/pub/-/issues2021-02-22T14:01:36Zhttps://git.frama-c.com/pub/frama-c/-/issues/2427Better support of //@ style2021-02-22T14:01:36Zmantis-gitlab-migrationBetter support of //@ styleID0000079:
**This issue was created automatically from Mantis Issue 79. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000079:
**This issue was created automatically from Mantis Issue 79. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000079 | Frama-C | Kernel > ACSL implementation | public | 2009-05-11 | 2010-02-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Annotation consisting of several //@ lines should be supported. Eg, the following code produces a syntax error, whereas the /*@ ... */ style works:
//@ loop invariant a[0] == 1;
//@ loop invariant 1 <= i;
for(i=1; i<10; i++)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2459Frama-C fails to parse a file2022-12-28T10:05:19Zmantis-gitlab-migrationFrama-C fails to parse a fileID0000261:
**This issue was created automatically from Mantis Issue 261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000261:
**This issue was created automatically from Mantis Issue 261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000261 | Frama-C | Kernel | public | 2009-10-01 | 2009-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It compiles fine with "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -c -o dbutil.o"
But when given to Frama-C (CPP is set accordinly), I get the following error:
libtommath/tommath.h:77:[kernel] user error: GCC width mode TI applied to unexpected type, or unexpected mode
In tommath.h line 77 we have a mysterious GCC incantation (>_<):
typedef unsigned long mp_word __attribute__ ((mode(TI)));
### Additional Information :
Uploaded a preprocessed file: "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -C -E -o dbutil.i"
## Attachments
- [dbutil.i](/uploads/ca1ba34059bd1dd4efa823437f09a2c6/dbutil.i)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2428ghost integer ?2021-02-22T13:58:46ZSylvie Boldoghost integer ?ID0000387:
**This issue was created automatically from Mantis Issue 387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000387:
**This issue was created automatically from Mantis Issue 387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000387 | Frama-C | Kernel > ACSL implementation | public | 2010-02-01 | 2010-02-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hello,
It is impossible to have a ghost variable of type integer.
I may have an int32 ghost, but I would really prefer having an unbounded integer instead of an int32.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2347Parse error when using a wide string literal to initialize uint16 array2021-02-22T13:56:58Zmantis-gitlab-migrationParse error when using a wide string literal to initialize uint16 arrayID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000593 | Frama-C | Kernel | public | 2010-09-30 | 2010-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Maria | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm trying to analyze Brew with Frama-C. OS - windows XP.
I've created simple Brew project(see attach), preprocessed it with Visual Studio and after it try to analyze with Frama-C:
C:\Frama-C\bin>frama-c.exe "\Program Files\BREW 3.1.5\sdk\examples\helloworld"\*.i
Also, I've tried to add files to project, using user interface, but nothing happened.
## Attachments
- [helloworld.zip](/uploads/e1faf5861730eaa7d75da589b90c18c6/helloworld.zip)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2323no multiple assert-clauses accepted in /*@...*/-style comment2021-02-22T13:56:31ZJochen Burghardtno multiple assert-clauses accepted in /*@...*/-style commentID0000601:
**This issue was created automatically from Mantis Issue 601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000601:
**This issue was created automatically from Mantis Issue 601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000601 | Frama-C | Kernel > ACSL implementation | public | 2010-10-12 | 2010-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
See attached program: when #define multipleAsserts is in force, the kernel complains about line 11-12, containing two assert-clauses in a single /*@...*/ comment.
I'm not sure this contradicts some ASCL-syntax definition.
However, it appears strange to me, since multiple requires, ensures, and loop invariant are admitted (although they could be joined into a single one by &&, as for assert, too).
## Attachments
- [ftest.c](/uploads/92ec6efb44e5b83b7f0d4baf1022eecc/ftest.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2324Empty specification causes syntax error2021-02-22T13:56:32Zmantis-gitlab-migrationEmpty specification causes syntax errorID0000605:
**This issue was created automatically from Mantis Issue 605. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000605:
**This issue was created automatically from Mantis Issue 605. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000605 | Frama-C | Kernel > ACSL implementation | public | 2010-10-13 | 2010-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
File [1] causes error [2] when processed with frama-c -val. However, processing with frama-c -jessie causes no errors.
### Additional Information :
[1]
int* p;
int foo();
/*@
*/
int main() {
int i, t[10];
for(i=0; i<=10; i++)
t[i]=i;
if(foo()) p[2] = 1;
return 0;
}
[2]
[kernel] preprocessing with "gcc -C -E -I. val1.c"
val1.c:6:[kernel] user error: syntax error while parsing annotation
[kernel] user error: skipping file "val1.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2255Strange AST produced with unspecified side-effects involve function calls in ...2021-02-22T14:02:55ZPascal CuoqStrange AST produced with unspecified side-effects involve function calls in expressionsID0000676:
**This issue was created automatically from Mantis Issue 676. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000676:
**This issue was created automatically from Mantis Issue 676. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000676 | Frama-C | Kernel | public | 2011-01-18 | 2011-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Original code:
if(((fast_read(o, 3) ^ fetch) & 0xffffff) == 0 && o < src - MINOFFSET)
Transformed as:
ui32 tmp_1 ;
{ /*undefined sequence*/
tmp_1 = fast_read((void const *)o,(unsigned int )3);
;
}
if (((tmp_1 ^ fetch) & (unsigned int )0xffffff) == (unsigned int )0) {
if (o < src - 2) {
Contact Pascal for whole function.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2240Any number of ";" should be allowed in specifications2021-02-22T13:54:38Zmantis-gitlab-migrationAny number of ";" should be allowed in specificationsID0000713:
**This issue was created automatically from Mantis Issue 713. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000713:
**This issue was created automatically from Mantis Issue 713. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000713 | Frama-C | Kernel > ACSL implementation | public | 2011-02-10 | 2011-02-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The specification below produces a syntax error. As in C, any number of ";" should be allowed in specifications.
### Additional Information :
#define v(this) requires \valid(this);
/*@ v(this);
v(&this->a);
*/Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2237Command.command_generic may raise Sys_error2021-02-22T13:54:34ZJulien SignolesCommand.command_generic may raise Sys_errorID0000734:
**This issue was created automatically from Mantis Issue 734. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000734:
**This issue was created automatically from Mantis Issue 734. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000734 | Frama-C | Kernel | public | 2011-02-21 | 2011-02-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | unable to reproduce |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Since Command.command_generic uses Filename.open_temp_file, it may raise Sys_error (see caml bts #5228, http://caml.inria.fr/mantis/view.php?id=5228).
Either change the spec of impacted Command's functions, or change Command's implem. Or both.
See for instance how Extlib.temp_file_cleanup_at_exit solves this issue.
### Steps To Reproduce :
Don't know how to easily reproduce the issue, but I'm pretty sure it is possible :).Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1753Several [invariant] at a program point2021-02-22T14:03:41Zmantis-gitlab-migrationSeveral [invariant] at a program pointID0000750:
**This issue was created automatically from Mantis Issue 750. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000750:
**This issue was created automatically from Mantis Issue 750. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000750 | Frama-C | Kernel > ACSL implementation | public | 2011-03-08 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
If we want to put several [invariant] annotations at a program point, we have to have several ACSL comment, else we get :
[kernel] user error: Only one code annotation is allowed per comment
But with several comments, several program points are created, and it is then difficult to interpret the invariants, because it seems that they have to be considered as a sequence, while we want to see them as a conjunction...
Would it be possible to have several invariants at the same point like it is done for le [loop invariant] ?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2171Functional expression in assigns properties2021-02-22T13:52:48Zmantis-gitlab-migrationFunctional expression in assigns propertiesID0000980:
**This issue was created automatically from Mantis Issue 980. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000980:
**This issue was created automatically from Mantis Issue 980. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000980 | Frama-C | Kernel > ACSL implementation | public | 2011-10-06 | 2011-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
It would be great to be able to write :
assigns bound \from bound = \old (bound) + 1;
instead of :
ensures bound == \old (bound) + 1;
assigns bound;
as it is specified in ACSL documentation.
It would give much more lighter proof obligations in WP (see below).
### Additional Information :
When we call a function specified by :
assigns t[x].a, t[x].b, t[x].c;
ensures t[x].a = y;
we get :
forall v0, v1, v2.
let t1 = t0[x -> set_a (t0[x], v0) in
let t2 = t1[x -> set_b (t0[x], v1) in
let t3 = t2[x -> set_c (t0[x], v2) in
get_a (t3[x]) = y
=> P
and it is not easy (in more complex example) to find back the relation between v0 and y. It would be easier to process :
assigns t[x].a = y;
assigns t[x].b, t[x].c;
as :
let v0 = y in
forall v1, v2.
let t1 = t0[x -> set_a (t0[x], v0) in
let t2 = t1[x -> set_b (t0[x], v1) in
let t3 = t2[x -> set_c (t0[x], v2) in
=> PVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2098suggest to provide FILE,LINE references for proof obligations in WP cmd-line ...2021-08-05T13:14:10ZJochen Burghardtsuggest to provide FILE,LINE references for proof obligations in WP cmd-line outputID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001011 | Frama-C | Plug-in > wp | public | 2011-11-04 | 2011-11-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the command-line (i.e. non-gui) version of WP gives internally-generated names of proof obligations, like e.g.
[wp] [Simplify] Goal store_axiom_pop_of_push_pre31_push_stack_s1 : Valid
[wp] [Simplify] Goal store_axiom_pop_of_push_pre26_pop_stack_s2 : Timeout
In order to support the user in improving his program to get it verified, it should be made clear where an unproven obligation originated from, by providing file name and line number. Although a lot of information can be found in the directory specified with "-wp-out", the FILE,LINE information cannot.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1006Default @requires property for the [main] function2021-02-22T14:02:26Zmantis-gitlab-migrationDefault @requires property for the [main] functionID0001103:
**This issue was created automatically from Mantis Issue 1103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001103:
**This issue was created automatically from Mantis Issue 1103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001103 | Frama-C | Kernel | public | 2012-02-22 | 2014-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I think that it would be great to generate a default @requires property for the 'main' function, wouldn't it ?
### Additional Information :
The one from [tests/aorai/test_recursion1.c] for instance seems ok.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2045__builtin_alloca2021-02-22T13:49:38Zmantis-gitlab-migration__builtin_allocaID0001190:
**This issue was created automatically from Mantis Issue 1190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001190:
**This issue was created automatically from Mantis Issue 1190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001190 | Frama-C | Kernel | public | 2012-06-08 | 2012-06-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In a file with a local array which size in defined by a variable :
float a[n];
I get :
[kernel] warning: Variable-sized local variable a
which is ok. But then, when I use the value analysis, I get :
[kernel] warning: No code for function __builtin_alloca,
default assigns generated
because the declaration has been translated in :
__lengthofa = (unsigned int)n;
a = (float *)__builtin_alloca(sizeof(*a) * __lengthofa);
which looks fine, but the question is :
shouldn't the assigns property be defined somewhere inside Frama-C for the builtin functions ?
As a workaround, what prototype and assigns should I write for this function.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1926Code annotation in the middle of labels2021-03-29T13:52:50ZJulien SignolesCode annotation in the middle of labelsID0001327:
**This issue was created automatically from Mantis Issue 1327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001327:
**This issue was created automatically from Mantis Issue 1327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001327 | Frama-C | Kernel | public | 2012-12-12 | 2012-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider this code:
void foo(int x) {
switch (x) {
case 0: /*@ assert \true; */
case 1: ;
}
}
Frama-C encloses both the assertion and the "case 1: ;" into a block inside the "case 0" as shown below. I'm not sure that it is the expected behavior (either the block should also include "case 0" or this program should be rejected as syntactically incorrect).
$ frama-c -kernel-debug 1 a.i
<skip trace>
/* Generated by Frama-C */
void foo(int x)
{
/* */
/*sid:2*/
switch (x) {
/* */
case 0:
/*sid:3*/
/*block:begin*/
{
/* */
/*sid:4*/ /*@ assert \true; */ ;
case 1: /*sid:5*/ ; }
/*block:end*/
}
/*sid:8*/
return;
}
Note: if you add a semi-colon right after the assertion, there is no issue.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/290How to use the "Callers ..." context menu item2021-02-22T12:58:22Zmantis-gitlab-migrationHow to use the "Callers ..." context menu itemID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001431 | Frama-C | Graphical User Interface | public | 2013-05-27 | 2018-01-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Pardon the ignorance, but I couldn't find this on the manual...
I have a program where, after parsing, some warnings of this form are emitted:
"Calling undeclared function __builtin_swap32. Old style K&R code?"
I know there is a missing source file somewhere in my project, but I'd like to know who is calling these functions (since they are never directly called in my code). So I right-click on the function prototype on the GUI, and the last button in the context menu is "Callers ...". If I click on it, the "Launching analysis" window is displayed, with no indication of which analysis to choose.
I suppose the analysis I'd like is "Syntactic callgraph". So I choose it, without customizing any options, click Execute, but nothing changes. The "Callers ..." button is always visible when right-clicking the function declaration.
I noticed that if I choose the "Users" analysis, when right-clicking afterwards there is no more "Callers ..." button on the context menu, but I fail to see how any of the new options (e.g. Dependencies) could help me identify the function callers.
Is there a simpler way, other than by manually parsing the DOT file (the produced graph is too large for me to visually inspect it), to obtain information about function callers?Andre MaronezeAndre Maronezehttps://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/1829declaration of variable of type void accepted2021-02-22T13:43:27ZJochen Burghardtdeclaration of variable of type void acceptedID0001576:
**This issue was created automatically from Mantis Issue 1576. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001576:
**This issue was created automatically from Mantis Issue 1576. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001576 | Frama-C | Kernel | public | 2013-11-28 | 2013-11-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp void.c" on the attached program doesn't report any error message, although declaring i to have type void doesn't make sense.
Vice versa, when "i" is deleted, or when "void i" is deleted, the kernel complains about a syntax error. Therefore, the only possibility to implement a logical constant is to declare "void i" as its parameter.
## Attachments
- [void.c](/uploads/b7fe0ef623a3ec56691e659d1b8d3673/void.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1827suggest to insert implicit cast of logic function's expression to return type2021-02-22T13:43:26ZJochen Burghardtsuggest to insert implicit cast of logic function's expression to return typeID0001577:
**This issue was created automatically from Mantis Issue 1577. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001577:
**This issue was created automatically from Mantis Issue 1577. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001577 | Frama-C | Kernel | public | 2013-11-28 | 2013-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The body expression "(i + 1)" of the Acsl logic function "mySuccA" could by tacitly casted to "mySuccA"'s return type, viz. "char". This would be similar to the treatment in C code (function "mySuccC").
Currently, Frama-C reports a user typing error for the former, but not for the latter.
Probably, this is not proper bug but compatible with the Acsl description. I just wanted to suggest to think about adapting the Ascl semantics here to the C semantics, which is more convenient for the user.
## Attachments
- [char.c](/uploads/200e02a207b925bf782474a662e90b4b/char.c)Virgile PrevostoVirgile Prevostohttps://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 Prevosto