frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-04-15T08:03:30Zhttps://git.frama-c.com/pub/frama-c/-/issues/425Creating a pointer to a local causes valid pointers above it to lose thier va...2021-04-15T08:03:30Zmantis-gitlab-migrationCreating a pointer to a local causes valid pointers above it to lose thier valid statusID0002234:
**This issue was created automatically from Mantis Issue 2234. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002234:
**This issue was created automatically from Mantis Issue 2234. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002234 | Frama-C | Plug-in > wp | public | 2016-06-21 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Pointers that are \valid lose their status as \valid if there is code below it that assigns to a pointer. This only seems to happen when the pointer in question is wrapped in a struct.
### Additional Information :
Tested on Aluminum on a Linux machine.
### Steps To Reproduce :
== file bug.c:
struct s {
int* ptr;
};
/*@
requires \valid(t.ptr);
@*/
void foo(struct s t) {
//@ assert \valid(t.ptr);
int a;
int* x = &a;
}
== Run command:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert : Unknown (51ms)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
== File fixed.c:
struct s {
int* ptr;
};
/*@
requires \valid(t.ptr);
@*/
void foo(struct s t) {
//@ assert \valid(t.ptr);
int a;
int* x; // = &a;
}
== Run command:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/424Add remark about additional axioms for read clauses2022-09-08T08:56:38ZJens GerlachAdd remark about additional axioms for read clausesID0001698:
**This issue was created automatically from Mantis Issue 1698. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001698:
**This issue was created automatically from Mantis Issue 1698. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001698 | Frama-C | Documentation > ACSL | public | 2014-03-14 | 2016-06-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
As long as WP does not generate foot prints for reads clauses of axiomatic declarations (see
https://bts.frama-c.com/view.php?id=1693), it might be helpful for users to understand, that it is their responsibility to formulate additional axioms/lemmas to express the foot print.
This could be added to Section 2.6.10 of
"ACSL Version 1.8 Implementation in Neon-20140301".https://git.frama-c.com/pub/frama-c/-/issues/423empty class instance as method argument leads to user error2021-02-22T14:01:31ZJochen Burghardtempty class instance as method argument leads to user errorID0001951:
**This issue was created automatically from Mantis Issue 1951. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001951:
**This issue was created automatically from Mantis Issue 1951. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001951 | Frama-Clang | Plug-in > Eva | public | 2014-11-03 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubunto-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
calling "frama-c -val 116.cpp" eventually leads to a user error:
[value] Done for function foo::Ctor
116.cpp:10:[value] user error: Function argument __fc_tmp_0 has unknown size. Aborting
[kernel] Plug-in value aborted: invalid user input.
The error message disappears if either
1) a variable (e.g. "int v;" after line 3) is declared inside class "foo",
2) the call "f.cat(f);" is omitted in line 10, or
3) the argument type of "cat" is changed to "int" in line 5 and "f" is replaced by "0" in line 10.
Apparently, the "f" in line 10 somehow causes an empty struct to be generated, which is not properly accepted.
## Attachments
- [116.cpp](/uploads/81a0fbdbba99b70ad2ddefa6b4bf3272/116.cpp)https://git.frama-c.com/pub/frama-c/-/issues/422suggest to suppress "Neither code nor specification" warning for __builtin_va...2021-02-22T13:37:15ZJochen Burghardtsuggest to suppress "Neither code nor specification" warning for __builtin_va_startID0001368:
**This issue was created automatically from Mantis Issue 1368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001368:
**This issue was created automatically from Mantis Issue 1368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001368 | Frama-C | Kernel | public | 2013-02-14 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
Running "frama-c -val ftest.c" on the attached program results in a "[kernel] warning: Neither code nor specification for function __builtin_va_start, generating default assigns from the prototype".
However,
(1) it is impossible to provide a fully general definition of that function;
(2) providing a special version adapted to our example results in a declaration-mismatch error, (which disappears when the name is changed to e.g. "__builtin_va_star2", so the name "__builtin_va_start" is in fact known to Frama-C).
I suggest to suppress the former warning "Neither code nor specification..." for __builtin_va_start(), and similar for va_end(), etc.
## Attachments
- [ftest.c](/uploads/e9165646a4e7b8fd718d1b64bea5964e/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/420Log message when plevel is used in logic needed2021-02-22T13:02:00ZPascal CuoqLog message when plevel is used in logic neededID0001674:
**This issue was created automatically from Mantis Issue 1674. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001674:
**This issue was created automatically from Mantis Issue 1674. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001674 | Frama-C | Plug-in > Eva | public | 2014-03-05 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Program:
extern int Frama_C_entropy_source;
/*@ requires \valid(p + (0 .. l-1));
assigns p[0 .. l-1] \from Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures \initialized(p + (0 .. l-1));
*/
void mu(char *p, unsigned l);
main(){
int a[48], b[53];
mu(&a, sizeof a);
mu(&b, sizeof b);
}
$ frama-c -val ~/t.c
Obtained result:
...
[value] computing for function mu <- main.
Called from /Users/pascal/t.c:12.
[value] using specification for function mu
/Users/pascal/t.c:3:[value] Function mu: precondition got status valid.
[value] Done for function mu
[value] computing for function mu <- main.
Called from /Users/pascal/t.c:13.
[value] Done for function mu
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
a[0..47] ∈ [--..--]
b[0..52] ∈ [--..--] or UNINITIALIZED
Wished result:
Warning: more than 200 locations to reduce. Approximating. See option -plevel.https://git.frama-c.com/pub/frama-c/-/issues/419No convenient way to specify shared library functions as assigns clauses2021-02-22T13:37:09ZPascal CuoqNo convenient way to specify shared library functions as assigns clausesID0001479:
**This issue was created automatically from Mantis Issue 1479. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001479:
**This issue was created automatically from Mantis Issue 1479. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001479 | Frama-C | Kernel > ACSL implementation | public | 2013-09-05 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | low | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Shared libraries functions store their entire state in a struct, in a pattern similar to that of the attached code.
It would be convenient to have a way to specify that while *ctx_p is computed \from *ctx_p, the pointer field(s) are used only by address and should not pollute the integer fields.
Currently:
$ ~/ppc/bin/toplevel.opt -val modular.c
…
[value] Values at end of function main:
ctx ? {{ garbled mix of &{ctx} (origin: Misaligned {modular.c:21}) }}
y ? {{ garbled mix of &{ctx} (origin: Misaligned {modular.c:21}) }}
## Attachments
- [modular.c](/uploads/d23c0d7f1d7d0eef2b867422055b0869/modular.c)https://git.frama-c.com/pub/frama-c/-/issues/418Cil does not reject incorrect initializers2021-02-22T13:37:05ZBoris YakobowskiCil does not reject incorrect initializersID0000936:
**This issue was created automatically from Mantis Issue 936. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000936:
**This issue was created automatically from Mantis Issue 936. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000936 | Frama-C | Kernel | public | 2011-08-24 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Cil should reject the initializers of the following program
int x = 1;
int y = x ^ 0;
int main () {
return y;
}
### Additional Information :
(Code such as
const int x = 1;
const int y = x ^ 0;
has seen been seen in the wild. An option that would force Cil to give a warning instead of an error in this case would be nice.)https://git.frama-c.com/pub/frama-c/-/issues/416Ocamlfind cannod be found2021-02-22T13:01:51Zmantis-gitlab-migrationOcamlfind cannod be foundID0002238:
**This issue was created automatically from Mantis Issue 2238. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002238:
**This issue was created automatically from Mantis Issue 2238. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002238 | Frama-C | Kernel | public | 2016-07-05 | 2016-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | alx | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux Fedora | **OS Version** | 24 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C crashes when run on a system without ocamlfind with Unexpected error.
### Additional Information :
I run frama-c precisely as
/usr/bin/frama-c -wp -wp-prop="-@assigns" -wp-model "Typed+cast" -wp-rte -wp-gen -wp-proof why3 -cpp-command="gcc -C -E -D_FRAMAC_ -I. -I./libc/" -wp-why-lib why-libs/MemoryAdd.why -wp-out checker_proofs envmap_base.c
[kernel] Current source was: :0
The full backtrace is:
Raised at file "pervasives.ml", line 30, characters 22-33
Called from file "findlib.ml", line 150, characters 10-151
Called from file "src/kernel_services/plugin_entry_points/dynamic.ml", line 292, characters 4-47
Called from file "src/kernel_services/plugin_entry_points/kernel.ml", line 598, characters 4-44
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 831, characters 2-22
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Failure("Config file not found - neither /etc/ocamlfind.conf nor the directory /etc/ocamlfind.conf.d")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Aluminium-20160501.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
### Steps To Reproduce :
1. Reinstall packet ocaml-findlib.x86_64 and delete directories
/etc/ocamlfind.conf
/etc/ocamlfind.conf.d"
2. Try to run frama-c on a filehttps://git.frama-c.com/pub/frama-c/-/issues/415Error in use of polyId in the 1.10 grammar2021-02-22T13:01:49ZDavid CokError in use of polyId in the 1.10 grammarID0002212:
**This issue was created automatically from Mantis Issue 2212. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002212:
**This issue was created automatically from Mantis Issue 2212. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002212 | Frama-C | Documentation > ACSL | public | 2016-02-25 | 2016-07-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | patrick | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The 1.10 ACSL grammar defines a poly-id as a combination of a simple id, optional label-binders and optional type-var-binders. This is correct for the many places that a poly-id is used as part of a declaration. However, poly-id is also used as a term - either as a standalone variable or as the function name in a function application. Here it is a **use** of the identifier, so the contents of the type list are type expressions (as in Fig. 2.12), not type variable binders. Similarly the labels are instances of labels (including label literals such as Here), and not binders. (The comment about binders also applies to the predicate application production in Fig. 2.2). Something like a poly-id-use is needed:
poly-id-use ::= id ( { label-use ( , label-use )* } )? ( < type-expr (, type-expr )* > )?
where
label-use ::= id | label-literal
label-literal ::= Here | Pre | ...https://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/413Implicit casting from integer to real causes failure in WP proof generation2021-04-15T06:54:30Zmantis-gitlab-migrationImplicit casting from integer to real causes failure in WP proof generationID0002241:
**This issue was created automatically from Mantis Issue 2241. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002241:
**This issue was created automatically from Mantis Issue 2241. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002241 | Frama-C | Plug-in > wp | public | 2016-07-29 | 2016-07-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL defines the integer type as a subset of the real type. Therefore, it states, implicit casting from integers to reals is allowed, because one is the subset of another. However, when this is done in practice, the WP plugin will generate goals that provers cannot parse, giving a type error.
### Additional Information :
This is confirmed to occur with the alt-ergo and why3 provers.
Tested on both Frama-C Sodium and Aluminum. Sodium produces slightly different errors than Aluminum, but both produce errors.
### Steps To Reproduce :
== Input file (bug.c):
/*@
axiomatic Bug {
logic integer ibug;
logic real rbug = ibug;
}
*/
/*@
requires i == rbug;
*/
void foo(int i);
void main() {
foo(42);
}
== Command to reproduce
frama-c -wp bug.c
== Output
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:13:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
/tmp/wp714796.dir/typed/A_Bug.ergo:7:[wp] user error: Alt-Ergo error:
characters 1-34:typing error: real and int cannot be unified
[wp] [Alt-Ergo] Goal typed_main_call_foo_pre : Failed
characters 1-34:typing error: real and int cannot be unified
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1)
## Attachments
- [bug.c](/uploads/24ea9349eeb21558e55d63d94453b416/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/412Incorrect location of warnings emitted by value analysis2021-02-22T13:57:59ZVirgile PrevostoIncorrect location of warnings emitted by value analysisID0000772:
**This issue was created automatically from Mantis Issue 772. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000772:
**This issue was created automatically from Mantis Issue 772. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000772 | Frama-C | Plug-in > Eva | public | 2011-03-30 | 2016-08-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | yakobowski | **Resolution** | won't fix |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the code below, frama-c -val -main f t.c will report an out of bound read on line 2. It should be line 3.
------------- t.c
void f (int* x) {
int a = 3 +
*x;
}
-----------------https://git.frama-c.com/pub/frama-c/-/issues/410Logic with read clauses can have their values invalidated by writes to separa...2021-08-05T09:15:39Zmantis-gitlab-migrationLogic with read clauses can have their values invalidated by writes to separated memory locationsID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002244 | Frama-C | Plug-in > wp | public | 2016-08-08 | 2016-08-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
In some cases, axiomatic logic using reads clauses can be true for a certain memory location, and then become unknown once an unrelated memory location is assigned to. You can even prove the memory locations as separate, but it does not fix the issue.
### Additional Information :
This bug is present on both Frama-C versions Sodium and Aluminum.
### Steps To Reproduce :
== File bug.c:
/*@
axiomatic Axiomatic {
logic boolean property_of_buffer(char *buffer) reads *buffer;
}
*/
/*@
assigns *buffer;
ensures property_of_buffer(buffer);
*/
void foo(char *buffer);
/*@
requires property_of_buffer(buffer);
assigns *buffer;
ensures property_of_buffer(buffer);
*/
int bar(char *buffer);
char buf1[1];
char buf2[1];
void main() {
foo(buf1);
bar(buf1);
foo(buf2);
bar(buf1);
}
== Command to run:
frama-c -wp bug.c
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_main_call_bar_pre : Valid
[wp] [alt-ergo] Goal typed_main_call_bar_pre_2 : Unknown (562ms)
[wp] Proved goals: 1 / 2
Qed: 1
alt-ergo: 0 (unknown: 1)
== Expected behavior: For typed_main_call_bar_pre_2 to prove valid.
## Attachments
- [bug.c](/uploads/40ef28c81962575b7520fa0642241586/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/409Nested scopes may cause issues with the validity of created pointers2021-04-15T08:57:59Zmantis-gitlab-migrationNested scopes may cause issues with the validity of created pointersID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002245 | Frama-C | Plug-in > wp | public | 2016-08-17 | 2016-08-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Upon entering a nested scope (caused by conditional blocks, or even just wrapping parts of code in {}), pointers once known as valid may become unknown in validity. This only seems to occur when more than 1 pointer is being reasoned about in the scope.
### Additional Information :
This bug occurs on both Sodium in Cygwin and Aluminum on Linux.
### Steps To Reproduce :
== Program bug.c:
/*@
ensures \valid(\result);
*/
int* foo();
void main() {
int* x = foo();
{
int y;
//@ assert \valid(x);
//@ assert \valid(&y);
}
}
== Command to run:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:6:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Unknown (51ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
== Expected output:
Both assertions to pass, since x is ensures to be valid, and the & operator always returns a valid pointer.
== Real output:
The pointer we ensure to be valid could not be proven to be valid.
Moving the definition of y to the outer scope fixes this issue, as well as moving the definition of x inside.
## Attachments
- [bug.c](/uploads/cfc99feea8974ba3cb5097bed4bfb3d3/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/408Frama-C does not support standard C digraphs2021-02-22T13:58:41ZDavid CokFrama-C does not support standard C digraphsID0002146:
**This issue was created automatically from Mantis Issue 2146. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002146:
**This issue was created automatically from Mantis Issue 2146. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002146 | Frama-C | Kernel | public | 2015-07-16 | 2016-08-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
Frama-C does not parse a program like
void func() <%
return;
%>
Presumably other standard digraphs and trigraphs are not supported as well.
## Attachments
- [clexer.mll.patch](/uploads/68eac5f1bf97603b7453d8f565aef75f/clexer.mll.patch)https://git.frama-c.com/pub/frama-c/-/issues/407Non working example in the documentation2021-02-22T13:37:00Zmantis-gitlab-migrationNon working example in the documentationID0001098:
**This issue was created automatically from Mantis Issue 1098. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001098:
**This issue was created automatically from Mantis Issue 1098. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001098 | Frama-C | Documentation | public | 2012-02-17 | 2016-08-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium |
### Description :
In logic_typing.ml the example to illustrate the definition of a new keyword is not typable.
The correct version is :
let foo_typer ~typing_context ~loc bhv ps =
match ps with
| p::[] ->
bhv.b_extended
<- ("FOO",42, [Logic_const.new_predicate (typing_context.type_predicate (typing_context.post_state [Normal]) p)]) ::bhv.b_extended
| _ -> typing_context.error loc "expecting a predicate after keyword FOO"
let () = register_behavior_extension "FOO" foo_typerhttps://git.frama-c.com/pub/frama-c/-/issues/405error in Coq file generation2021-04-15T08:59:05ZAlain Giorgettierror in Coq file generationID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002260 | Frama-C | Plug-in > wp | public | 2016-12-03 | 2016-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | giorgetti | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When an ACSL axiomatic in a C file main.c contains a type declaration, say
type t;
the command
frama-c .. -wp main.c -wp-prover coqide ..
generates a wrong line
Parameter fct : Type.
in the file typed_fct/A_coq_.v.
### Additional Information :
Noticed during a meeting with L. CorrensonLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/404Unterminated comment while generating division-by-zero assertion2021-02-22T13:01:31ZKostyantyn VorobyovUnterminated comment while generating division-by-zero assertionID0002250:
**This issue was created automatically from Mantis Issue 2250. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002250:
**This issue was created automatically from Mantis Issue 2250. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002250 | Frama-C | Kernel | public | 2016-10-13 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Gentoo | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | Frama-C 14-Silicon | **Fixed in Version** | - |
### Description :
For the following code snippet:
...
ret = dividend / *p;
...
RTE generates annotation:
/*@ assert rte: signed_overflow: dividend/*p ≤ 2147483647; */
The above leads to unterminated comment preprocessing error
### Steps To Reproduce :
frama-c -rte -then -print
of the following program:
int zero_division_006_gbl_divisor = 0;
void zero_division_006 () {
int dividend = 1000;
int *p;
int ret;
p = &zero_division_006_gbl_divisor;
ret = dividend / *p;
}
int main(int argc, const char **argv) {
zero_division_006();
return 0;
}
## Attachments
- [a.c](/uploads/fac19dff3e17847ea3277c0a8c3c3fbf/a.c)https://git.frama-c.com/pub/frama-c/-/issues/403workaround for coq-8.5.1 issue?2021-02-22T13:01:28ZJochen Burghardtworkaround for coq-8.5.1 issue?ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002233 | Frama-C | Plug-in > wp | public | 2016-06-16 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Aluminium-20160501 | **OS** | xubuntu16.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
We ran the command
frama-c-gui -cpp-extra-args='-I.' -pp-annot -no-unicode -wp -wp-rte -wp-script wp0.script -wp-model Typed+ref -wp-prop AdjacentDifferenceInverse -wp-coq-timeout 5 -wp-prover coq -wp-par 1 -wp-out adjacent_difference_inverse.wp adi.c
on the attached file "adi.c", using the attached Coq-script "wp0.script".
The goal isn't proven, and when manually starting the Coq Ide, it complains:
Error: The reference Q_UnchangedSection was not found in the current
environment.
However, the lemma "UnchangedSection" is present in lines 28-33 of file "adi.c", and a "Hypothesis Q_UnchangedSection" is present in lines 33-36 of the generated file "adjacent_difference_inverse.wp/typed_ref/Axiomatic.v", which is included in line 33 of file "adjacent_difference_inverse.wp/typed_ref/lemma_AdjacentDifferenceInverse_Coq.v" (i.e. of the file shown in the Coq Ide).
For these reasons, we believe that the behavior is a Coq-8.5.1 problem, not a Frama-c problem. Moreover, the same files cause no problems when Coq-8.5.1 is replaced by Coq-8.4.6.
Nevertheless, in an e-mail to Jens, Loic encouraged us to report the issue here, since Frama-C might provide a workaround for it.
## Attachments
- [adi.c](/uploads/c4c8150d300c94e05ae4078a54bb0388/adi.c)
- [wp0.script](/uploads/7a7bb805cc9c8332faccefd8ebe42e5d/wp0.script)
- [Axiomatic.v](/uploads/9ab08c5dc84284dc5f8412c7ddc95f09/Axiomatic.v)
- [lemma_AdjacentDifferenceInverse_Coq.v](/uploads/d61593407465c9df0f749dc04240e6ea/lemma_AdjacentDifferenceInverse_Coq.v)
- [adi.script](/uploads/9ab0f4bd54640d060c2292833e1bcd01/adi.script)https://git.frama-c.com/pub/frama-c/-/issues/402__attribute__((aligned(0))) tacitly causes sizeof computation to fail2021-02-22T13:37:02ZJochen Burghardt__attribute__((aligned(0))) tacitly causes sizeof computation to failID0002249:
**This issue was created automatically from Mantis Issue 2249. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002249:
**This issue was created automatically from Mantis Issue 2249. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002249 | Frama-C | Kernel | public | 2016-10-13 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | Aluminium-20160501 | **OS** | xbuntu 64bit | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c -val aaa.c" on the attached program issues the warnings:
[value] Computing initial state
aaa.c:6:[kernel] warning: division by zero. assert sizeof(struct _st) ≢ 0;
aaa.c:6:[value] Evaluation of initializer '(int)((unsigned int)1000 / sizeof(struct _st))' failed
[value] Initial state computed
When the "aligned(0)" attribute is omitted, the warning disappears. While it is acceptible that the Frama-C value analysis doesn't support all esoteric gcc contructs (like __attribute__), issueing a warning that "alignied(0)" isn't supported would help the user to understand the reasons for the warning.
## Attachments
- [aaa.c](/uploads/da286bc72aa9f2a0fbb3e13ad293ea02/aaa.c)
- [aaa2.c](/uploads/366b803f2d48dc409aec4d71a24cf3fb/aaa2.c)