frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:37:55Z
https://git.frama-c.com/pub/frama-c/-/issues/489
alt-ergo: undefined symbol andb
2021-02-22T13:37:55Z
mantis-gitlab-migration
alt-ergo: undefined symbol andb
ID0002159:
**This issue was created automatically from Mantis Issue 2159. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002159:
**This issue was created automatically from Mantis Issue 2159. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002159 | Frama-C | Plug-in > wp | public | 2015-09-14 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | azaostro | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | 64 bit | **OS** | Ubuntu | **OS Version** | 14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
WP fails to handle my recursive boolean function, defined as "full_rec":
/*@ logic integer size_rec{L}(int* busybits, integer capa) =
@ (capa == 0) ? 0 :
@ (busybits[capa-1] != 0) ? 1 + size_rec(busybits, capa - 1) : 0;
@
@ logic boolean full_rec{L}(int *busybits, integer capa) =
@ (capa == 0) ? \true :
@ (busybits[capa-1] != 0) ? full_rec(busybits, capa - 1) : \false;
@
@ lemma full_rec_size_rec: \forall int* busybits, integer capa;
@ size_rec(busybits, capa) == capa <==> full_rec(busybits, capa);
*/
The result:
$ frama-c -wp repr.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing repr.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
/tmp/wpfaa705.dir/typed/lemma_full_rec_size_rec.ergo:13:[wp] user error: Alt-Ergo error:
characters 5-94:typing error: undefined symbol andb
[wp] [Alt-Ergo] Goal typed_lemma_full_rec_size_rec : Failed
Error: characters 5-94:typing error: undefined symbol andb
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1)
### Steps To Reproduce :
run
frama-c -wp repr.c
on the attached file repr.c
## Attachments
- [repr.c](/uploads/78cf3015b33886cf55680addd2e02316/repr.c)
https://git.frama-c.com/pub/frama-c/-/issues/2134
alt-ergo version managment
2021-02-22T14:04:18Z
mantis-gitlab-migration
alt-ergo version managment
ID0000641:
**This issue was created automatically from Mantis Issue 641. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000641:
**This issue was created automatically from Mantis Issue 641. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000641 | Frama-C | Plug-in > wp | public | 2010-12-16 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dargaye | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Nitrogen-20111001 | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
When the alt-ergo version is 0.91.x and the -wp-no-arrays option isn't set,
find a way to catch the alt-ergo error output
https://git.frama-c.com/pub/frama-c/-/issues/159
Ambiguous path error using why3
2021-02-22T12:55:18Z
mantis-gitlab-migration
Ambiguous path error using why3
ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002454 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
### Steps To Reproduce :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
## Attachments
- [example.c](/uploads/ba254a88318716a5e0665ff9fe46d1f4/example.c)
https://git.frama-c.com/pub/frama-c/-/issues/2249
An erorr appears when executing right-click on the source-file name(left side...
2021-02-22T14:03:36Z
mantis-gitlab-migration
An erorr appears when executing right-click on the source-file name(left side of the screen).
ID0000508:
**This issue was created automatically from Mantis Issue 508. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000508:
**This issue was created automatically from Mantis Issue 508. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000508 | Frama-C | Graphical User Interface | public | 2010-06-14 | 2011-01-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | adytzul_ac | **Assigned To** | signoles | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | random |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The full backtrace is:
Raised at file "src/pdg_types/pdgTypes.ml", line 548, characters 22-25
Called from file "src/pdg_types/pdgTypes.ml", line 554, characters 32-48
Called from file "src/security_slicing/components.ml", line 393, characters 2-80
Called from file "list.ml", line 74, characters 24-34
Called from file "list.ml", line 74, characters 24-34
Called from file "src/security_slicing/components.ml", line 601, characters 22-53
Called from file "src/security_slicing/components.ml", line 676, characters 14-69
Called from file "src/lib/type.ml", line 746, characters 40-45
Called from file "src/kernel/journal.ml", line 323, characters 15-26
Re-raised at file "src/kernel/journal.ml", line 338, characters 14-15
Called from file "src/impact/register_gui.ml", line 117, characters 15-37
Called from file "src/lib/extlib.ml", line 176, characters 12-15
Re-raised at file "src/lib/extlib.ml", line 181, characters 10-11
Called from file "src/gui/gtk_helper.ml", line 533, characters 8-385
Unexpected error (PdgTypes.Pdg.Top).
Please report as 'crash' at http://bts.frama-c.com
## Attachments
- [main.c](/uploads/cfcb446045cce03adbefbcea7c5c3715/main.c)
- ![error_2](/uploads/0df923cdc34eef798552c3264fdfa575/error_2.JPG)
https://git.frama-c.com/pub/frama-c/-/issues/2488
An extra ')' is missing in the Printexc.record_backtrace patch on the Frama-C...
2021-02-22T13:59:57Z
mantis-gitlab-migration
An extra ')' is missing in the Printexc.record_backtrace patch on the Frama-C wiki
ID0000181:
**This issue was created automatically from Mantis Issue 181. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000181:
**This issue was created automatically from Mantis Issue 181. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000181 | Frama-C | Kernel | public | 2009-07-13 | 2009-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
http://bts.frama-c.com/view.php?id=169 is fixed by a patch posted on the Frama-C wiki (http://bts.frama-c.com/dokuwiki/lib/exe/fetch.php?media=wiki:frama-c-beryllium-20090601-beta1.patch)
However, I think near the end an extra ')' is missing:
- (Printexc.to_string e)
- (if Parameters.Debug.get () > 0 then Printexc.get_backtrace ()
- else ""));
+ (Printexc.to_string e);
It should be:
+ (Printexc.to_string e));
https://git.frama-c.com/pub/frama-c/-/issues/2365
Annotations analysis does not find preprocessor macro
2021-04-15T09:17:19Z
mantis-gitlab-migration
Annotations analysis does not find preprocessor macro
ID0000486:
**This issue was created automatically from Mantis Issue 486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000486:
**This issue was created automatically from Mantis Issue 486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000486 | Frama-C | Plug-in > jessie | public | 2010-05-18 | 2010-05-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following is correct c-code, but is doesn't verify.
#define BUFF_SIZE 4
/*@ requires \valid(msg+(0..BUFF_SIZE));
ensures msg[BUFF_SIZE] == '\0';
*/
int setFoo(char* msg) {
msg[BUFF_SIZE] = '\0';
return 0;
}
~/progs/C/frama-c/test$ frama-c -jessie -pp-annot t.c
[kernel] preprocessing with "gcc -C -E -I. -dD t.c"
t.c:3:[kernel] user error: Error during annotations analysis: unbound logic variable BUFF_SIZE
[kernel] user error: skipping file "t.c" that has errors.
[kernel] Plugin kernel aborted because of invalid user input(s).
A work-around is to add a space between .. and BUFF_SIZE.
https://git.frama-c.com/pub/frama-c/-/issues/401
Annotation wrongly displayed as checked (green bullet) whereas it is false, w...
2021-02-22T13:01:21Z
mantis-gitlab-migration
Annotation wrongly displayed as checked (green bullet) whereas it is false, when using the option -rte on command line.
ID0002258:
**This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002258:
**This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002258 | Frama-C | Plug-in > RTE | public | 2016-11-24 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | julien-cohen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | PC | **OS** | Linux Ubuntu | **OS Version** | 16.04 LTS |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have a program with an incorrect acces outside an array. When lauching frama-c-gui with no options and value analysis, the out-of-bounds access is detected and the corresponding annotation is displayed with an orange bullet. When using the -rte option, two annotations are displayed (for the lower and upper bound of the array), and a green bullet is displayed for both (which is not correct).
/*@ assert rte: index_bound: 0 ≤ cpt; */
/*@ assert rte: index_bound: cpt < 5; */
The console says :
tableau_erreur.c:11:[value] Assertion 'rte,index_bound' got status valid.
### Additional Information :
Posted on http://stackoverflow.com/questions/40763614/unsound-behavior-with-rte-option-in-magnesium/40766174#40766174 .
There are two screen captures there. Someone (anol) replied and gave additional information (see the post).
### Steps To Reproduce :
Here is my program :
int main(){
int t[5] = {1,2,3,4,5};
int cpt =0 ;
int tmp ;
while (cpt<10){
tmp = getchar() ;
if ( t[cpt] > tmp )
{ return 1 ; }
cpt++ ;
}
return 10 ;
}
The problem occurs when launching frama-c-gui -rte and the calue analysis on this program.
https://git.frama-c.com/pub/frama-c/-/issues/2629
Anomalous behavior of anonymous 'behavior'
2022-09-22T08:58:47Z
David Cok
Anomalous behavior of anonymous 'behavior'
### Steps to reproduce the issue
See this code:
```
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
...
### Steps to reproduce the issue
See this code:
```
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
/*@
requires P != 0;
assigns Q;
ensures Q == 1;
*/
void d() {
Q = 1;
}
//@ assigns Q;
void c() {
d();
}
```
which is an minimal as I could make it.
Note that a calls b, where b has a always-true behavior. c calls d the same way, but without a behavior.
The example is extracted from a larger specification with lots of behaviors.
### Actual behaviour
In my environment, the above, run with `frama-c -wp` produces
```
fc $ frama-c -wp behavior.c
[kernel] Parsing behavior.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_exit : Timeout (Qed:0.81ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_call_b_requires : Timeout (Qed:0.78ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_normal : Timeout (Qed:0.77ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_c_call_d_requires : Timeout (10s)
[wp] Proved goals: 7 / 11
Qed: 7
Alt-Ergo 2.4.1: 0 (interrupted: 4)
```
That is c calling d is fine. a calling b is not.
### Expected behaviour
I expect a calling be to behave precisely like c calling d.
It appears that even with a prefix consisting of just requires clauses, WP produces an
anonymous behavior that contains something like `assigns \everything`. That then causes
the very mysterious assigns errors that you see above.
Fortunately, now that I know the problem there is an easy workaround -- but prior to that it wasted many days of time.
### Contextual information
Frama-C 25.0, built from source, with WP
MacOS 12.5
Loïc Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/1234
aorai causes failed assertion
2021-02-22T13:31:22Z
Jochen Burghardt
aorai causes failed assertion
ID0001289:
**This issue was created automatically from Mantis Issue 1289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001289:
**This issue was created automatically from Mantis Issue 1289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001289 | Frama-C | Plug-in > aoraï | public | 2012-10-25 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Running "frama-c ftest.c -aorai-automata ftest.ya" on the attached program causes an unexpectyed error in file cil_datatype.ml; see attached stdout log.
## Attachments
- [ftest.c](/uploads/00b0a24a7ad13eb171b46cdba01964c0/ftest.c)
- [ftest.ya](/uploads/9991a7f542c1b39583bf6d5770b4d0ba/ftest.ya)
- [log.txt](/uploads/79e5a6ac1f6b4465b46a3c7b5078777e/log.txt)
https://git.frama-c.com/pub/frama-c/-/issues/1459
aorai doesn't enrich user's "loop assigns" by generated internal variables
2021-02-22T13:32:04Z
Jochen Burghardt
aorai doesn't enrich user's "loop assigns" by generated internal variables
ID0001290:
**This issue was created automatically from Mantis Issue 1290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001290:
**This issue was created automatically from Mantis Issue 1290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001290 | Frama-C | Plug-in > aoraï | public | 2012-10-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Running "frama-c ftest.c -aorai-automata ftest.ya" on the attached files yields an annotated file "ftest_annot.c" (also attached) with a wrong "loop assigns" clause. In line 74, the user-given clause (from line 3 of "ftest.c") is just copied, while the assignment to the generated variable "aorai_Loop_Init_11" in line 78 should lead to the inclusion of that variable into the loop assigns clause.
## Attachments
- [ftest.c](/uploads/e061f517c65a28c92295edf2270d49d6/ftest.c)
- [ftest.ya](/uploads/7fa374911c510084fa3fcc4a34fb8014/ftest.ya)
- [ftest_annot.c](/uploads/09d9e9ac64e03729657111706a042bd4/ftest_annot.c)
https://git.frama-c.com/pub/frama-c/-/issues/980
A pointer can be reported as belonging to an adjacent memory blocks in the bi...
2021-02-22T13:16:29Z
Arvid Jakobsson
A pointer can be reported as belonging to an adjacent memory blocks in the bittree memory model
ID0001836:
**This issue was created automatically from Mantis Issue 1836. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001836:
**This issue was created automatically from Mantis Issue 1836. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001836 | Frama-C | Plug-in > E-ACSL | public | 2014-07-16 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
There is a one-off error in the calculation of to which block a pointer. The following series of calls to the memory model triggers it (but I've got no simple program example which reproduces the error).
struct _block bk1 = {.ptr = 1, .size = 1};
__add_element(&bk1);
assert(__get_cont((void*)0) == NULL);
assert(__get_cont((void*)1) == &bk2);
assert(__get_cont((void*)2) == NULL); // will report 2 as belonging to bk1.
The offending line in e_acsl_bittree.c is:
else if((size_t)ptr <= tmp->leaf->size + tmp->addr)
where the comparison is strict and another clause should be added to handle the case of empty structs.
https://git.frama-c.com/pub/frama-c/-/issues/368
applicability of Coq proof script depends on order of include files
2021-04-15T08:02:31Z
Jochen Burghardt
applicability of Coq proof script depends on order of include files
ID0002282:
**This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002282:
**This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002282 | Frama-C | Plug-in > wp | public | 2017-02-16 | 2017-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
We run "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prop HeapMaximum -wp-prover coq make_heap_cpp.c" on the attached files. In the current form, the Coq proof script "wp0.script" works fine and proved the lemma "HeapMaximum" from file "make_heap_cpp.c".
However, when that lemma is moved after the "axiomatic Count", which is completely unrelated, the same command doesn't work any longer. Using "-wp-out" shows that both versions differ in the location where lemma "HeapBounds" is available in Coq; this make it necessary to change the names used in the proof.
The problem originated from lemma "HeapMaximum" being used for the verification of two different function contracts. For software engineering reasons, the order of #include files was different (since different files were preferred to be included in the ".c", rather than already in the ".h" file). This resulted in "lemma HeapMaximum" appearing before and after an "axiomatic", making "wp0.script" work and not work, respectively.
## Attachments
- [make_heap_cpp.c](/uploads/256c2042ed0e2b08fc7901c42cdcbb49/make_heap_cpp.c)
- [wp0.script](/uploads/7277fc9a7ed0386527de3694d96817e5/wp0.script)
Loïc Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/2517
A pure predicate in an axiomatic with some "unpure" axioms have some strange ...
2021-04-15T09:17:42Z
François Bobot
A pure predicate in an axiomatic with some "unpure" axioms have some strange results
ID0000073:
**This issue was created automatically from Mantis Issue 73. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000073:
**This issue was created automatically from Mantis Issue 73. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000073 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
A pure predicate in an axiomatic with some "unpure" axioms have some strange results. In this case an assertion failed :
myc.c
============================
/*@
axiomatic myaxioms{
predicate myrelation(int p,int q);
logic int mylogic{L}(int * p);
axiom myaxiom{L} :
\forall int * p, q; \at(myrelation(mylogic(p),q),L);
}
@*/
frama-c -jessie-analysis unwanted_label.c.assertion_failed.c :
=========================
Calling Jessie tool in subdir unwanted_label.c.assertion_failed.jessie
File "jc/jc_typing.ml", line 2687, characters 20-20:
Uncaught exception: File "jc/jc_typing.ml", line 2687, characters 20-26: Assertion failed
===========================
### Additional Information :
frama-c : 5186
https://git.frama-c.com/pub/frama-c/-/issues/2565
Arch Linux package uninstallable due to dependency that no longer exists
2021-10-06T07:53:07Z
Olivier Nicole
Arch Linux package uninstallable due to dependency that no longer exists
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [ ] you insta...
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Arch Linux User Repository package
- Frama-C version: 21.1-1
- Plug-in used: N/A
- OS name: Arch Linux
- OS version: N/A
The Arch Linux User Repository package `frama-c` depends on gtksourceview2 which seems to no longer exist in the repositories, preventing the installation.
# Fix ideas
I'm not sure which would be simpler between upgrading to a newer version of gtksourceview or making that dependency available again.
https://git.frama-c.com/pub/frama-c/-/issues/1413
Arguments are not checked when function call precedes function declaration
2021-02-22T14:03:07Z
Virgile Prevosto
Arguments are not checked when function call precedes function declaration
ID0000728:
**This issue was created automatically from Mantis Issue 728. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000728:
**This issue was created automatically from Mantis Issue 728. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000728 | Frama-C | Kernel | public | 2011-02-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Cil allows a function to be called before being defined but does not check that the number/types of argument correspond. See for instance
tests/misc/call_variadic.i, which fails with frama-c -check, while the error should be reported directly when type-checking.
https://git.frama-c.com/pub/frama-c/-/issues/2434
Arithmetic safety of bitwise operators cannot be verified
2021-04-15T09:17:29Z
mantis-gitlab-migration
Arithmetic safety of bitwise operators cannot be verified
ID0000348:
**This issue was created automatically from Mantis Issue 348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000348:
**This issue was created automatically from Mantis Issue 348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000348 | Frama-C | Plug-in > jessie | public | 2009-12-03 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie cannot verify arithmetic safety in the following code:
typedef unsigned int uint32;
uint32 b1(uint32 x, uint32 y)
{
return x^y;
}
uint32 b2(uint32 x, uint32 y)
{
return x&y;
}
uint32 b3(uint32 x, uint32 y)
{
return x|y;
}
uint32 b4(uint32 x)
{
return ~x;
}
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2193
array access in "decreases"-clause causes "Unexpected internal region in logic"
2021-04-15T09:17:05Z
Jochen Burghardt
array access in "decreases"-clause causes "Unexpected internal region in logic"
ID0000846:
**This issue was created automatically from Mantis Issue 846. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000846:
**This issue was created automatically from Mantis Issue 846. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000846 | Frama-C | Plug-in > jessie | public | 2011-05-30 | 2011-05-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie reports an uncaught exception: Failure("Unexpected internal region in logic") on the attached file. That message vanishes if either
- the array access "b[f]" in line 4 is replaced e.g. by "0",
- the "decreases" clause in line 8 is deleted, or
- the recursive call in line 11 is deleted.
(The code is nonsensical, but has been boiled down from a reasonable program.)
## Attachments
- [ftest.c](/uploads/9f30f7973db62f3510ab1bdb277ee75a/ftest.c)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2262
array id "shift"
2021-04-15T09:17:10Z
mantis-gitlab-migration
array id "shift"
ID0000651:
**This issue was created automatically from Mantis Issue 651. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000651:
**This issue was created automatically from Mantis Issue 651. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000651 | Frama-C | Plug-in > jessie | public | 2010-12-24 | 2010-12-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
void
alg( void )
{
long shift[255];
/*@
@ loop invariant 0 <= i <= 255;
@ loop variant 255 - i;
@ loop invariant \forall integer k; 0 <= k < i ==>
@ shift[k] == -1;
@*/
for ( unsigned i = 0; i < 255; ++i )
shift[i] = -1;
}
tester@ubuntu-fm:~/workspace/test5$ frama-c -jessie -jessie-atp gui alg1.c
[kernel] preprocessing with "gcc -C -E -I. -dD alg1.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir alg1.jessie
[jessie] File alg1.jessie/alg1.jc written.
[jessie] File alg1.jessie/alg1.cloc written.
[jessie] Calling Jessie tool in subdir alg1.jessie
Generating Why function alg
[jessie] Calling VCs generator.
gwhy-bin [...] why/alg1.why
Computation of VCs...
decomp_fun_type=long_P pointer ref
File "why/alg1.why", line 452, characters 36-73:
This term cannot be applied (either it is not a function
or it is applied to non pure arguments)
make: *** [alg1.stat] Error 1
[jessie] user error: Jessie subprocess failed: make -f alg1.makefile gui
## Attachments
- [alg.c](/uploads/f5506542a8fc69c2920511269e592335/alg.c)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2460
array range in requires predicate
2021-04-15T09:17:36Z
mantis-gitlab-migration
array range in requires predicate
ID0000256:
**This issue was created automatically from Mantis Issue 256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000256:
**This issue was created automatically from Mantis Issue 256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000256 | Frama-C | Plug-in > jessie | public | 2009-09-25 | 2009-09-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jcrown | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -main foo file.c -jessie
on code
typedef struct { int a; } A;
typedef struct { A * c[10]; } B;
typedef struct { B * c[10]; } C;
C v;
/*@.......*/
void foo(void);
wth one of the 3 contracts below on foo()
/*@ requires \valid((v.c[0 .. 9])->c[0 .. 9]); */
/*@ requires \valid((v.c[0 .. 9])->c+(0 .. 9)); */
/*@ requires \valid((v.c+(0 .. 9))->c+(0 .. 9)); */
->
Uncaught exception: File "jc/jc_interp.ml", line 939, characters 25-31: Assertion failed
on the 1st and 2nd ones,
and
file.c:8:[kernel] user error: Error during annotations analysis: expected a struct with field c
on the 3rd one.
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/963
array-type parameter causes "Old style K&R" kernel warning with cxx plugin
2021-02-22T13:27:57Z
Jochen Burghardt
array-type parameter causes "Old style K&R" kernel warning with cxx plugin
ID0001814:
**This issue was created automatically from Mantis Issue 1814. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001814:
**This issue was created automatically from Mantis Issue 1814. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001814 | Frama-Clang | Plug-in > clang | public | 2014-06-20 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
taint02.cpp:7:[kernel] warning: Calling undeclared function _Z3fooPi. Old style K&R code?
The warning disappears if the file is renamed to "taint02.c".
## Attachments
- [taint02.cpp](/uploads/0071ae679c085de2390e5212762dc45d/taint02.cpp)