frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:55:13Zhttps://git.frama-c.com/pub/frama-c/-/issues/155External provers broken with 19.0-beta12021-02-22T12:55:13Zmantis-gitlab-migrationExternal provers broken with 19.0-beta1ID0002437:
**This issue was created automatically from Mantis Issue 2437. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002437:
**This issue was created automatically from Mantis Issue 2437. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002437 | Frama-C | Kernel | public | 2019-05-20 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bpc | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 GNU/Linux | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
External provers, with why3, look broken with 19.0-beta1 :
$ frama-c -wp -wp-prover why3:z3 swap.c
[kernel] Parsing swap.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [z3] Goal typed_swap_ensures_A : Unknown (Qed:3ms) (51ms)
[wp] Proved goals: 3 / 4
Qed: 3 (0.38ms-0.63ms-0.77ms)
Z3: 0 (unknown: 1)
Same problem using why3:cvc4-15 and why3:alt-ergo.
With the "native" alt-ergo, no problem :
$ frama-c -wp -wp-prover alt-ergo swap.c
[kernel] Parsing swap.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] Proved goals: 4 / 4
Qed: 3 (0.60ms-1ms-3ms)
Alt-Ergo: 1 (11ms) (40)
### Additional Information :
$ opam list
# Packages matching: installed
# Name # Installed # Synopsis
alt-ergo 2.3.0 The Alt-Ergo SMT prover
alt-ergo-lib 2.3.0 The Alt-Ergo SMT prover library
alt-ergo-parsers 2.3.0 The Alt-Ergo SMT prover parser library
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
biniou 1.2.0 Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve
camlp5 7.06.10-g84ce6cc4 Preprocessor-pretty-printer of OCaml
camlzip 1.07 Provides easy access to compressed files in ZIP, GZIP and JAR format
conf-autoconf 0.1 Virtual package relying on autoconf installation
conf-gmp 1 Virtual package relying on a GMP lib system installation
conf-gnomecanvas 2 Virtual package relying on a Gnomecanvas system installation
conf-graphviz 0.1 Virtual package relying on graphviz installation
conf-gtksourceview 2 Virtual package relying on a GtkSourceView system installation
conf-m4 1 Virtual package relying on m4
conf-perl 1 Virtual package relying on perl
conf-pkg-config 1.1 Virtual package relying on pkg-config installation
conf-python-2-7 1.0 Virtual package relying on Python-2.7 installation
conf-which 1 Virtual package relying on which
coq 8.9.0 Formal proof management system
cppo 1.6.5 Equivalent of the C preprocessor for OCaml programs
dune 1.9.3 Fast, portable and opinionated build system
easy-format 1.3.1 High-level and functional interface to the Format module of the OCaml standard library
frama-c 19.0.beta1 pinned to version 19.0.beta1 at git+https://github.com/Frama-C/Frama-C-snapshot.git#latest
jbuilder transition This is a transition package, jbuilder is now named dune. Use the dune
lablgtk 2.18.8 OCaml interface to GTK+
menhir 20181113 An LR(1) parser generator
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-config 1 OCaml Switch Configuration
ocaml-system 4.05.0 The OCaml compiler (system version, from outside of opam)
ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
ocamlfind 1.8.0 A library manager for OCaml
ocamlgraph 1.8.8 A generic graph library for OCaml
ocplib-simplex 0.4 A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities and optimizing linear objective functions
psmt2-frontend 0.2 A library to parse and type-check a conservative extension of the SMT-LIB 2 standard with prenex polymorphism
seq 0.1 Compatibility package for OCaml's standard iterator type starting from 4.07.
why3 1.2.0 Why3 environment for deductive program verification
yojson 1.7.0 Yojson is an optimized parsing and printing library for the JSON format
z3 4.8.4 Z3 solver
zarith 1.7 Implements arithmetic and logical operations over arbitrary-precision integers
## Attachments
- [swap.c](/uploads/cdbec3e4e4a47f15ad17c1c3703832b9/swap.c)
- [tst.c](/uploads/d3498f1224a689c944bb6c4ef8857c30/tst.c)https://git.frama-c.com/pub/frama-c/-/issues/157configure does not detect gtksourceview due to wrong path2022-09-28T11:03:51Zmantis-gitlab-migrationconfigure does not detect gtksourceview due to wrong pathID0002457:
**This issue was created automatically from Mantis Issue 2457. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002457:
**This issue was created automatically from Mantis Issue 2457. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002457 | Frama-C | Kernel > configure | public | 2019-06-20 | 2019-06-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | 6.5 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is on 19.0-beta2.
due to looking in the wrong directory, gtksourceview is not found.
Diff can be found in `Additional Information`
### Additional Information :
Index: configure.in
--- configure.in.orig
+++ configure.in
@@ -975,8 +975,8 @@ else
fi
configure_library([GTKSOURCEVIEW],
- [$SOURCEVIEW_PATH/lablgtksourceview2.$LIB_SUFFIX,
- $SOURCEVIEW_PATH/lablgtk3_sourceview3.$LIB_SUFFIX],
+ [$LABLGTKPATH_FOR_CONFIGURE/lablgtksourceview2.$LIB_SUFFIX,
+ $LABLGTKPATH_FOR_CONFIGURE/lablgtk3_sourceview3.$LIB_SUFFIX],
[lablgtksourceview not found],
no)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/158build failure due to mangled variable assignment in Makefile2022-09-28T11:02:51Zmantis-gitlab-migrationbuild failure due to mangled variable assignment in MakefileID0002458:
**This issue was created automatically from Mantis Issue 2458. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002458:
**This issue was created automatically from Mantis Issue 2458. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002458 | Frama-C | Kernel > configure | public | 2019-06-20 | 2019-06-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | 6.5-current |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
here's the patch:
Index: Makefile.generating
--- Makefile.generating.orig
+++ Makefile.generating
@@ -153,8 +153,8 @@ endif
ifeq ($(HAS_OCAML408),yes)
DYNLINK_INIT=fun () -> ()
FORMAT_STAG=stag
- FORMAT_STRING_OF_STAG=match s with\n\
- | Format.String_tag str -> str\n\
+ FORMAT_STRING_OF_STAG=match s with \
+ | Format.String_tag str -> str \
| _ -> raise (Invalid_argument "unsupported tag extension")
FORMAT_STAG_OF_STRING=Format.String_tag s
else
The \n quoting does not work on GNU make 4.2.1. I get
FORMAT_STRING_OF_STAG='match s withn | Format …`
The GNU make manual recommends to use the 'define' keyword to assign multi-line values to make variables, but why bother? We don't need the linebreaks, do we?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/159Ambiguous path error using why32021-02-22T12:55:18Zmantis-gitlab-migrationAmbiguous path error using why3ID0002454:
**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/160Does not build with OCaml 4.08.02022-09-28T11:03:06Zmantis-gitlab-migrationDoes not build with OCaml 4.08.0ID0002456:
**This issue was created automatically from Mantis Issue 2456. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002456:
**This issue was created automatically from Mantis Issue 2456. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002456 | Frama-C | Kernel > Makefile | public | 2019-06-18 | 2019-06-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | -current |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
The build fails with OCaml 4.08.0:
Packing /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.cmo
File "_none_", line 1:
Error: The implementation (obtained by packing)
does not match the interface /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.mli:
...
In module Cint:
Values do not match:
val is_cint_simplifier : Conditions/1.simplifier
is not included in
val is_cint_simplifier : Conditions/2.simplifier
File "src/plugins/wp/Cint.mli", line 80, characters 0-45:
Expected declaration
File "src/plugins/wp/Cint.mli", line 80, characters 0-45:
Actual declaration
File "_none_", line 1:
Definition of module Conditions/1
File "_none_", line 1:
Definition of module Conditions/2
gmake: *** [src/plugins/wp/.Makefile.plugin.generated:580: /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.cmo] Error 2
I suspect the problem lies in there being multiple identical Wp.mli files, each declaring the same Conditions module, which OCaml 4.08.0 now does not view as identical.François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/163invalid links to "ACSL by Example"2021-03-30T11:18:12ZJens Gerlachinvalid links to "ACSL by Example"ID0002449:
**This issue was created automatically from Mantis Issue 2449. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002449:
**This issue was created automatically from Mantis Issue 2449. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002449 | Frama-C | Documentation > website | public | 2019-06-08 | 2019-06-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The WP webpage (https://frama-c.com/wp.html) uses old (abandoned) links to "ACSL by Example".
I suggest to replace the link
http://www.fokus.fraunhofer.de/download/acsl_by_example
with
https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf
and the link
https://gitlab.fokus.fraunhofer.de/verification/open-acslbyexample.git
with
https://github.com/fraunhoferfokus/acsl-by-example
### Additional Information :
The suggested links have been stable for a couple of years now.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/164frama-c installation needs dune > 1.5 package installed2022-07-28T11:34:57Zmantis-gitlab-migrationframa-c installation needs dune > 1.5 package installedID0002448:
**This issue was created automatically from Mantis Issue 2448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002448:
**This issue was created automatically from Mantis Issue 2448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002448 | Frama-C | Documentation > website | public | 2019-06-04 | 2019-06-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | varosi | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | macOS | **OS Version** | Mojave |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Installation instructions here - https://frama-c.com/install-18.0-Argon.html#installing-frama-c-on-macos
Doesn't tell that dune package in spam should be > 1.5. This brakes build with strange message telling the reverse:
# Error: Version 1.5 of dune is not supported.
# Supported versions:
# - 0.0
# - 1.0 to 1.1
If you do install later package with:
opam install dune.1.9.3
Everything works just fine. So it would make life of newcomers like me easier if this is said in install instructions here:
https://frama-c.com/install-18.0-Argon.html#installing-frama-c-on-macosFrançois BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/168Division by zero doesn't increase the number of VC in console output2021-02-22T12:55:28Zmantis-gitlab-migrationDivision by zero doesn't increase the number of VC in console outputID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002428 | Frama-C | Plug-in > wp | public | 2019-02-17 | 2019-02-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Obvious division by zero doesn't increase the total number of proof obligations:
Test2:
<pre>
/*@ assigns \nothing;
*/
int test2(int a)
{
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test2.c (with preprocessing)
[rte] annotating function test2
[rte] test2.c:5:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
Proved goals line is the same as in the case without division:
Test1:
<pre>
/*@ assigns \nothing;
*/
int test1(int a)
{
return a;
}
</pre>
Frama-C output:
<pre>
[kernel] Parsing test1.c (with preprocessing)
[rte] annotating function test1
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
From my point of view this is an incorrect behavior and the proved goals like should be 'Proved goals: 1 / 2' as in this case:
Test3:
<pre>
/*@ assigns \nothing;
*/
int test3(int a)
{
//@ assert 0 != 0;
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test3.c (with preprocessing)
[rte] annotating function test3
[rte] test3.c:6:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_test3_assert : Unknown (109ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
</pre>
## Attachments
- [test2.c](/uploads/6a8a966174608d26a4e3aaca44d430f1/test2.c)https://git.frama-c.com/pub/frama-c/-/issues/169One \valid seems sufficient to write in a whole array.2021-02-22T12:55:31Zmantis-gitlab-migrationOne \valid seems sufficient to write in a whole array.ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002426 | Frama-C | Plug-in > wp | public | 2019-02-12 | 2019-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | VincentPenelle | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Linux Manjaro | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am on Chlorine version.
When I try to verify the following function with RTE guard enabled, WP succeeds. However, I think it should not, as only the first cell is specified to be valid, the rest is just specified to have valid read.
/*@ requires \valid(a);
@ requires \valid_read(a + (0 .. n-1));
@ requires 0 <= n <= INT_MAX;
*/
void foo(int *a, int n){
/*@ loop invariant 0 <= i <= n;
@ loop invariant \valid(a + (0 .. n-1));
*/
for (int i = 0; i<n;i++) a[i] = i;
}
Note: that works as well without any loop.
It doesn't work if you declare to pointers with different names, and declare one to be \valid and the other to be \valid_read (like in swap function for example).
It looks like the loop invariant \valid is simplified to true by Qed.
If that's normal, please explain me why.
Thanks,
--
Vincent Penelle.
### Steps To Reproduce :
Specify an array as being \valid_read, and one of its cells to be \valid.
Then, try to write in any cell.
Generate the RTE guards. WP should succeed to prove that the cells you're writing in are \valid.https://git.frama-c.com/pub/frama-c/-/issues/177Incorrect handling of \initialized when initialized struct is passed to a fun...2022-09-28T11:30:33ZKostyantyn VorobyovIncorrect handling of \initialized when initialized struct is passed to a function by valueID0002310:
**This issue was created automatically from Mantis Issue 2310. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002310:
**This issue was created automatically from Mantis Issue 2310. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002310 | Frama-C | Plug-in > E-ACSL | public | 2017-06-13 | 2019-01-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
This test case is derived from Toyota ITC benchmarks (File uninit_var.c, test case 012). Consider the following code:
struct S1 {
int t;
};
int foo(struct S1 s) {
/*@assert \initialized(&s.t); */
if (s.t > 0) return 0;
return 1;
}
int main(int argc, const char **argv) {
struct S1 s;
s.t = 1;
foo(s);
return 0;
}
Field `t` of struct `S1` is initialized in `main` but when it is passed to `foo` (by value) it's a brand new block where field `t` is not marked as initialized. Consequently assertion in `foo` wrongly fails.
## Attachments
- [itc-uninit-var-12.c](/uploads/4d29c1dc6442465e49a331c23bdd24b3/itc-uninit-var-12.c)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/178option -report-csv doesn't work anymore ?2021-02-22T12:55:41ZPatricia Mouyoption -report-csv doesn't work anymore ?ID0002423:
**This issue was created automatically from Mantis Issue 2423. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002423:
**This issue was created automatically from Mantis Issue 2423. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002423 | Frama-C | Plug-in > report | public | 2019-01-22 | 2019-01-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pmo | **Assigned To** | maroneze | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | linux | **OS** | ubuntu | **OS Version** | 4.18 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 19-Potassium | **Fixed in Version** | - |
### Description :
this option seems to be deprecated now ...
I know there is a new option to make report with Eva but only for red alarms and only with eva - I want a complete report as before with -report-csv
There is no indication at all in the changelog or maybe I've missed something ?
Is there a new way to use this option or another option to have the same result ?https://git.frama-c.com/pub/frama-c/-/issues/180E-ACSL crash with RTE generated assertion with booleans2021-04-20T07:09:09Zmantis-gitlab-migrationE-ACSL crash with RTE generated assertion with booleansID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002412 | Frama-C | Plug-in > E-ACSL | public | 2018-12-03 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux x86_64 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
There might be a regression with the RTE or E-ACSL plugin with Argon.
/////////// boolean.c
#include <stdbool.h>
bool return_false(void)
{
return false;
}
int main(void)
{
return 0;
}
///////////////////////////
### Additional Information :
On Chlorine-20180502 (bfd93b819) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
### Steps To Reproduce :
On Argon 18.0 (2f7a0eee0) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Current source was: rte_boolean.c:10
The full backtrace is:
Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023
Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 18.0 (Argon).
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
## Attachments
- [boolean.c](/uploads/1b34c066b4dc860013dcc10c38a49aad/boolean.c)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/181Missing cast in code generated by RTE2021-04-20T07:27:57ZJulien SignolesMissing cast in code generated by RTEID0002419:
**This issue was created automatically from Mantis Issue 2419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002419:
**This issue was created automatically from Mantis Issue 2419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002419 | Frama-C | Plug-in > RTE | public | 2018-12-17 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
==========
int main(void) {
int i = 2;
unsigned int j = i < 2;
return 0;
}
$ frama-c -check -rte -warn-unsigned-downcast -print -ocode res.c
[kernel] Parsing a.c (with preprocessing)
[rte] annotating function main
/* Generated by Frama-C */
int main(void)
{
int __retres;
int i = 2;
/*@ assert rte: unsigned_downcast: (i < 2) ≤ 4294967295; */
/*@ assert rte: unsigned_downcast: 0 ≤ (i < 2); */
unsigned int j = (unsigned int)(i < 2);
__retres = 0;
return __retres;
}
$ frama-c res.c
[kernel] Parsing res.c (with preprocessing)
[kernel:annot-error] res.c:6: Warning:
comparison of incompatible types: 𝔹 and ℤ. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
==========
The terms (i < 2) should be casted to int in the generated predicatesJulien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/188With -no-lib-entry, the dimension of global structs is not passed to the gene...2021-02-22T12:55:57ZNicky WilliamsWith -no-lib-entry, the dimension of global structs is not passed to the generatorID0001490:
**This issue was created automatically from Mantis Issue 1490. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001490:
**This issue was created automatically from Mantis Issue 1490. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001490 | Frama-C | Plug-in > pathcrawler | public | 2013-10-01 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nicky | **Assigned To** | muriel | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Compare the fixed_domain.pl file produced by running
frama-c -pc-analyzer -main test_me microwave.c
and
frama-c -pc-analyzer -main test_me microwave.c -lib-entry
There is no const_dim_input clause for structs mw_state and mw_inputs with the -no-lib-entry option
### Additional Information :
ajout de unrollType dans save_const_dim_input
## Attachments
- [microwave.c](/uploads/97d81542bcb5cea3951f8aaca63fa263/microwave.c)https://git.frama-c.com/pub/frama-c/-/issues/197Plug-in crash with "Unregistered_library_function" error2021-02-22T13:35:13ZKostyantyn VorobyovPlug-in crash with "Unregistered_library_function" errorID0002192:
**This issue was created automatically from Mantis Issue 2192. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002192:
**This issue was created automatically from Mantis Issue 2192. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002192 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | kvorobyov | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 14-Silicon |
### Description :
/** Instrumentation of the following program leads to the plug-in crash with Unexpected error (Misc.Unregistered_library_function("__store_block")) */
#include <stdlib.h>
char *a;
main(char *argv[]) {
a = argv = atoi(argv[1]);
}
### Additional Information :
This error has been extracted by creduce from one of the SPEC CPU2000 179.art benchmark. There seems to be an issue while processing the atoi ACSL contract. This error is triggered in at least 6 more SPEC benchmarks.https://git.frama-c.com/pub/frama-c/-/issues/216Strange dot callgraphs2021-02-22T12:56:30Zmantis-gitlab-migrationStrange dot callgraphsID0000989:
**This issue was created automatically from Mantis Issue 989. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000989:
**This issue was created automatically from Mantis Issue 989. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000989 | Frama-C | Plug-in > callgraph | public | 2011-10-19 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
First of all, the callgraph shown in the GUI is not the same than the one generated with the [-cg] option. In the GUI, some of the functions are not displayed at all (g1 and g2 in the enclosed example).
Moreover, in both graphs (from the GUI and the command line), there is an edge between [g] and [nxt] even if [g] doesn't directly call [nxt]...
## Attachments
- [toto.c](/uploads/32fad344b4c6d0d290edf568bdd94f1b/toto.c)https://git.frama-c.com/pub/frama-c/-/issues/219Too many edges in call graph2021-02-22T12:56:35Zmantis-gitlab-migrationToo many edges in call graphID0000435:
**This issue was created automatically from Mantis Issue 435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000435:
**This issue was created automatically from Mantis Issue 435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000435 | Frama-C | Plug-in > callgraph | public | 2010-03-28 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dclist | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
For some reason there are three edges on non-recursive function calls
in the dot file produced by frama-c -scg (see attached)
frama-c -scg foo.dot foo.c && dot -Tpng foo.dot
--------------------------------
int fact(int n)
{
if(n <= 0)
return 0;
else
return fact(n-1);
}
void foo(void)
{
printf("foo\n");
}
int main(void)
{
fact(10);
foo();
}
## Attachments
- [scg-frama.ps](/uploads/490d044b58af5d6a44bce73501b37139/scg-frama.ps)https://git.frama-c.com/pub/frama-c/-/issues/2232D variable length array2021-02-22T14:01:16ZJulien Signoles2D variable length arrayID0002186:
**This issue was created automatically from Mantis Issue 2186. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002186:
**This issue was created automatically from Mantis Issue 2186. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002186 | Frama-C | Kernel | public | 2015-11-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
2D variable length arrays are valid wrt C99 but rejected by Frama-C:
=====
extern int n;
int main(void) {
int a[n]; // accepted
int b[n][n]; // should be accepted, but refused
return 0;
}
=====
$ frama-c a.i
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing a.i (no preprocessing)
a.i:4:[kernel] warning: Variable-sized local variable a
a.i:5:[kernel] user error: Length of array is not a constant: n
a.i:5:[kernel] warning: Variable-sized local variable b
[kernel] user error: stopping on file "a.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
Reported by email by G. Karpenkovhttps://git.frama-c.com/pub/frama-c/-/issues/224`strlen` used from code makes it no longer possible to prove `assigns \nothing`.2021-02-22T12:56:40Zmantis-gitlab-migration`strlen` used from code makes it no longer possible to prove `assigns \nothing`.ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002380 | Frama-C | Plug-in > wp | public | 2018-06-23 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | namin | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
`strlen` used from code makes it no longer possible to prove `assigns \nothing`. The definition in the Frama-C library has `@ assigns \result \from indirect:s[0..];`, but this should not prevent check?
### Steps To Reproduce :
$ cat bug.c
#include <string.h>
/*@
requires strlen(s)>=0 && \valid(s+(0..strlen(s)));
assigns \nothing;
*/
int len(char *s) {
return strlen(s);
}
$ frama-c -wp -wp-rte -wp-prover CVC4,alt-ergo bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function len
[wp] 5 goals scheduled
[wp] [Failed] Goal typed_len_assign_normal_part1
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (324ms)
[wp] [Failed] Goal typed_len_assign_exit
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (322ms)
[wp] Proved goals: 3 / 5
Qed: 2 (0.35ms-0.85ms-2ms)
Alt-Ergo: 1 (15ms) (20) (unknown: 2)
CVC4: 0 (interrupted: 2)https://git.frama-c.com/pub/frama-c/-/issues/225Some issues related to Frama-C 18.0 (beta) "Argon"2021-02-22T13:33:32ZJens GerlachSome issues related to Frama-C 18.0 (beta) "Argon"ID0002408:
**This issue was created automatically from Mantis Issue 2408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002408:
**This issue was created automatically from Mantis Issue 2408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002408 | Frama-C | Plug-in > wp | public | 2018-11-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
This entry serves to link my GitHub issues on Argon (beta) to the BTS. The issues are
https://github.com/Frama-C/Frama-C-snapshot/issues/12
https://github.com/Frama-C/Frama-C-snapshot/issues/13
https://github.com/Frama-C/Frama-C-snapshot/issues/14https://git.frama-c.com/pub/frama-c/-/issues/227Failed to install framaC on macosx using opam2021-02-22T12:56:48Zmantis-gitlab-migrationFailed to install framaC on macosx using opamID0002399:
**This issue was created automatically from Mantis Issue 2399. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002399:
**This issue was created automatically from Mantis Issue 2399. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002399 | Frama-C | Opam | public | 2018-09-11 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.gimbert | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Apple | **OS** | macosx | **OS Version** | HighSierra 10.3. |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Followed step by step the install procedure on http://frama-c.com/install-chlorine-20180501.html#installing-frama-c-on-macos
Failed at the last step, because compilation of alt-ergo 1.30 fails with following message
hugo-3:~ gimbert$ opam install frama-c
The following actions will be performed:
∗ install alt-ergo 1.30 [required by frama-c]
∗ install frama-c 20180502
Alt-Ergo Graphical Interface can be used by the WP plug-in
Yojson enables kernel option -json-compilation-database
===== ∗ 2 =====
Do you want to continue ? [Y/n] Y
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[alt-ergo] Archive in cache
[frama-c] Archive in cache
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[ERROR] The compilation of alt-ergo failed at "make".
Processing 1/2: [alt-ergo: rm]
#=== ERROR while installing alt-ergo.1.30 =====================================#
# opam-version 1.2.2
# os darwin
# command make
# path /Users/gimbert/.opam/system/build/alt-ergo.1.30
# compiler system (4.07.0)
# exit-code 2
# env-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.env
# stdout-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.out
# stderr-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.err
### stdout ###
# [...]
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myDynlink.mli
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myDynlink.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myZip.mli
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myZip.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.mli
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.mli
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numbersInterface.mli
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numsNumbers.mli
### stderr ###
# Makefile.users:264: .depend: No such file or directory
# File "/Users/gimbert/.opam/system/build/alt-ergo.1.30/src/util/numsNumbers.mli", line 24, characters 47-62:
# Error: Unbound module Big_int
# make: *** [src/util/numsNumbers.cmi] Error 2
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
The following actions were aborted
∗ install frama-c 20180502
The following actions failed
∗ install alt-ergo 1.30
No changes have been performedhttps://git.frama-c.com/pub/frama-c/-/issues/228user error: scalar value (of type int) initialized by compound initializer2021-02-22T12:56:50Zmantis-gitlab-migrationuser error: scalar value (of type int) initialized by compound initializerID0002384:
**This issue was created automatically from Mantis Issue 2384. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002384:
**This issue was created automatically from Mantis Issue 2384. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002384 | Frama-C | Kernel | public | 2018-07-04 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Example:
<pre>
struct test {
union {
int a;
long b;
};
};
static struct test t = { { .a = 0 } };
</pre>
Run:
<pre>
$ gcc -c test.c
$ echo $?
0
$ frama-c test.c
</pre>
Error Log:
<pre>
[kernel] Parsing test.c (with preprocessing)
[kernel] test.c:1: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
[kernel] test.c:8: User Error:
scalar value (of type int) initialized by compound initializer
6 };
7
8 static struct test t = { { .a = 0 } };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[kernel] User Error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
</pre>
Frama-C Version:
<pre>
$ frama-c -version
Chlorine-20180501
</pre>
## Attachments
- [test.c](/uploads/9b2870c999eda7e90e97626672511315/test.c)
- [restore-initializers.patch](/uploads/9236fdb360274563d8f5bbc41595bd8c/restore-initializers.patch)https://git.frama-c.com/pub/frama-c/-/issues/229FE_* API is available on OpenBSD2021-02-22T12:56:52Zmantis-gitlab-migrationFE_* API is available on OpenBSDID0002379:
**This issue was created automatically from Mantis Issue 2379. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002379:
**This issue was created automatically from Mantis Issue 2379. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002379 | Frama-C | Kernel > libc | public | 2018-06-18 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | any | **OS** | OpenBSD | **OS Version** | 6.3 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
please include attached patch.
## Attachments
- [patch-src_libraries_utils_c_bindings_c](/uploads/5d11f5d41c049aab5269993f94365e40/patch-src_libraries_utils_c_bindings_c)https://git.frama-c.com/pub/frama-c/-/issues/231Generate out-of-scope variable when using quantified variable in a \old2021-02-22T12:56:54ZJulien SignolesGenerate out-of-scope variable when using quantified variable in a \oldID0001762:
**This issue was created automatically from Mantis Issue 1762. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001762:
**This issue was created automatically from Mantis Issue 1762. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001762 | Frama-C | Plug-in > E-ACSL | public | 2014-04-25 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | fmaurica | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
===== a.i =====
/*@ ensures \forall integer i; 0 <= i < 10 ==> \old(t[i]) == 0; */
void f(int *t) { }
int main(void) {
int t[10];
int i;
for(i = 0; i < 10; i++) t[i] = 0;
f(t);
return 0;
}
================
$ frama-c a.i -e-acsl -then-on e-acsl -print -ocode res.i
$ ./gcc.sh res.i
compiling res.i
res.i: In function ‘__e_acsl_f’:
res.i:84:53: error: ‘__e_acsl_i’ undeclared (first use in this function)
res.i:84:53: note: each undeclared identifier is reported only once for each funhttps://git.frama-c.com/pub/frama-c/-/issues/233Name of RTE plugin in documentation2021-02-22T13:59:32ZJens GerlachName of RTE plugin in documentationID0002398:
**This issue was created automatically from Mantis Issue 2398. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002398:
**This issue was created automatically from Mantis Issue 2398. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002398 | Frama-C | Documentation > manuals | public | 2018-09-04 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
The RTE plugin manual has two titles: On the title page it reads "Annotation Generation".
On the third page it reads "Frama-C’s annotation generator plug-in".
Neither title mentions "RTE". Is this intentional?
### Steps To Reproduce :
See http://frama-c.com/download/rte-manual-Chlorine-20180501.pdfhttps://git.frama-c.com/pub/frama-c/-/issues/234E-ACSL: internal error: raised at file "src/libraries/project/project.ml", li...2021-02-22T12:57:00Zmantis-gitlab-migrationE-ACSL: internal error: raised at file "src/libraries/project/project.ml", line 402ID0002386:
**This issue was created automatically from Mantis Issue 2386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002386:
**This issue was created automatically from Mantis Issue 2386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002386 | Frama-C | Plug-in > E-ACSL | public | 2018-07-06 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | fmaurica | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Error:
<pre>
$ frama-с -version
Chlorine-20180501
$ frama-с -e-acsl memchr.c
...
[e-acsl] test.c:21: Warning:
E-ACSL construct `variant' is not yet supported. Ignoring annotation.
[e-acsl] test.c:27: Warning:
invalid E-ACSL construct
`non integer variable k in quantification ∀ u8 *k; (u8 *)s ≤ k < p ⇒ *k ≢ (u8)c'.
Ignoring annotation.
[kernel] test.c:26: Failure:
mkBinOp: p - (unsigned char const *)s == __gen_e_acsl_at - n
[kernel] Current source was: test.c:39
The full backtrace is:
Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023
Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 791, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8
Frama-C aborted: internal error.
</pre>
Example code:
<pre>
/*@ requires \typeof(s) <: \type(u8 *);
requires \valid((u8 *)s+(0..n-1));
assigns \nothing;
behavior found:
assumes \exists u8 *p; (u8 *)s <= p < (u8 *)s + n && *p == (u8) c;
ensures s <= \result <= s + n;
ensures \forall u8 *p; (u8 *)s <= p < (u8 *)\result ==> *p != (u8) c;
ensures *((u8 *)\result) == (u8) c;
behavior not_exists:
assumes \forall u8 *p; (u8 *)s <= p < (u8 *)s + n ==> *p != (u8) c;
ensures \result == \null;
complete behaviors;
disjoint behaviors;
*/
void *memchr(const void *s, int c, size_t n)
{
const unsigned char *p = s;
/*@ loop invariant 0 <= n <= \at(n,Pre);
loop invariant (u8 *)s <= p <= (u8 *)s + \at(n,Pre);
loop invariant p - s == \at(n,Pre) - n;
loop invariant \forall u8 *k; (u8 *)s <= k < p ==> *k != (u8) c;
loop variant n;
*/
while (n-- != 0) {
if ((unsigned char) c == *p++) {
return (void *)(p - 1);
}
}
//@ assert n == (size_t)(-1);
return NULL;
}
int main(int argc, char *argv[])
{
const char *s = "1234567890";
void *ptr;
ptr = memchr(s, '0', 11);
ptr = memchr(s, 'a', 11);
ptr = ptr;
return 0;
}
</pre>
## Attachments
- [memchr.c](/uploads/6c87db6bb9861d6b6bb7f2ceb372297c/memchr.c)
- [memchr_v2.c](/uploads/d8f9701b3619dadb6d3936ef60d08be8/memchr_v2.c)https://git.frama-c.com/pub/frama-c/-/issues/235RTE assertion for signed right shift is wrong2021-02-22T12:57:02Zmantis-gitlab-migrationRTE assertion for signed right shift is wrongID0002354:
**This issue was created automatically from Mantis Issue 2354. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002354:
**This issue was created automatically from Mantis Issue 2354. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002354 | Frama-C | Plug-in > RTE | public | 2018-02-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | xleroy | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Consider:
/*@ ensures \result == arg >> 2; */
int toto(int arg) { return arg >> 2; }
"frama-c -wp -wp-rte" fails to verify this rather tautological spec because the RTE pass inserts the assertion
/*@ assert rte: shift: 0 ≤ arg; */
I think this is an incorrect reading of the ISO C 90 and C 99 specs: right-shift of a signed integer expression that has a negative value is implementation-defined, but is not an undefined behavior. (See ISO C 99 section 6.5.7 item 5.)
I would suggest that WP and RTE accept the spec above, so that I can actually reason about the right shift, probably by adding axioms specifying how right shifts of negative numbers work on the platforms I am (and everyone is) interested in.https://git.frama-c.com/pub/frama-c/-/issues/236E-ACSL: proper bitfileds handling2021-02-22T13:35:41Zmantis-gitlab-migrationE-ACSL: proper bitfileds handlingID0002305:
**This issue was created automatically from Mantis Issue 2305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002305:
**This issue was created automatically from Mantis Issue 2305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002305 | Frama-C | Plug-in > E-ACSL | public | 2017-05-29 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | fmaurica | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
E-ACSL generates code which takes address from bitfields. This leads to compilation error.
Test:
#include <stdbool.h>
struct bitfields {
int i : 2;
bool j : 1;
} t;
int test(struct bitfields *a)
{
return a->i;
}
int main(int argc, char **argv)
{
//@ assert \valid_read(&(t.j));
t.j = 1;
return test(&t);
}
E-ACSL code:
struct bitfields t;
int test(struct bitfields *a)
{
int __retres;
/*@ assert rte: mem_access: \valid_read(&a->i); */
{
int __gen_e_acsl_valid_read;
__e_acsl_store_block((void *)(& a),4U);
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& a->i), // ERROR
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",
(char *)"test",
(char *)"rte: mem_access: \\valid_read(&a->i)",10);
__retres = (int)a->i;
}
__e_acsl_delete_block((void *)(& a));
return __retres;
}
int main(int argc, char **argv)
{
int tmp;
__e_acsl_memory_init(& argc,& argv,4U);
__e_acsl_globals_init();
/*@ assert \valid_read(&t.j); */
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& t.j), // ERROR
sizeof(_Bool));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",
(char *)"main",(char *)"\\valid_read(&t.j)",15);
}
__e_acsl_initialize((void *)(& t.j),sizeof(_Bool)); //ERROR
t.j = (_Bool)1;
tmp = test(& t);
__e_acsl_delete_block((void *)(& t));
__e_acsl_memory_clean();
return tmp;
}
GCC Output on E-ACSL code:
# gcc ./generated.c
generated.c: In function ‘test’:
generated.c:86:60: error: cannot take address of bit-field ‘i’
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& a->i),
^
generated.c: In function ‘main’:
generated.c:112:60: error: cannot take address of bit-field ‘j’
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& t.j),
^
generated.c:117:32: error: cannot take address of bit-field ‘j’
__e_acsl_initialize((void *)(& t.j),sizeof(_Bool));
### Additional Information :
Quickfix (doesn't handle __e_acsl_initialize):
diff --git a/translate.ml b/translate.ml
index b5229db..1ea272e 100644
--- a/translate.ml
+++ b/translate.ml
@@ -704,7 +704,17 @@ and named_predicate_content_to_exp ?name kf env p =
| Pvalid_read _ -> "valid_read"
| _ -> assert false
in
- mmodel_call_with_size ~loc kf name Cil.intType env t
+ let ptyp = Cil.unrollType(Typing.typ_of_term(t)) in
+ let typ = match ptyp with
+ | TPtr(a,_) -> a
+ | _ -> assert false
+ in
+ let attr = Cil.typeAttrs typ in
+ if Cil.hasAttribute Cil.bitfield_attribute_name attr
+ then
+ not_yet env "Can't take address from variable with bitfield."
+ else
+ mmodel_call_with_size ~loc kf name Cil.intType env t
in
if !is_visiting_valid then begin
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
### Steps To Reproduce :
frama-c -e-acsl-prepare -rte -rte-precond ./bf.c -then -e-acsl -then-last -print
## Attachments
- [bf.c](/uploads/0e5781355d2eea694674f62ca97a7cc3/bf.c)
- [bitfileds.patch](/uploads/119108c3c57130706e94675406221748/bitfileds.patch)https://git.frama-c.com/pub/frama-c/-/issues/240frama-clang fails to compile2022-09-28T11:04:53Zmantis-gitlab-migrationframa-clang fails to compileID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002402 | Frama-C | Plug-in > clang | public | 2018-10-01 | 2018-10-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | barafael | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 18.04 LTS |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to compile frama-clang, I encounter
Error: Unbounded constructor ASinteger
in file convert_acsl.ml.
ASidentifier is also missing.
### Steps To Reproduce :
Get sources for frama-clang-0.0.6, configure, makeVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/241Newer releases of FramaC produce apparent WP plug-in bug2021-02-22T14:01:18Zmantis-gitlab-migrationNewer releases of FramaC produce apparent WP plug-in bugID0002403:
**This issue was created automatically from Mantis Issue 2403. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002403:
**This issue was created automatically from Mantis Issue 2403. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002403 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2018-10-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached code base is a small example in which a reactive program interacts with peripherals via memory mapped I/O through a constant address. While earlier releases of framaC (Phosphorous) was able to generate full and faithful altergo for our proofs, the new version produces syntactically malformed altergo for the following boolean logic function defined in our example's ACSL:
mac.h line 35:
logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_\
packet.object_low == 0x0A) && (mac->mac_packet.payload_length == 0x00));
Whereas such boolean logic functions were correctly axiomatized in the older (Phosphorous) release, the current version is axiomatizing such a function as :
function L_isAMessage
() :
bool =
andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))
note that the argument to the logic function is absent, and the fields of hte mac_t referenced in the logic function are rendered as "#{w_i}", about which altergo then complains. These malformed altergo expressions seem to have been generated by the pretty printer's find_var function.
### Steps To Reproduce :
tar -xvf framaBug.tar.gz
make wp
## Attachments
- [framaBug.tar.gz](/uploads/54add4d4c38c4a03cb21e9dd404eef64/framaBug.tar.gz)
- [frmaBug.tar.gz](/uploads/fccae63bbfa3517b0d9bc45326a5f0e6/frmaBug.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/242Missing __END_DECLS in ./share/libc/__fc_alloc_axiomatic.h2021-02-22T13:34:04Zmantis-gitlab-migrationMissing __END_DECLS in ./share/libc/__fc_alloc_axiomatic.hID0002400:
**This issue was created automatically from Mantis Issue 2400. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002400:
**This issue was created automatically from Mantis Issue 2400. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002400 | Frama-C | Plug-in > clang | public | 2018-09-21 | 2018-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | richardlford | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Ubuntu via WSL | **OS Version** | 16 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
In file ./share/libc/__fc_alloc_axiomatic.h there is a
__BEGIN_DECLS but no matching __END_DECLS.
When __BEGIN_DECLS expands to 'extern "C" {' and __END_DECLS expands
to '}' this results in miss-matched braces and the following
code appears to be under and extern "C". This leads to
errors, e.g. when template definitions are encountered.
### Additional Information :
Adding in the missing __END_DECLS removes this problem.
### Steps To Reproduce :
Install Frama-C Chlorine and frama-clang-0.0.6.
use the command "frama-c version.cpp" where version.cpp has this content:
// 'Hello World!' program
#include <iostream>
int main()
{
std::cout << "Hello World, version is "<< __cplusplus << "!" << std::endl;
return 0;
}
## Attachments
- [version.cpp](/uploads/346834ddcee99405a81e7ee8cce118f4/version.cpp)https://git.frama-c.com/pub/frama-c/-/issues/245Losing some cmdline option settings when loading2021-02-22T14:01:18ZJulien SignolesLosing some cmdline option settings when loadingID0000687:
**This issue was created automatically from Mantis Issue 687. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000687:
**This issue was created automatically from Mantis Issue 687. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000687 | Frama-C | Kernel | public | 2011-01-25 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "./bin/viewer.opt -val t.c", then clicking on "Execute": ok -val is correctly set.
BUT running "./bin/toplevel.opt -val -save t.sav t.c" followed by "./bin/viewer.opt -load t.sav", then clicking on "Execute": KO -val is not set anymore.
This behavior only exists for (what is internally called) 'action' parameters. Actually we must precise the exact semantics, and then implement it consistently.https://git.frama-c.com/pub/frama-c/-/issues/246WP is not able to validate a statically declared structure followed by a memset2021-02-22T12:57:18ZPatricia MouyWP is not able to validate a statically declared structure followed by a memsetID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002387 | Frama-C | Plug-in > wp | public | 2018-07-11 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pmo | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
By using a clean way to declare the structure, WP fails to validate the structure but by using a "dirty" way, it works !
#include <string.h>
typedef struct {
int i;
float f;
} stest;
void notclean_but_valid() {
char b[sizeof(stest)];
stest *s = b;
memset(s, 0, sizeof(stest));
}
void clean_but_invalid() {
stest s;
memset(&s, 0, sizeof(stest));
}
### Steps To Reproduce :
frama-c -wp-model typed_cast_ref -wp struc.chttps://git.frama-c.com/pub/frama-c/-/issues/247Can't compile2021-02-22T13:35:44Zmantis-gitlab-migrationCan't compileID0002391:
**This issue was created automatically from Mantis Issue 2391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002391:
**This issue was created automatically from Mantis Issue 2391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002391 | Frama-C | Kernel > Makefile | public | 2018-07-25 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yurichev | **Assigned To** | virgile | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x64 | **OS** | Ubuntu Linux | **OS Version** | 16.04 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Got this file: https://frama-c.com/download/frama-c-Chlorine-20180502.tar.gz
Unpacked, typed "./configure", then "make" and got:
======================================================================
...
Ocamlc src/libraries/datatype/type.cmi
Ocamlc src/kernel_services/plugin_entry_points/log.cmi
Ocamlc src/libraries/project/project_skeleton.cmi
Ocamlc src/libraries/utils/pretty_utils.cmi
Ocamlc src/libraries/stdlib/integer.cmi
File "src/libraries/stdlib/integer.mli", line 26, characters 9-12:
Error: Unbound module Z
share/Makefile.generic:70: recipe for target 'src/libraries/stdlib/integer.cmi' failed
make: *** [src/libraries/stdlib/integer.cmi] Error 2
======================================================================
## Attachments
- [make_stdout](/uploads/401d9f44f320b484e178a6155274ee0d/make_stdout)
- [make_stderr](/uploads/8ecf375aceb48adc242fde2b25e103a0/make_stderr)
- [config.log](/uploads/cd25941939119614209fbc318815d10f/config.log)https://git.frama-c.com/pub/frama-c/-/issues/248Frama-C GUI manual2021-02-22T12:57:24Zmantis-gitlab-migrationFrama-C GUI manualID0002393:
**This issue was created automatically from Mantis Issue 2393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002393:
**This issue was created automatically from Mantis Issue 2393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002393 | Frama-C | Documentation > manuals | public | 2018-08-09 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | maroneze | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Is there any detailed (stepwise) manual about GUI of Drama-C?
May be I'm missing some points but Could we edit/write new files within GUI interface? GUI seems to be not very user friendly...https://git.frama-c.com/pub/frama-c/-/issues/250cast error with reference fields2021-03-30T08:44:29Zmantis-gitlab-migrationcast error with reference fieldsID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002396 | Frama-C | Plug-in > clang | public | 2018-08-24 | 2018-08-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abhishek.anand.iitg@gmail.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | manjaro | **OS Version** | 8/23/3018 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
```
class B {
};
template <typename T>
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
B b;
B & y=b;
A<B> a(y);
}
```
I get the following error:
```
root@27db7a69b96a:/hostshare# frama-c -print refFieldBug.cpp
[kernel] Parsing refFieldBug.cpp (external front-end)
Now output intermediate result
[kernel] refFieldBug.cpp:8: Failure: castTo struct _Z1B -> struct _Z1B *
[kernel] User Error: stopping on file "refFieldBug.cpp" that has errors.
[kernel] Frama-C aborted: invalid user inp
```
I don't see what could be the problem because the following succeeds:
```
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
int x=0;
int & y=x;
A<int> a(y);
}
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/251request of clarification about using the address of a formal argument2021-02-22T13:48:48ZJens Gerlachrequest of clarification about using the address of a formal argumentID0002392:
**This issue was created automatically from Mantis Issue 2392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002392:
**This issue was created automatically from Mantis Issue 2392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002392 | Frama-C | Documentation > ACSL | public | 2018-07-25 | 2018-07-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | suspended |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
In #2390 the issue was raised whether functions contracts such as
/*@ requires
\valid(&a);
ensures \false; */
void f(int a) {
return ;
}
are meaningful.
More specifically, the ACSL manual should clarify whether using the address of a formal argument in a precondition is illegal.
(When I see that WP uses such a precondition to verify \false, them I am all in for disallowing it.)
Of course, it would also be nice if Frama-C (the kernel?) would issue a diagnostics.
### Additional Information :
The question also came up about using the address of a formal argument in a postcondition.
For the time being, I don't see it as a meaningful feature.https://git.frama-c.com/pub/frama-c/-/issues/252E-ACSL: vla handling2021-02-22T14:01:19Zmantis-gitlab-migrationE-ACSL: vla handlingID0002381:
**This issue was created automatically from Mantis Issue 2381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002381:
**This issue was created automatically from Mantis Issue 2381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002381 | Frama-C | Plug-in > E-ACSL | public | 2018-07-01 | 2018-07-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The code:
<pre>
int main(void)
{
int size = 10;
int array[size];
return 0;
}
</pre>
<pre>
a.out.frama.c:141: undefined reference to `__fc_vla_alloc'
a.out.frama.c:143: undefined reference to `__fc_vla_free'
collect2: error: ld returned 1 exit status
e-acsl-gcc: fatal error: fail to compile/link instrumented code
</pre>https://git.frama-c.com/pub/frama-c/-/issues/253Cannot compile variable length arrays2021-02-22T14:01:19ZArvid JakobssonCannot compile variable length arraysID0001834:
**This issue was created automatically from Mantis Issue 1834. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001834:
**This issue was created automatically from Mantis Issue 1834. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001834 | Frama-C | Plug-in > E-ACSL | public | 2014-07-15 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
The resulting C-code from running Frama-C with E-ACSL on the following program (same as attached):
int main(int argc, char **argv) {
int len = 4;
int data[len];
return 0;
}
cannot be compiled, giving the following error:
bug-vla.c:(.text+0xa74): undefined reference to `alloca'
the code generated is:
[...]
void *alloca(unsigned long);
[...]
int len;
int *data;
unsigned long __lengthofdata;
len = 4;
{
/*sequence*/
__lengthofdata = (unsigned long)len;
data = (int *)alloca(sizeof(*data) * __lengthofdata);
}
[...]
This code does not compile with GCC and the flag -std=c99.
## Attachments
- [bug-vla.c](/uploads/1c4f45e3e9069be2db558c88138b286a/bug-vla.c)https://git.frama-c.com/pub/frama-c/-/issues/254Crash when trying to analyse a file with jessie2021-04-15T09:16:54Zmantis-gitlab-migrationCrash when trying to analyse a file with jessieID0002334:
**This issue was created automatically from Mantis Issue 2334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002334:
**This issue was created automatically from Mantis Issue 2334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002334 | Frama-C | Plug-in > jessie | public | 2017-12-06 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abustany | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | 4.7.9 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
When running "frama-c -jessie jessie-crash.c" on the attached file, I get the following crash:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing encoding.c (with preprocessing)
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/__fc_string_axiomatic.h:35
The full backtrace is:
Raised at file "interp.ml", line 2383, characters 5-24
Called from file "interp.ml", line 2644, characters 22-41
Called from file "list.ml", line 70, characters 22-25
Called from file "interp.ml", line 2731, characters 27-66
Called from file "register.ml", line 175, characters 16-32
Called from file "register.ml", line 278, characters 6-12
Re-raised at file "register.ml", line 251, characters 29-103
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (File "interp.ml", line 2383, characters 5-11: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
My packages are at the following version:
frama-c 20170501
why 2.39
why3 0.87.3
ocaml 4.03.0
## Attachments
- [jessie-crash.c](/uploads/d0c7ce11aeaa47a5db5fcf2126955551/jessie-crash.c)https://git.frama-c.com/pub/frama-c/-/issues/256Crash on attempt to start framaCIRGen when libs are linked statically and dyn...2021-02-22T12:57:36Zmantis-gitlab-migrationCrash on attempt to start framaCIRGen when libs are linked statically and dynamically.ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002368 | Frama-C | Plug-in > clang | public | 2018-02-15 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DeMaze | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | GNU/Linux | **OS** | Debian | **OS Version** | 9.3 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
On the attempt to install Frama-Clang regularly as described (see
attached file installation.txt), the executable framaCIRGen exits with
an error when executed. The error message points to a problem with
LLVM. In fact, it depicts one commandline option to be registered more
than once. This occurs on the attempt of using Frama-C to parse C++
source code and when the executable framaCIRGen is invoked manually on
the commandline. I get the following error:
<output nr="0" command="./frama-clang-0.0.4/bin/framaCIRGen">
: CommandLine Error: Option 'asm-macro-max-nesting-depth' registered more than once!
LLVM ERROR: inconsistency in registered CommandLine options
</output>
However, this has only been observed ith llvm-5.0 on Debian GNU/Linux
9.3 (my system, see lsb_release_3ffbf_2018-02-10000905) for now. With
llvm 3.9, no such errors happen. Presumably, versions of llvm > 5.0
could also be affected. This seems to be a problem many people have
experienced with llvm related programs [2][3][4][5]. In fact, it has
even been reported for frama-clang [6].
### Additional Information :
Root Cause
==========
As far as my investigations revealed, this problem occurs because of
the linking mechanism on Debian GNU/Linux. On this distribution,
libraries of LLVM are built two-fold:
Static archives (lib*.a):
clangFrontend, clangDriver, clangTooling, clanParse, clangSema,
clangAnalysis, clangEdit, clangAST, clangLex, clangSerialization,
clangBasic, LLVMTransformUtils, LLVMBitReader, LLVMMCParser,
LLVMOption
Shared object (lib*.so):
LLVM-5.0
Therefore, it is tried to link them according to their type (lines 74-77, 82-85):
<output nr="1" command="cat frama-clang-0.0.4/Makefile.clang -n | grep 'USEDLIBS' -A 5 -B 5 ">
69 CFLAGS+=-g
70 CLANG_LINKFLAGS+=-g
71 endif
72
73 #LINK_COMPONENTS := $(TARGETS_TO_BUILD) asmparser support mc
74 USEDLIBS = clangFrontend \
75 clangDriver clangTooling clangParse clangSema \
76 clangAnalysis clangEdit clangAST clangLex clangSerialization \
77 clangBasic LLVMTransformUtils LLVMBitReader LLVMMCParser LLVMOption
78
79 # for use in main Makefile
80 default: $(PLUGIN_DIR)/bin/$(TOOLNAME)
81
82 $(PLUGIN_DIR)/bin/$(TOOLNAME): $(OBJS) $(PLUGIN_DIR)/bin
83 $(PRINT_LINKING) $@
84 $(CXX) $(CLANG_LINKFLAGS) -o $@ \
85 $(OBJS) $(addprefix -l,$(USEDLIBS)) $(LLVM_LIBS) $(CLANG_SYSLIBS) $(CLANG_LINKFLAGS)
86
87 $(PLUGIN_DIR)/bin:
88 $(MKDIR) $@
89
90 clean:
</output>
This results in the following dependencies on dynamic libraries as follows:
<output n="2" command="ldd ./frama-clang-0.0.4/bin/framaCIRGen">
linux-vdso.so.1 (0x00007ffe31ff5000)
libLLVM-5.0.so.1 => /usr/lib/x86_64-linux-gnu/libLLVM-5.0.so.1 (0x00007fb4c4825000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb4c44a3000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb4c419f000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb4c3f88000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb4c3be9000)
libffi.so.6 => /usr/lib/x86_64-linux-gnu/libffi.so.6 (0x00007fb4c39e0000)
libedit.so.2 => /usr/lib/x86_64-linux-gnu/libedit.so.2 (0x00007fb4c37a8000)
librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007fb4c35a0000)
libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb4c339c000)
libtinfo.so.5 => /lib/x86_64-linux-gnu/libtinfo.so.5 (0x00007fb4c3172000)
libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb4c2f55000)
libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x00007fb4c2d3b000)
/lib64/ld-linux-x86-64.so.2 (0x00007fb4c9431000)
libncurses.so.5 => /lib/x86_64-linux-gnu/libncurses.so.5 (0x00007fb4c2b18000)
libbsd.so.0 => /lib/x86_64-linux-gnu/libbsd.so.0 (0x00007fb4c2902000)
</output>
From this output, this assumption can be confirmed because
ligcc_s.so.1 as well as libLLVM-5.0.so.1 occurs. A response on a bug
report of LLVM considers this as rather bad practice
however. Moreover, this is mentioned as a classical problem of LLVM's
"global object-based commandline switch registration" [1]:
"The command line option error is the classical problem one gets due
to the LLVM's global object-based command line switch registration. If
you somehow link the same global object (that registers the command
line option) twice via dynamic loading of the LLVM library twice or
more to the same process, it registers the same command line object
again (when calling the global object initializer), resulting in this
error." [1]
The aforementioned symbol 'asm-macro-max-nesting-depth' occurs both in
libLLVMMCParser.a and libLLVM-5.0.so.1 . Hence, I conjecture these are
the files in conflict.
My Solution
===========
Just link without libLLVMMCParser.a or more precisely, remove
LLVMMCParser from USEDLIBS in Makefile.clang. This seems to work as
C++ code is analyzable again. Please find patches for Makefile.clang
attached which circumvent this problem according to my proposal
(Makefile.clang.patch / Makefile.clang.patch.better). Feel free to
contacting me in case of any further quesions / comments.
References
==========
[1] https://bugs.llvm.org/show_bug.cgi?id=30587#c6
[2] https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=768185
[3] https://bugs.llvm.org/show_bug.cgi?id=31571
[4] http://llvm.1065342.n5.nabble.com/llvm-dev-LLD-and-LLVM-LINK-LLVM-DYLIB-td104570.html
[5] https://github.com/zig-lang/zig/issues/67
[6] https://stackoverflow.com/questions/45647503/errors-when-using-the-frama-clang-plugin
### Steps To Reproduce :
1. Manually install llvm-5.0 as described on https://apt.llvm.org/
2. Download and build frama-clang as described officially with llvm-5.0
3. Execute ./bin/framaCIRGen
## Attachments
- [logs_and_more.tar.xz](/uploads/d2a4d0490b88cd4c21961e8a55ab0ca2/logs_and_more.tar.xz)https://git.frama-c.com/pub/frama-c/-/issues/257Issues while installation of Frama-C using OPAM2021-02-22T12:57:40Zmantis-gitlab-migrationIssues while installation of Frama-C using OPAMID0002375:
**This issue was created automatically from Mantis Issue 2375. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002375:
**This issue was created automatically from Mantis Issue 2375. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002375 | Frama-C | Opam | public | 2018-05-23 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Mac OS | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
I am having trouble while installation of frame-C on MacOS. I am trying to install it via OPAM.
I have installed all the dependencies also e.g
(brew install gmp gtk+ gtksourceview libgnomecanvas) but still it is not working.
please see the attached file for detailed error message
## Attachments
- [Terminal_Saved_Output](/uploads/7082f81c36f02c3d9c9831398809ace4/Terminal_Saved_Output)
- [framaC_Output](/uploads/a5124f3a2af8c58f9b21d67edb0a40be/framaC_Output)
- [Frama-CUpgrade](/uploads/2f7687f8cab2e31c03be170677f4b396/Frama-CUpgrade)https://git.frama-c.com/pub/frama-c/-/issues/258opam install why3 failed2021-02-22T12:57:42Zmantis-gitlab-migrationopam install why3 failedID0002373:
**This issue was created automatically from Mantis Issue 2373. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002373:
**This issue was created automatically from Mantis Issue 2373. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002373 | Frama-C | Opam | public | 2018-04-09 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | agrcs | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Mac | **OS** | Mac OS | **OS Version** | 10.13.3 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Following opam installation instructions at http://frama-c.com/install-sulfur-20171101.html#installing-frama-c-on-mac-os-x
all ok when: opam install altgr-ergo why3=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[ERROR] The compilation of conf-gtksourceview failed at "pkg-config --short-errors --print-errors gtksourceview-2.0".
#=== ERROR while installing conf-gtksourceview.2 ==============================#
# opam-version 1.2.2
# os darwin
# command pkg-config --short-errors --print-errors gtksourceview-2.0
# path /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2
# compiler system (4.06.1)
# exit-code 127
# env-file /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2/conf-gtksourceview-1291-1872ec.env
# stdout-file /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2/conf-gtksourceview-1291-1872ec.out
# stderr-file /Users/wenlongxie/.opam/system/build/conf-gtksourceview.2/conf-gtksourceview-1291-1872ec.err
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
The following actions were aborted
∗ install altgr-ergo 1.30
∗ install lablgtk 2.18.6
∗ install ocamlgraph 1.8.8
∗ install why3 0.88.3
∗ install why3-base 0.88.3
The following actions failed
∗ install conf-gtksourceview 2
No changes have been performed
=-=- conf-gtksourceview.2 troobleshooting -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
=> This package relies on external (system) dependencies that may be missing. `opam depext conf-gtksourceview.2' may help
you find the correct installation for your system.
ocaml is 4.06.1
opam is 1.2.2https://git.frama-c.com/pub/frama-c/-/issues/259Invalid sizeof(struct) calculation in Sulfur2021-02-22T12:57:43Zmantis-gitlab-migrationInvalid sizeof(struct) calculation in SulfurID0002344:
**This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002344:
**This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002344 | Frama-C | Plug-in > wp | public | 2018-01-19 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abustany | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
FramaC version: Sulfur-20171101 (cannot select it in BTS because of #0002343)
With the following C code:
-------------------------------
#include <stdint.h>
#include <string.h>
typedef struct {
uint8_t a;
uint8_t b;
uint8_t c;
uint16_t d;
uint16_t e;
uint16_t f;
char g[4086];
uint16_t h;
} message_t;
/*@ requires \valid(msg);
@*/
void reset_message(message_t *msg) {
memset(msg, 0, sizeof(message_t));
}
-------------------------------
Running: frama-c -wp -wp-fct reset_message -wp-rte -wp-print err.c
produces the following unprovable goal:
-------------------------------
Assume {
(* Heap *)
Have: (region(msg_0.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, msg_0, 4093).
}
Prove: valid_rw(Malloc_0, shift_sint8(w, 0), 4098).
-------------------------------
Using the Typed+cast model doesn't help.
I'm not really sure how the size of the struct is computed (with regard to alignment or padding), but somehow two different parts of the code seem to disagree here.https://git.frama-c.com/pub/frama-c/-/issues/260Frama-C incompatible with Coq 8.8.02021-02-22T12:57:44Zmantis-gitlab-migrationFrama-C incompatible with Coq 8.8.0ID0002377:
**This issue was created automatically from Mantis Issue 2377. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002377:
**This issue was created automatically from Mantis Issue 2377. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002377 | Frama-C | Opam | public | 2018-05-30 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ramsdell | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i686 | **OS** | Fedora | **OS Version** | 28 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Installation with opam worked well except that it deleted my modern version of Coq!
### Steps To Reproduce :
Install Coq and then install frama-chttps://git.frama-c.com/pub/frama-c/-/issues/261WP: internal error: only the kernel should set the status of property assumes2021-02-22T12:57:46Zmantis-gitlab-migrationWP: internal error: only the kernel should set the status of property assumesID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002383 | Frama-C | Plug-in > wp | public | 2018-07-04 | 2018-07-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Example:
<pre>
int test(void)
{
int a = 1;
/*@ behavior ok:
assumes a > 0;
ensures \true;
*/
return 3;
}
</pre>
Command:
<pre>
frama-c -wp test.c
</pre>
Log:
<pre>
[wp] [CFG] Goal test_stmt_ok_post : Valid (Unreachable)
[wp] [CFG] Goal test_stmt_ok_assume : Valid (Unreachable)
[kernel] failure: only the kernel should set the status of property assumes
a > 0
[kernel] Current source was: test.c:1
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 568, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 939, characters 6-44
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 9-16
Called from file "src/kernel_services/ast_data/property_status.ml", line 538, characters 4-109
Called from file "src/kernel_services/ast_data/property_status.ml" (inlined), line 551, characters 42-80
Called from file "src/plugins/wp/wpAnnot.ml", line 81, characters 4-71
Called from file "list.ml", line 85, characters 12-15
Called from file "list.ml", line 85, characters 12-15
Called from file "src/plugins/wp/wpAnnot.ml", line 1243, characters 10-38
Called from file "src/plugins/wp/wpAnnot.ml", line 1258, characters 12-28
Called from file "src/plugins/wp/wpAnnot.ml", line 1271, characters 16-68
Called from file "src/plugins/wp/Generator.ml", line 108, characters 4-67
Called from file "map.ml", line 270, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
</pre>
## Attachments
- [test.c](/uploads/2597c1f73c5b7b83511f003173086460/test.c)https://git.frama-c.com/pub/frama-c/-/issues/262Strange difference in generated Coq code between Chlorine and Sulfur2021-02-22T13:37:10ZJens GerlachStrange difference in generated Coq code between Chlorine and SulfurID0002374:
**This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002374:
**This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002374 | Frama-C | Plug-in > wp | public | 2018-05-09 | 2018-06-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This report refers to the BETA-release of Chlorine and affects a couple of Coq-proofs in ACSL by Example:
The problem is like this: If the attached file 'foo.c' is processed with the command line
frama-c -wp -wp-prover coq -wp-out foo.wp foo.c
then it produces in foo.wp among other files the Coq file A_Count.v.
The only difference when using with Frama-C-Sulfur or Frama-C-Chlorine is the following:
diff A_Count.sulfur.v A_Count.chlorine.v
28,32c28,32
< Hypothesis Q_CountSectionHit: forall (i_2 i_1 i : Z),
< forall (t : farray addr Z), forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
< (((t.[ (shift_sint32 a x) ]) = i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
< (((1 + ((L_Count t a i%Z x i_2%Z))) = ((L_Count t a i%Z i_1%Z i_2%Z)))%Z).
---
> Hypothesis Q_CountSectionHit: forall (i_1 i : Z), forall (t : farray addr Z),
> forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((i < i_1)%Z) ->
> ((is_sint32 x_1)) ->
> (((1 + ((L_Count t a i%Z x x_1))) = ((L_Count t a i%Z i_1%Z x_1)))%Z).
It looks like as if the argument 'v' of axiom 'CountSectionHit' has not been translated into Coq.
## Attachments
- [foo.c](/uploads/53423ef104c4f86e7469ef5bb783ec52/foo.c)
- [A_Count.sulfur.v](/uploads/774888275fb8101cef0293aaee7dafa5/A_Count.sulfur.v)
- [A_Count.chlorine.v](/uploads/878201905680422222e1b2e12a40293d/A_Count.chlorine.v)https://git.frama-c.com/pub/frama-c/-/issues/263frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined size...2021-04-20T17:20:20Zmantis-gitlab-migrationframa-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002376 | Frama-C | Plug-in > jessie | public | 2018-05-29 | 2018-05-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | foo | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi all,
I'm very new to the frama-c and why ecosystem. I hope it's really a bug with frama-c and not jessie.
The C input is:
#include<stdlib.h>
int main(void) {
char *p =malloc(5);
p[0] = 4;
return 3;
}
I'd like to verify that the write to p[0] goes toa valid address.
$ Frama-c -val -jessie t.c
[kernel] Parsing t.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_mblen_state ∈ [--..--]
__fc_mbtowc_state ∈ [--..--]
__fc_wctomb_state ∈ [--..--]
t.c:4:[value] allocating variable __malloc_main_l4
t.c:5:[value] warning: out of bounds write. assert \valid(p + 0);
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
p ∈ {{ &__malloc_main_l4[0] }}
__retres ∈ {3}
__malloc_main_l4[0] ∈ {4}
[1..4] ∈ UNINITIALIZED
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/stdlib.h:389
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/cil.ml", line 5238, characters 9-67
Called from file "common.ml", line 329, characters 27-46
Called from file "norm.ml", line 1551, characters 11-55
Called from file "norm.ml", line 1571, characters 37-71
Called from file "norm.ml", line 1614, characters 22-47
Called from file "norm.ml", line 1685, characters 19-43
Called from file "src/kernel_services/ast_queries/cil.ml", line 2239, characters 15-31
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 3543, characters 17-35
Called from file "src/kernel_services/ast_queries/cil.ml", line 3572, characters 12-19
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 3576, characters 23-50
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3613, characters 14-38
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3602, characters 5-80
Called from file "src/kernel_services/ast_queries/cil.ml", line 3840, characters 16-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 2323, characters 24-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 3808, characters 5-53
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 6463, characters 17-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 6468, characters 24-33
Called from file "src/kernel_services/ast_queries/cil.ml", line 6470, characters 3-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 6487, characters 15-39
Called from file "common.ml", line 580, characters 2-13
Called from file "norm.ml", line 1959, characters 2-26
Called from file "register.ml", line 158, characters 4-23
Called from file "register.ml", line 278, characters 6-12
Called from file "src/kernel_services/plugin_entry_points/journal.ml", line 442, characters 19-22
Re-raised at file "src/kernel_services/plugin_entry_points/journal.ml", line 457, characters 10-17
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sulfur-20171101.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[kernel] writing journal in file `./.frama-c/frama_c_journal.ml'.
### Additional Information :
I'm using
frama-c Sulfur-20171101
why 2.40
Why3 0.88.3
ocaml 4.06.1
## Attachments
- [frama_c_journal.ml](/uploads/d55e08324ce8dc26fa7317cab9a5d1be/frama_c_journal.ml)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/267C-function returning a struct causes warning on missing Ctor code/spec when i...2021-03-30T08:24:10ZJochen BurghardtC-function returning a struct causes warning on missing Ctor code/spec when inside 'extern "C" {...}'ID0002367:
**This issue was created automatically from Mantis Issue 2367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002367:
**This issue was created automatically from Mantis Issue 2367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002367 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp equal_range_cpp.cpp" prints
[kernel] warning: Assuming declared function pair::Ctor can't throw any exception
equal_range_cpp.cpp:6:[kernel] warning: Neither code nor specification for function pair::Ctor, generating default assigns from the prototype
Both messages disappear when the file is renamed to "equal_range_cpp.c" and/or the leading 'extern "C" {' and the trailing '}' are removed.
## Attachments
- [equal_range_cpp.cpp](/uploads/345e6cc5ed90e78e5878e8d5736cbef8/equal_range_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/268loop assigns clause ginored under strange circumstances2021-03-30T08:17:49ZJochen Burghardtloop assigns clause ginored under strange circumstancesID0002366:
**This issue was created automatically from Mantis Issue 2366. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002366:
**This issue was created automatically from Mantis Issue 2366. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002366 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp reverse_cpp.cpp" on the attached program reports
reverse_cpp.cpp:13:37: Ambiguity when choosing overloaded function Rev.
reverse_cpp.cpp:16:[wp] warning: Missing assigns clause (assigns 'everything' instead)
For the 1st message, cf. #2364, using a similar program.
The 2nd message disappears if
(1) the file is renamed to "reverse_cpp.c",
(2) the "assert" clause in line 10 is removed,
(3) the "loop invariant" clause in line 13 is removed, or
(4) the (possibly imaginary, cf. #2364) "Rev" ambiguity is resolved by removing one of the overloaded predicate definitions in lines 3 and 5.
## Attachments
- [reverse_cpp.cpp](/uploads/8c82fdfbc3ec2d18a714a489c7d8a4df/reverse_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/278predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang2021-03-30T08:05:33ZJochen Burghardtpredicate argument type "struct S" accepted by Frama-C, but not by Frama-clangID0002358:
**This issue was created automatically from Mantis Issue 2358. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002358:
**This issue was created automatically from Mantis Issue 2358. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002358 | Frama-C | Plug-in > clang | public | 2018-02-08 | 2018-02-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c stack_init_cpp.cpp" in the attached file results in an error message "keyword 'keyword -> struct' encountered when parsing a type" for line 6 (C++/C subroutine), but not for line 4 (Acsl predicate). When the file is renamed to "frama-c stack_init_cpp.c" , the error message disappears.
## Attachments
- [stack_init_cpp.cpp](/uploads/655f490009c017323d0b16f5261f5c9f/stack_init_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/279kernel warns about invalid implicit conversion2021-03-30T08:04:31ZJens Gerlachkernel warns about invalid implicit conversionID0002350:
**This issue was created automatically from Mantis Issue 2350. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002350:
**This issue was created automatically from Mantis Issue 2350. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002350 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-02-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
When processing the attached (C-)code with Fram-Clang the kernels sends a diagnostic as follows
frama-c -wp -wp-rte implicit_conversion.cpp
[kernel] Parsing implicit_conversion.cpp (external front-end)
implicit_conversion.cpp:16:44: invalid implicit conversion
Now output intermediate result
When processed as a ACSL/C file by WP no warning occurs.
## Attachments
- [implicit_conversion.cpp](/uploads/fe14759cabb542c2f83d85b61b0e28e9/implicit_conversion.cpp)
- [imcCnv2.cpp](/uploads/d6c96e86d9b3ff6a2032499013b2aac0/imcCnv2.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/282no diagnostics on wrong keyword2021-03-30T07:48:10ZJens Gerlachno diagnostics on wrong keywordID0002351:
**This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002351:
**This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002351 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached ACSL/C code contains a typo in the assigns clause:
"assign" instead of "assigns".
Frama-Clang provides no diagnostic message on this
frama-c -wp -wp-rte wrong_keyword.cpp
[kernel] Parsing wrong_keyword.cpp (external front-end)
Now output intermediate result
[rte] annotating function foo
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
When processed as a normal C file by Frama-C/WP a more appropriated message is shown
frama-c -wp -wp-rte wrong_keyword.c
[kernel] Parsing wrong_keyword.c (with preprocessing)
wrong_keyword.c:5:[kernel] user error: unexpected token 'a'
[kernel] user error: stopping on file "wrong_keyword.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [wrong_keyword.cpp](/uploads/577364237c433e7a05c5ae2104548eda/wrong_keyword.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/284BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"2021-02-22T12:58:14ZJens GerlachBTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"ID0002343:
**This issue was created automatically from Mantis Issue 2343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002343:
**This issue was created automatically from Mantis Issue 2343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002343 | Frama-C | Documentation | public | 2018-01-18 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version" ...https://git.frama-c.com/pub/frama-c/-/issues/291Incorrect dependency assignment using arraay inside for loop2021-02-22T13:12:37Zmantis-gitlab-migrationIncorrect dependency assignment using arraay inside for loopID0002341:
**This issue was created automatically from Mantis Issue 2341. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002341:
**This issue was created automatically from Mantis Issue 2341. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002341 | Frama-C | Plug-in > from | public | 2018-01-11 | 2018-01-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jaimeabe | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | urgent | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 16.04.3 LTS (GN |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file, the dependencies Analysis result should be GlobalVector[3] FROM Schalter dependent. However, the reality is that it assigns the dependenciy of Schalter to the whole vector (GlobalVector[0..4]).
### Steps To Reproduce :
Call the -deps Option in frama-c from command line using the attached file.
## Attachments
- [arrayInLoop.c](/uploads/54a6bd7ff7988631cf94538bcc12e52e/arrayInLoop.c)https://git.frama-c.com/pub/frama-c/-/issues/293Incorrect overflow and cast assertions for bitfields2021-02-22T13:36:38ZKostyantyn VorobyovIncorrect overflow and cast assertions for bitfieldsID0002314:
**This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002314:
**This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002314 | Frama-C | Plug-in > RTE | public | 2017-06-26 | 2017-12-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following snippet:
struct STR { int num : 7; };
void foo(int a, long b) {
struct STR s = { .num = 0 };
s.num = b;
s.num += a;
}
generates the following assertions
/*@ assert rte: signed_downcast: b ≤ 2147483647; */
/*@ assert rte: signed_downcast: -2147483648 ≤ b; */
s.num = (int)b;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)s.num + a; */
/*@ assert rte: signed_overflow: (int)s.num + a ≤ 2147483647; */
s.num = (int)((int)s.num + a);
The limits for s.num are incorrect, since s.num is a bitfield of 7 bits its limits should be [-64, 63]
### Steps To Reproduce :
frama-c -machdep x86_64 file.c -rte -warn-signed-overflow -warn-signed-downcast -print
## Attachments
- [b.c](/uploads/40289826f17e8973d35c95cb375e1d60/b.c)
- [patch-downcast-rte](/uploads/f5123ced359a007c0de00ba52c7fc3cd/patch-downcast-rte)https://git.frama-c.com/pub/frama-c/-/issues/294opam upgrade/update failed to update frama-c2021-02-22T12:58:31Zmantis-gitlab-migrationopam upgrade/update failed to update frama-cID0002335:
**This issue was created automatically from Mantis Issue 2335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002335:
**This issue was created automatically from Mantis Issue 2335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002335 | Frama-C | Kernel | public | 2017-12-07 | 2017-12-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cdelord | **Assigned To** | maroneze | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux x86_64 | **OS** | Fedora | **OS Version** | 26 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
opam refuses to upgrade from Frama-C Phosphorus to Sulfur because of dependency issues with the legacy frama-c-base package.
### Additional Information :
Workaround: opam remove frama-c-base
### Steps To Reproduce :
(previous version of frama-c installed with opam)
opam update
opam upgradehttps://git.frama-c.com/pub/frama-c/-/issues/295Should warn for overlapping lv=lv; assignments2021-03-29T08:03:16ZPascal CuoqShould warn for overlapping lv=lv; assignmentsID0000945:
**This issue was created automatically from Mantis Issue 945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000945:
**This issue was created automatically from Mantis Issue 945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000945 | Frama-C | Plug-in > Eva | public | 2011-09-01 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C should warn for this program:
struct S { int x; int y; };
struct T { int z; struct S s; };
union U { struct S f ; struct T g; } u;
main(){
u.f = u.g.s;
return 0;
}
6.5.16.1 3:
If the value being stored in an object is read from another object that overlaps in any way the storage of the first object, then the overlap shall be exact and the two objects shall have qualified or unqualified versions of a compatible type; otherwise, the behavior is undefined.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/297suggest to provide and document a unique warning string to grep for in value-...2021-02-22T13:36:36ZJochen Burghardtsuggest to provide and document a unique warning string to grep for in value-analysis output filesID0002259:
**This issue was created automatically from Mantis Issue 2259. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002259:
**This issue was created automatically from Mantis Issue 2259. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002259 | Frama-C | Plug-in > Eva | public | 2016-11-28 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | - |
### Description :
When running Frama-C value analysis with parameters that cause a huge output file, it is not possible to read thourgh it line by line. (My current output file, "results.txt.gz", has the size 700 MB in gzipped format) In this case, it is only possible to use tools like "zgrep -10 -n -i 'warning:' results.txt.gz >resultsExcerpt.txt" to find relevant messages.
The value analysis manual suggests (on p.41) to grep for "assert" to get all messages that relate to a proof obligation. However, warnings about non-terminating functions are not found this way, so at least another grep for "terminat" seems necessary. More important, I can't be not sure that "assert" and "terminat" will cover all relevant messages.
Therefore I suggest to provide a single search string that will appear at every relevant message. It shouldn't fit into C's variable name syntax (so 'warning:' is ok, but 'warning' is not). It should be mentioned in the manual at a prominent place when discussing the batch (i.e. non-gui) version of value analysis; it is an essential part of the methodology then.
If there are several such strings (e.g. for different degrees of severity, like 'error:' or 'hint:'), they should all be documented in that same place. A user who has read this documentation part should be confident about how to catch all relevant messages.https://git.frama-c.com/pub/frama-c/-/issues/301Substraction results in unknown values2021-03-26T16:58:43Zmantis-gitlab-migrationSubstraction results in unknown valuesID0002166:
**This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002166:
**This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002166 | Frama-C | Plug-in > Eva | public | 2015-09-17 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | buhler | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
This line of code has:
if (len + n >= 64) len -= n;
For callstack [SHA256_Update :: frama-test.c:19 <- main]
Before this statement / after this statement:
n ∈ [1..63]
and:
For callstack [SHA256_Update :: frama-test.c:19 <- main]
Before this statement:
len ∈ [1..1024]
After this statement:
len ∈ [--..--]
I was expecting len after this to be:
len ∈ [0..1023]
It might be non-obvious to get that completely correct from the first time, and could understand that it would be turned in:
len ∈ [-62..1023]
KurtDavid BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/303Support for struct containing flexible array members2021-03-23T17:20:25Zmantis-gitlab-migrationSupport for struct containing flexible array membersID0002306:
**This issue was created automatically from Mantis Issue 2306. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002306:
**This issue was created automatically from Mantis Issue 2306. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002306 | Frama-C | Kernel | public | 2017-05-29 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Flexible array member is a feature introduced in the C99 standard of the C programming language (in particular, in section §6.7.2.1, item 16, page 103).
Test:
struct cgroup {
int a;
int b[];
};
struct {
struct cgroup cgrp;
};
Frama-c run:
$ frama-c rte_cgrp.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing rte_cgrp.c (with preprocessing)
rte_cgrp.c:5:[kernel] user error: field cgrp is declared with incomplete type struct cgroup
[kernel] user error: stopping on file "rte_cgrp.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
### Steps To Reproduce :
frama-c rte_cgrp.c
## Attachments
- [rte_cgrp.c](/uploads/0ad8c8b6e4cd151d69fcefe6ec3fbf0d/rte_cgrp.c)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/305the return statement of a called function was wrongly removed2021-02-22T13:36:13Zmantis-gitlab-migrationthe return statement of a called function was wrongly removedID0002302:
**This issue was created automatically from Mantis Issue 2302. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002302:
**This issue was created automatically from Mantis Issue 2302. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002302 | Frama-C | Plug-in > slicing | public | 2017-05-23 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Yangyibiao | **Assigned To** | Nikolai_Kosmatov | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Ubuntu | **OS Version** | Ubuntu 16.04.4 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
While slicing the last statement in the attached test.c file, the "return g_79;" statement in function func_2 (line 312 in the test.c file) was wrongly removed from the slice.
gcc version: gcc(Ubuntu-5.4.0-6ubuntu1~16.04.4) 5.4.0 20160609
frama-c version: Silicon-20161101
### Tags :
csmith
### Steps To Reproduce :
frama-c -cpp-command "gcc -C -E " test.c -slice-pragma main -then-on 'Slicing export' -print -ocode slice.c
gcc test.c -o test && ./test
gcc slice.c -o slice && ./slice
## Attachments
- [test.c](/uploads/adbee40e23d6254e092332570c6b656f/test.c)https://git.frama-c.com/pub/frama-c/-/issues/306repeated predicate definitions in separate file cause crash2021-02-22T14:01:23ZJochen Burghardtrepeated predicate definitions in separate file cause crashID0002322:
**This issue was created automatically from Mantis Issue 2322. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002322:
**This issue was created automatically from Mantis Issue 2322. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002322 | Frama-C | Kernel | public | 2017-07-31 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Running 'frama-c -wp part.c whole.c' on the attached files causes the follwoing crash:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing part.c (with preprocessing)
[kernel] Parsing whole.c (with preprocessing)
[wp] warning: Missing RTE guards
[kernel] Current source was: whole.c:12
The full backtrace is:
Raised at file "map.ml", line 117, characters 16-25
Called from file "list.ml", line 55, characters 20-23
Called from file "src/plugins/wp/LogicCompiler.ml", line 772, characters 17-61
Called from file "src/plugins/wp/Warning.ml", line 139, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 853, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 41-46
Called from file "src/plugins/wp/Warning.ml", line 155, characters 14-18
Called from file "src/plugins/wp/cfgWP.ml", line 461, characters 23-135
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "list.ml", line 84, characters 24-34
Called from file "src/plugins/wp/calculus.ml", line 339, characters 22-62
Called from file "src/plugins/wp/calculus.ml", line 343, characters 23-45
Called from file "src/plugins/wp/calculus.ml", line 647, characters 20-43
Called from file "src/plugins/wp/calculus.ml", line 606, characters 19-40
Called from file "src/plugins/wp/calculus.ml", line 757, characters 40-59
Called from file "set.ml", line 305, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/calculus.ml", line 757, characters 4-64
Called from file "src/plugins/wp/calculus.ml", line 793, characters 19-51
Called from file "src/plugins/wp/cfgWP.ml", line 1468, characters 43-66
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/cfgWP.ml", line 1456, characters 14-957
Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 25-28
Called from file "src/plugins/wp/Model.ml", line 126, characters 19-36
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
The problem disappears if:
* the source file order is exchanged on the command line,
* the overloaded predicate 'Bnd(integer n)' in while.c:5 is renamed e.g. to 'Bnd2',
* the trivial 'ensures' clause is removed in whole.c:10, or
* the 'requires' clause in whole.c:9 is changed to 'Bnd(1,(int)0)', i.e. 'Bnd' is inlined.
## Attachments
- [part.c](/uploads/d19b970ae0a4ede44f1a974e55fcd0b9/part.c)
- [whole.c](/uploads/2cc05d6d85775174d51049260a279891/whole.c)https://git.frama-c.com/pub/frama-c/-/issues/307predicate overloading causes crash when multiple files are given to wp2021-02-22T14:01:23ZJochen Burghardtpredicate overloading causes crash when multiple files are given to wpID0002151:
**This issue was created automatically from Mantis Issue 2151. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002151:
**This issue was created automatically from Mantis Issue 2151. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002151 | Frama-C | Kernel > ACSL implementation | public | 2015-07-30 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | xubuntu14.04 | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c -wp 481a.c 481b.c" on the attached files causes a crash with following output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 481a.c (with preprocessing)
[kernel] Parsing 481b.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[kernel] Current source was: 481b.c:9
The full backtrace is:
Raised at file "map.ml", line 117, characters 16-25
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/LogicCompiler.ml", line 776, characters 17-61
Called from file "src/wp/Warning.ml", line 139, characters 6-10
Called from file "src/wp/LogicSemantics.ml", line 813, characters 12-42
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 462, characters 23-140
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "list.ml", line 84, characters 24-34
Called from file "src/wp/calculus.ml", line 331, characters 22-64
Called from file "src/wp/calculus.ml", line 341, characters 23-45
Called from file "src/wp/calculus.ml", line 613, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 586, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 724, characters 40-59
Called from file "set.ml", line 304, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/wp/calculus.ml", line 724, characters 4-64
Called from file "src/wp/calculus.ml", line 770, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1402, characters 39-62
Called from file "src/wp/cfgWP.ml", line 1391, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 15-40
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 27-29
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
## Attachments
- [481a.c](/uploads/bbfbbd240806e1f43941db309a86ecd8/481a.c)
- [481b.c](/uploads/6eb9eab3b5ff4466235f341d5f87e5c4/481b.c)https://git.frama-c.com/pub/frama-c/-/issues/308E-ACSL: compilation fail: generated functions doesn't have static inline attr...2021-02-22T12:58:55Zmantis-gitlab-migrationE-ACSL: compilation fail: generated functions doesn't have static inline attributesID0002304:
**This issue was created automatically from Mantis Issue 2304. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002304:
**This issue was created automatically from Mantis Issue 2304. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002304 | Frama-C | Plug-in > E-ACSL | public | 2017-05-29 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
The absence of static inline attributes forces optional dependencies to be strict. This leads to undefined reference errors during compilation.
Test (inline.c):
extern int do_mmap(int *a);
static inline int test_extern(int *a) // Static inline
{
return do_mmap(a);
}
int main(void)
{
return 0;
}
GCC Run:
$ gcc ./inline.c # There is no error about do_mmap
$ echo $?
0
Generated Code (inline_generated.c):
...
/*@ assigns \result, *a;
assigns \result \from *a;
assigns *a \from *a; */
int __gen_e_acsl_do_mmap(int *a);
...
__inline static int test_extern(int *a)
{
int tmp;
/*@ behavior pre_do_mmap:
assigns tmp, *a;
assigns tmp \from *a;
assigns *a \from *a;
*/
tmp = __gen_e_acsl_do_mmap(a);
return tmp;
}
...
/*@ assigns \result, *a;
assigns \result \from *a;
assigns *a \from *a; */
int __gen_e_acsl_do_mmap(int *a) // <== ERROR
{
int __retres;
__retres = do_mmap(a);
return __retres;
}
GCC Run:
$ gcc ./inline_generated.c
/tmp/cczBUd0r.o: In function `__gen_e_acsl_do_mmap':
inline_generated.c:(.text+0x24): undefined reference to `do_mmap'
collect2: error: ld returned 1 exit status
### Additional Information :
Quickfix:
diff --git a/dup_functions.ml b/dup_functions.ml
index 5774115..3b25fde 100644
--- a/dup_functions.ml
+++ b/dup_functions.ml
@@ -197,6 +197,8 @@ let dup_global loc old_prj spec bhv kf vi new_vi =
let name = vi.vname in
Options.feedback ~dkey ~level:2 "entering in function %s" name;
let fundec = dup_fundec loc spec bhv kf vi new_vi in
+ fundec.svar.vinline <- true;
+ fundec.svar.vstorage <- Static;
let fct = Definition(fundec, loc) in
let new_spec = fundec.sspec in
let new_kf = { fundec = fct; spec = new_spec } in
### Steps To Reproduce :
frama-c -e-acsl-prepare -rte -rte-precond ./inline.c -then -e-acsl -then-last -print > inline_generated.c
gcc inline_generated.c
## Attachments
- [inline.c](/uploads/c2d9a86ad5918510e45daae55935ae17/inline.c)
- [inline.patch](/uploads/df7aafd5ea9cdab056e99d6bec1a5365/inline.patch)https://git.frama-c.com/pub/frama-c/-/issues/309E-ACSL generates functions definitions without argument-names2021-02-22T12:58:57Zmantis-gitlab-migrationE-ACSL generates functions definitions without argument-namesID0002303:
**This issue was created automatically from Mantis Issue 2303. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002303:
**This issue was created automatically from Mantis Issue 2303. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002303 | Frama-C | Plug-in > E-ACSL | public | 2017-05-29 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Test:
extern int test(int *);
static inline int test2(int *a)
{
return test(a);
}
Output:
...
/*@
predicate diffSize{L1, L2}(ℤ i) =
\at(__e_acsl_heap_allocation_size,L1) -
\at(__e_acsl_heap_allocation_size,L2) ≡ i;
*/
/*@ assigns \result;
assigns \result \from \nothing; */
int __gen_e_acsl_test(int *);
/*@ assigns \result;
assigns \result \from \nothing; */
extern int test(int *);
...
/*@ assigns \result;
assigns \result \from \nothing; */
int __gen_e_acsl_test(int *) // <== ERROR
{
int __retres;
__retres = test();
return __retres;
}
### Additional Information :
Possible fix:
diff --git a/dup_functions.ml b/dup_functions.ml
index e87ce02..d447353 100644
--- a/dup_functions.ml
+++ b/dup_functions.ml
@@ -157,10 +157,22 @@ let dup_funspec tbl bhv spec =
end in
Cil.visitCilFunspec o spec
+
+let gen_name name idnum =
+ if name = ""
+ then
+ let id = idnum + 1 in
+ ("__e_acsl_tmp_var_" ^ string_of_int (id), id)
+ else
+ (name, idnum)
+
let dup_fundec loc spec bhv kf vi new_vi =
new_vi.vdefined <- true;
let formals = Kernel_function.get_formals kf in
- let new_formals = List.map (fun vi -> Cil.copyVarinfo vi vi.vname) formals in
+ let idnum : int ref = ref 0 in
+ let new_formals = List.map (fun vi -> let (name, id) = gen_name vi.vname !idnum in
+ (idnum := id);
+ Cil.copyVarinfo vi name) formals in
let res =
let ty = Kernel_function.get_return_type kf in
if Cil.isVoidType ty then None
### Steps To Reproduce :
frama-c -main test2 -e-acsl-prepare -rte -rte-precond ./argument_names.c -then -e-acsl -then-last -print
## Attachments
- [argument_names.c](/uploads/f6a48e4adf8624e308ef43220f1b2a94/argument_names.c)
- [argument_names.patch](/uploads/2f81a843d78ef5f5e7d9a9a21c2d9c14/argument_names.patch)https://git.frama-c.com/pub/frama-c/-/issues/310syntax error before loop contract reported after loop contract2021-02-22T13:34:00ZJochen Burghardtsyntax error before loop contract reported after loop contractID0002297:
**This issue was created automatically from Mantis Issue 2297. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002297:
**This issue was created automatically from Mantis Issue 2297. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002297 | Frama-C | Kernel | public | 2017-05-08 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Running "frama-c -wp synt.c" gives the output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing synt.c (with preprocessing)
[kernel] syntax error at synt.c:7:
5 loop assigns i,s;
6 loop variant 9-i;
7 */
^^^
8 for (int i=0; i<9; ++i)
9 s += 2;
[kernel] Frama-C aborted: invalid user input.
This suggests that there is some syntax error within the loop contract (and it often takes a long time to check the contract byte by byte for correctness). However, the error is the missing semi-colon in line 3, immediately before the contract.
## Attachments
- [synt.c](/uploads/394b26965a65ecc018ff2e8c94d2008b/synt.c)https://git.frama-c.com/pub/frama-c/-/issues/311opam installation of frama-c-base fails2021-02-22T12:59:01Zmantis-gitlab-migrationopam installation of frama-c-base failsID0002331:
**This issue was created automatically from Mantis Issue 2331. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002331:
**This issue was created automatically from Mantis Issue 2331. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002331 | Frama-C | Kernel > Makefile | public | 2017-11-07 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | seberoon | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | mac | **OS** | mac os | **OS Version** | 10.11.6 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Following opam installation instructions at https://frama-c.com/install-phosphorus-20170501.html#installing-frama-c-on-mac-os-x.
All ok up until opam install frama-c-base, which fails:
# File "src/plugins/wp/qed/src/numbers.mll", line 131, characters 18-19:
# Error: This expression has type string but an expression was expected of type
# bytes
This is using a fresh installation of homebrew and opam.
### Additional Information :
Mac OS 10.11.6
Xcode 8.2.1
## Attachments
- [frama-c_install_fail.txt](/uploads/21e1e50e3f88505149e7ba982b3583b9/frama-c_install_fail.txt)https://git.frama-c.com/pub/frama-c/-/issues/312Command "Show callgraph" fails.2021-02-22T13:38:43Zmantis-gitlab-migrationCommand "Show callgraph" fails.ID0002270:
**This issue was created automatically from Mantis Issue 2270. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002270:
**This issue was created automatically from Mantis Issue 2270. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002270 | Frama-C | Graphical User Interface | public | 2017-01-12 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Cygwin | **OS** | Windows 7 | **OS Version** | x64 SP1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Callgraph is not displayed with "Show callgraph".
In cygwin terminal prints as follows:
"dot" ▒▒ ▒▒▒▒ ▒▒▒▒७▒▒▒ ▒▒▒ ▒▒▒譥▒
▒▒▒▒▒▒▒▒, ▒ᯮ▒▒塞▒▒ ▒ணࠬ▒▒▒ ▒▒▒ ▒▒▒▒▒▒ 䠩▒▒▒.
In callback for signal activate, uncaught exception: DGraphModel.DotError("Error during dot execution")
Raised at file "format.ml", line 185, characters 41-52
Called from file "format.ml", line 427, characters 6-24
### Additional Information :
Callgraph plug-in was run with default settings. File dgraph######.dot was created in cygwin64/tmp directory successfully.
### Steps To Reproduce :
In GUI select Analises -> Show callgraphhttps://git.frama-c.com/pub/frama-c/-/issues/313compilation fails on i386 with gcc-72021-02-22T13:40:00ZRalf Treinencompilation fails on i386 with gcc-7ID0002328:
**This issue was created automatically from Mantis Issue 2328. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002328:
**This issue was created automatically from Mantis Issue 2328. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002328 | Frama-C | Plug-in > E-ACSL | public | 2017-09-08 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | treinen | **Assigned To** | kvorobyov | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | i386 | **OS** | linux | **OS Version** | debian sid |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | Frama-C 16-Sulfur | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
we have a compilation failure of frama-c on i386. A complete log of an attempt to compile can be found here:
https://buildd.debian.org/status/fetch.php?pkg=frama-c&arch=i386&ver=20170501%2Bphosphorus%2Bdfsg-1&stamp=1502480362&raw=0
Please note that the default compiler on debian sid is gcc-7.https://git.frama-c.com/pub/frama-c/-/issues/314File frama-c/libc/features.h should include definition of the macro __GNUC_PR...2021-04-01T21:06:09ZJochen BurghardtFile frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.hID0002253:
**This issue was created automatically from Mantis Issue 2253. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002253:
**This issue was created automatically from Mantis Issue 2253. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002253 | Frama-C | Kernel > libc | public | 2016-10-17 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
The macro __GNUC_PREREQ is used in many system include files. It is defined in referring to "/usr/include/features.h"l.
However, a "#include <features.h>" directive is redirected by Frama-C to (e.g.) "~/.opam/system/share/frama-c/libc/features.h" which doesn't define the macro.
Adding the definition there wouldn't cause any harm (? - at least, I can't think of any) and would help to make more system include files work with Frama-C.https://git.frama-c.com/pub/frama-c/-/issues/315Parser does not handle mixed concatenations of wide and non-wide strings2021-02-22T12:59:09ZPascal CuoqParser does not handle mixed concatenations of wide and non-wide stringsID0001467:
**This issue was created automatically from Mantis Issue 1467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001467:
**This issue was created automatically from Mantis Issue 1467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001467 | Frama-C | Kernel | public | 2013-08-07 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
~/ppc $ cat tests/misc/wstring_phase6.i
/* run.config
OPT: -journal-disable -print
*/
// See http://stackoverflow.com/questions/18102502/mixing-wide-and-narrow-string-literals-in-c
main(){
printf( "%s\n", "123" "456" );
printf( "%ls\n", L"123" L"456" );
printf( "%ls\n", "123" L"456" );
printf( "%ls\n", L"123" "456" );
printf( "%ls\n", L"123" L"456" );
}
~/ppc $ bin/toplevel.opt -print tests/misc/wstring_phase6.i
tests/misc/wstring_phase6.i:9:[kernel] user error: syntax error
[kernel] user error: skipping file "tests/misc/wstring_phase6.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
~/ppc $
### Additional Information :
As commented in the test, the behavior is defined and is explained in http://stackoverflow.com/questions/18102502/mixing-wide-and-narrow-string-literals-in-chttps://git.frama-c.com/pub/frama-c/-/issues/318Duplicates are created on the tab "Messages"2022-09-28T11:26:37Zmantis-gitlab-migrationDuplicates are created on the tab "Messages"ID0002276:
**This issue was created automatically from Mantis Issue 2276. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002276:
**This issue was created automatically from Mantis Issue 2276. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002276 | Frama-C | Graphical User Interface | public | 2017-02-03 | 2017-11-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | maroneze | **Resolution** | reopened |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
New messages append to old messages on the tab "Messages" if an analysis are rerun with new options.
### Steps To Reproduce :
1. Run Value analysis.
2. Change any option.
3. Run Value analysis.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/319Make it build on bytecode architectures2021-02-22T12:59:14Zmantis-gitlab-migrationMake it build on bytecode architecturesID0002325:
**This issue was created automatically from Mantis Issue 2325. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002325:
**This issue was created automatically from Mantis Issue 2325. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002325 | Frama-C | Graphical User Interface | public | 2017-08-11 | 2017-09-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Hi,
Frama-C's GUI doesn't build on bytecode only architecture because the Makefile always depend on TARGET_GUI which may contain native objects.
Please find attached a simple patch that fixes this issue.
## Attachments
- [0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch](/uploads/1f211d8c6be79ada3a7ab5a60cd9838e/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch)https://git.frama-c.com/pub/frama-c/-/issues/320Spelling errors2021-02-22T12:59:16Zmantis-gitlab-migrationSpelling errorsID0002323:
**This issue was created automatically from Mantis Issue 2323. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002323:
**This issue was created automatically from Mantis Issue 2323. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002323 | Frama-C | Documentation | public | 2017-08-11 | 2017-09-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Hi,
I've found some spelling errors in Frama-C's source code. Please find attached a patch to fixe them.
## Attachments
- [0008-More-fixes-of-spelling-errors.patch](/uploads/202926e102b518e7e14b24d4d1de7011/0008-More-fixes-of-spelling-errors.patch)
- [0001-Fix-spelling-error-in-binary.patch](/uploads/78cca8ddcb2d7003d2128aae12eb17ce/0001-Fix-spelling-error-in-binary.patch)https://git.frama-c.com/pub/frama-c/-/issues/321Value.cmo needs LoopAnalysis.cmo2021-02-22T12:59:17Zmantis-gitlab-migrationValue.cmo needs LoopAnalysis.cmoID0002326:
**This issue was created automatically from Mantis Issue 2326. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002326:
**This issue was created automatically from Mantis Issue 2326. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002326 | Frama-C | Plug-in > Eva | public | 2017-08-11 | 2017-09-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Value plugin needs LoopAnalysis, but appears first during the linking
phase. In order to workaround that, we move it before Value.cmo in the
PLUGIN_CMO_LIST variable.
Please find attached a simple patch which fixes this in the Makefile.
## Attachments
- [0005-Value.cmo-needs-LoopAnalysis.cmo.patch](/uploads/10d367477191926bad9aa0e5fae200dd/0005-Value.cmo-needs-LoopAnalysis.cmo.patch)https://git.frama-c.com/pub/frama-c/-/issues/322Port to OCaml 4.052021-02-22T12:59:20Zmantis-gitlab-migrationPort to OCaml 4.05ID0002324:
**This issue was created automatically from Mantis Issue 2324. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002324:
**This issue was created automatically from Mantis Issue 2324. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002324 | Frama-C | Kernel | public | 2017-08-11 | 2017-08-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
In order to make Frama-C build with OCaml 4.05. Please a find patch attached that introduces a few minor changes and make it compile again.
## Attachments
- [0007-Fix-FTBFS-with-OCaml-4.05.0.patch](/uploads/03c4935869f9dc001ab55e76af16df0b/0007-Fix-FTBFS-with-OCaml-4.05.0.patch)https://git.frama-c.com/pub/frama-c/-/issues/323Configure step fails on bytecode architectures2021-02-22T12:59:21Zmantis-gitlab-migrationConfigure step fails on bytecode architecturesID0001763:
**This issue was created automatically from Mantis Issue 1763. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001763:
**This issue was created automatically from Mantis Issue 1763. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001763 | Frama-C | Kernel > configure | public | 2014-04-28 | 2017-08-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The configure step fails on pure bytecode architectures with the following message:
checking for /usr/lib/ocaml/ocamlgraph/graph.cmo... yes
configure: OcamlGraph 1.8.5 > 1.8.4 found: should be compatible, but no warranty. Use it at your own risk!
configure: OcamlGraph 1.8.5 is incompatible with Frama-C.
configure: switching to OcamlGraph provided by Frama-C
checking for ocamlgraph... no
checking for ocamlgraph.tar.gz... no
configure: error: cannot find OcamlGraph in the current directory.
Quite strange: would your Frama-C distribution be corrupted?
Anyway:
1. download the latest version from http://ocamlgraph.lri.fr/download
2. install it by './configure && make && make install'
3. rerun ./configure here
make[1]: *** [override_dh_auto_configure] Error 1
It is due to the fact that the script tries to compile a test program linking against the OCamlgraph library in the native case and calls ocamlgraph_error in the bytecode case instead of trying to compile the test program.
In order to make Frama-C build on bytecode architecture, I've disabled that call to ocamlgraph_error.https://git.frama-c.com/pub/frama-c/-/issues/324statement contract apparently confuses parser2021-04-15T09:31:56ZJochen Burghardtstatement contract apparently confuses parserID0002301:
**This issue was created automatically from Mantis Issue 2301. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002301:
**This issue was created automatically from Mantis Issue 2301. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002301 | Frama-C | Plug-in > wp | public | 2017-05-11 | 2017-07-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp assigns.c" on the attached program produces a warning:
assigns.c:12:[wp] warning: Missing assigns clause (assigns 'everything' instead)
The warning is unjustified since the loop in line 12 does have a "loop assigns" clauses, and loops don't use (plain) "assigns" clauses.
If the trivial assertion in line 9 is activated, the warning disappears, and everything is proven.
If instead the braces in line 5 and 7 are removed, Frama-c reports a crash (text see "Additional Information").
### Additional Information :
Crash message:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing assigns.c (with preprocessing)
[wp] failure: Several assigns ?
[kernel] Current source was: assigns.c:2
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 568, characters 30-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 15-16
Called from file "src/plugins/wp/wpStrategy.ml", line 470, characters 13-63
Called from file "src/plugins/wp/wpStrategy.ml", line 505, characters 8-34
Called from file "list.ml", line 73, characters 12-15
Called from file "src/plugins/wp/wpStrategy.ml", line 541, characters 2-34
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/wpAnnot.ml", line 1023, characters 2-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1094, characters 15-41
Called from file "src/plugins/wp/wpAnnot.ml", line 1273, characters 14-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1274, characters 9-22
Called from file "src/plugins/wp/wpAnnot.ml", line 1363, characters 2-47
Called from file "map.ml", line 168, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
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
## Attachments
- [assigns.c](/uploads/f5df9089249e50094cfbca65b1a403f3/assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/327Statement contracts and WP2023-07-24T10:25:01ZJens GerlachStatement contracts and WPID0002317:
**This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002317:
**This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002317 | Frama-C | Documentation > manuals | public | 2017-07-18 | 2017-07-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a follow-up on issue https://bts.frama-c.com/view.php?id=2300 which was rather briskly closed.
I can understand that the question on the semantics of statement contracts in WP is not discussed in the ACSL implementation manual. However, in my opinion, it should then be discussed in the WP manual.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/328suggest to clarify semantics of statement contract in ACSL implementation manual2021-02-22T14:01:24ZJochen Burghardtsuggest to clarify semantics of statement contract in ACSL implementation manualID0002300:
**This issue was created automatically from Mantis Issue 2300. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002300:
**This issue was created automatically from Mantis Issue 2300. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002300 | Frama-C | Documentation > ACSL | public | 2017-05-11 | 2017-07-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | patrick | **Resolution** | no change required |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | Silicon/Phosphorus | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
We were wondering about the semantical difference between assertions and a statement contract. Therefore, we ran "frama-c -wp contractTest.c" on the attached program (Frama-c version Phosphorus-20170501-beta1). The assertion "bar" couldn't be proven (without the statement contract, it could). This supports our hypothesis that a statement contract completely overrides the standard Hoare-calculus semantics.
However, this isn't explicitly stated in the ACSL Implementation manual (version Silicon-20161101), where statement contracts are mentioned on p.12 and 36, and mainly in their own section (2.4.4) on p.44-45.
We therefore wonder if the observed "override behavior" is just special to the WP plugin, or if it is part of the ACSL language definition and obligatory for all plug-ins. An appropriate sentence in section 2.4.4 could clarify this question.
## Attachments
- [contractTest.c](/uploads/2b83abb09390db63e48f41428c49a323/contractTest.c)https://git.frama-c.com/pub/frama-c/-/issues/330unsoundness after external function call2021-02-22T12:59:30Zmantis-gitlab-migrationunsoundness after external function callID0002315:
**This issue was created automatically from Mantis Issue 2315. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002315:
**This issue was created automatically from Mantis Issue 2315. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002315 | Frama-C | Plug-in > Eva | public | 2017-07-01 | 2017-07-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | maxime | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi everyone,
Frama-C is unsound after an external function call. See the attached file.
Running frama-c -val unsound.c gives me:
[value] Called Frama_C_show_each_r({1})
This is wrong. The call to the external function f can update **x, and so *y can be anything.
At the call to f(x), I think you should grab all the base addresses that are reachable by the arguments and set them to TOP.
### Steps To Reproduce :
frama-c -val unsound.c
## Attachments
- [unsound.c](/uploads/f18a6127d86087eb32b6b831193aceb8/unsound.c)https://git.frama-c.com/pub/frama-c/-/issues/331suggestions for improvement of Sect.3.6 and 3.7 of the wp manual2023-07-24T10:43:54ZJochen Burghardtsuggestions for improvement of Sect.3.6 and 3.7 of the wp manualID0002313:
**This issue was created automatically from Mantis Issue 2313. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002313:
**This issue was created automatically from Mantis Issue 2313. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002313 | Frama-C | Documentation > manuals | public | 2017-06-15 | 2017-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | wp-manual-Phosphorus-20170501.pd | **OS** | n/a | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the WP manual, section 3.6 "The Typed Memory Model", instead of explaining the "Typed" memory model, refers to an old "Store" memory model and only describes the differences. However, few (and increasingly fewer) users are familiar with that old model, let alone availability issues of old WP manuals. Therefore, the "Typed" model should be described from scratch. Also, the section should initially state that it is about the model named "Typed".
In section 3.7, I found the following senteces hard to understand, and added my questions in "{}":
This detection is more clever than the standard one {That is, the one of the "Typed" model?} since it only takes into account local usage {What is local and global usage of a function? How can an approach being more clever than another one although it is based on less information?} of each function (not global ones).
Additionally, the Caveat memory model of Frama-C performs a local allocation {What is a local allocation? Shouldn't Frama-C's allocation reflect those made by the C compiler, which pushes actual parameters on the local stack in a new stack-frame, and expects formal parameters on the local stack in the current stack frame?} of formal parameters with pointer types that cannot be treated as reference parameters.
This makes explicit the separation hypothesis of memory regions pointed by formals in the Caveat tool. The major benefit of the WP version {Compared to what? To the Caveat tool? To the plain "Typed" model?} is that aliases are taken into account by the Typed memory model, hence, there are no more suspicious aliasing warnings.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/332value analysis introduces weird pointer assert with variable length arrays2021-02-22T12:59:35Zmantis-gitlab-migrationvalue analysis introduces weird pointer assert with variable length arraysID0002137:
**This issue was created automatically from Mantis Issue 2137. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002137:
**This issue was created automatically from Mantis Issue 2137. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002137 | Frama-C | Plug-in > Eva | public | 2015-06-26 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rcl | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
The value analysis plugin generates an assertion of the form
/*@ assert
Value: ptr_comparison:
\pointer_comparable((void *)*(arr+0), (void *)val);
*/
when arr is a VLA. This assertion looks bogus; it doesn't make any sense and doesn't even type check.
### Steps To Reproduce :
Run the value analysis plugin on the attached source code form.
## Attachments
- [ptrcmp.c](/uploads/11abeaa22c5401127f5cbb7d5985a107/ptrcmp.c)
- [ptrcmp.2.c](/uploads/4f5a1ba7e847d9950b81756c1170a3f0/ptrcmp.2.c)https://git.frama-c.com/pub/frama-c/-/issues/333false postcondition shouldn't be verified in default memory-model setting2021-04-15T09:30:17ZJochen Burghardtfalse postcondition shouldn't be verified in default memory-model settingID0002312:
**This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002312:
**This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002312 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte memmodel_default.c" verifies all 11 proof obligations, while the assert clase in line 21 is obviously violated. The reason for Frama-C's behavior is that it assumes the "Hoare Variables mixed with Pointers" memory model as a default (in accordance with WP manual sect.3.4, p.45) without checking its preconditions, viz. the absence of any address-taking of a variable.
A novice user who doesn't yet know about the subtleties of memory models will assume after the above Frama-c run that the program is ok, as is has been formally verified. This may build up unjustified trust in the program, and discredit Frama-C (or even the whole field of formal methods) once the bug is detected at runtime, possibly causing severe damage.
I suggest to either
1. check the applicability of the "Hoare Variables mixed with Pointers" model (this should be easily achievable, if only the source code needs to be scanned for a unary "&"), or
2. use another, less restrictive, model as default.
## Attachments
- [memmodel_default.c](/uploads/05c89d93d3c5c3dde72d94f83901958d/memmodel_default.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/334poor errors message texts for Hoare memory model checks2021-09-21T13:21:18ZJochen Burghardtpoor errors message texts for Hoare memory model checksID0002311:
**This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002311:
**This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002311 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | sometimes |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-model Hoare memmodel_Hoare.c" on the attached program produces the output:
...
[rte] annotating function foo
memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:8:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:8:[wp] warning: No validity
memmodel_Hoare.c:4:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:3:[wp] warning: No validity
[wp] 4 goals scheduled
...
The name of the memory model is "Hoare" on the command line and in the WP manual (Sect.3.2, p.44), but it is called "Empty" in the error message output.
Moreover, the message "No validity" should be expanded to be more understandable. As an additional convenience, Frama-C could mention in each message the variable it refers to ("x" resp. "*x") in all cases in the example).
## Attachments
- [memmodel_Hoare.c](/uploads/913f6495cac3874938af5d592e39d609/memmodel_Hoare.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/336naming the default behavior influences proven obligations2021-04-15T09:29:03ZJochen Burghardtnaming the default behavior influences proven obligationsID0002309:
**This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002309:
**This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002309 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp ilog2_beh.c -wp-prop ilog2 -wp-prover alt-ergo -wp-prover cvc4" on the attached program proves everything except (the lemmas and) loop invariant "a".
However, when lines 16,27,30,36,41 are uncommented, i.e. the default behavior is assigned an explicit name, everything except (the lemmas and) the loop variant is proven instead.
Naming vs. not naming a behavior shouldn't have such an influence.
## Attachments
- [ilog2_beh.c](/uploads/61d5de2e4e4cfecc8959933e484a3108/ilog2_beh.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/337suggest to check (loop) assigns clauses by data flow analysis2021-08-05T09:22:29ZJochen Burghardtsuggest to check (loop) assigns clauses by data flow analysisID0002308:
**This issue was created automatically from Mantis Issue 2308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002308:
**This issue was created automatically from Mantis Issue 2308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002308 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | low | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | n/a | **OS** | n/a | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp ifft_assigns.c -wp-prop check -wp-prover cvc4" on the attached file proved \false in line 339, which was intentionally inserted as a consistency check at the file's end. The reason for the inconsistency turned out to be a missing variable in a loop assigns clause (commented out for demo purposes in line 237). The detailled argument doesn't matter here; nevertheless it is given in (*) below for convenience.
I guess it would be easy for Frama-C to perform some coarse data-flow analysis and issue a warning about "nu2" being modified in line 295, but missing in the "loop assigns" clauses for the loop in line 242-302. Such an analysis could ignore nontrivial aliases, dead code, and array subranges, thus making it straight-forward to implement.
The example shows the value of warnings that such an analysis is able to issue. Already in this tiny example, it is easy to lose overview (cf. the many experimental "asserts", most of which a probably unncessary, or even nonsensical), and any tool help that doesn't cost much additional computation time is appreciated.
As a further application, it could print suggestions for "assigns" clauses of loops and procedure contracts.
(*): In fact, property "a2" from line 214 implies "nu1!=65536", if the latter variable remained unchanged during the loop in line 242-302, then property "c2" in line 232 boild down to "nu1+l==nu", which is false after the loop since then the termination condition "nu<l" has to hold, and "nu1" is unsigned.
## Attachments
- [ifft_assigns.c](/uploads/c813b7d252cb81e38d9f4fe871139244/ifft_assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/338Incorrectness when early exiting a block2021-02-22T12:59:41ZJulien SignolesIncorrectness when early exiting a blockID0001740:
**This issue was created automatically from Mantis Issue 1740. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001740:
**This issue was created automatically from Mantis Issue 1740. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001740 | Frama-C | Plug-in > E-ACSL | public | 2014-04-07 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
Local variables of a block are de-allocated at the end of the block. However, they are not de-allocated when exiting a block earlier (e.g. by a goto or a break). That may lead to incorrectness as in the attached example.
$ frama-c -e-acsl a.i -then-on e-acsl -print -ocode b.i
$ ./gcc.sh b.i
compiling b.i
executing b.i
Assertion failed at line 13 in function main.
The failing predicate is:
!\valid(p).
No error should be detected.
## Attachments
- [a.i](/uploads/6d82b2b9c687fba962ef8c594c4645d2/a.i)https://git.frama-c.com/pub/frama-c/-/issues/339Invalid results in presence of pseudo-recursive calls in inout and from2021-02-22T12:59:43ZBoris YakobowskiInvalid results in presence of pseudo-recursive calls in inout and fromID0000733:
**This issue was created automatically from Mantis Issue 733. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000733:
**This issue was created automatically from Mantis Issue 733. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000733 | Frama-C | Plug-in > inout | public | 2011-02-20 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
The Inout and From plugins are apparently designed to handle "pseudo" recursive calls, ie. when the value analysis does not detect a recursive call, but the plugin see a circularity in the stacks of examined functions. However, they are all buggy, because of the way the results are cached.
Indeed, when a circularity is encountered, the analysis is stopped immediately. This means that the results for the first function in the cycle is correct, but not those for the intermediate functions.
This can be seen with the example file: the inputs (option -input) for function h2 should include x.
### Additional Information :
Commit 12050 has removed most of the warnings the plugins printed unnecessarily when those pseudo recursive calls were encountered, so the error can now be completely silent (however, even with the warnings the plugins were buggy, as they implied that the analysis was correct if the value analysis was happy).
I have some (quite obvious) suggestions for correcting the bug, but they are not very efficient wrt to time complexity. Suggestions are welcome.
## Attachments
- [recursion2.i](/uploads/8eb737ed45eea708129388baa739b6db/recursion2.i)https://git.frama-c.com/pub/frama-c/-/issues/340EVA analysis does not start with click on "Execution" button.2021-02-22T12:59:44Zmantis-gitlab-migrationEVA analysis does not start with click on "Execution" button.ID0002279:
**This issue was created automatically from Mantis Issue 2279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002279:
**This issue was created automatically from Mantis Issue 2279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002279 | Frama-C | Plug-in > Eva | public | 2017-02-10 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
EVA analysis does not start with click on "Execution" button. But if select -val option it does it.
User have to click on "Run" button to start EVA analysis. This is unusual behavior.
### Steps To Reproduce :
1. [Customize EVA analysis]
2. Click on "Execution" button.
3. Verify that analysis did not started.
4. Select -val option.https://git.frama-c.com/pub/frama-c/-/issues/341Operability depends on the order of options changes2021-02-22T12:59:47Zmantis-gitlab-migrationOperability depends on the order of options changesID0002277:
**This issue was created automatically from Mantis Issue 2277. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002277:
**This issue was created automatically from Mantis Issue 2277. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002277 | Frama-C | Plug-in > Eva | public | 2017-02-03 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
If value analysis is run on attached file with default options Frama-C makes no warnings. If you then turn on -warn-signed-downcast and repeat the analysis, a warning appears on the Message tab:
main.c:13:[value] warning: signed downcast. assert 128 ≤ 127;
If you reload Frama-C and turn on -warn-signed-downcast before first running of analysis, analysis will not run.
On Console tab will be output:
[value] Initial state computed
[value:initial-state] Values of globals at initialization
NOT ACCESSIBLE
[value] Value analysis not started because globals initialization is not computable.
If you then turn off -warn-signed-downcast and repeat the analysis, nothing changes.
### Steps To Reproduce :
1. Run Frama-C GUI.
2. Add attached file.
3. Turn on -warn-signed-downcast option.
4. Run value analysis.
5. Turn off -warn-signed-downcast option.
6. Run value analysis.
7. Reload Frama-C GUI.
8. Add attached file.
9. Run value analysis.
10. Turn on -warn-signed-downcast option.
11. Run value analysis.
## Attachments
- [main.c](/uploads/6fa38af626b269dcd5cb4e77024b802e/main.c)https://git.frama-c.com/pub/frama-c/-/issues/342There is a typo in description of plug-in: "objuscator" instead of "obfuscator".2022-09-08T08:56:38Zmantis-gitlab-migrationThere is a typo in description of plug-in: "objuscator" instead of "obfuscator".ID0002269:
**This issue was created automatically from Mantis Issue 2269. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002269:
**This issue was created automatically from Mantis Issue 2269. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002269 | Frama-C | Plug-in > obfuscator | public | 2017-01-12 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | none | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
$ frama-c -plugins
...
Obfuscator objuscator for confidential code (-obfuscator-h)
...
And there is the same typo in GUI: "Objuscator for confidential code".
### Steps To Reproduce :
1. In command line enter:
frama-c -plugins
2. In GUI select Analyses -> Obfuscator.https://git.frama-c.com/pub/frama-c/-/issues/343GMP typing issue2021-02-22T13:36:42ZKostyantyn VorobyovGMP typing issueID0002252:
**This issue was created automatically from Mantis Issue 2252. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002252:
**This issue was created automatically from Mantis Issue 2252. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002252 | Frama-C | Plug-in > E-ACSL | public | 2016-10-14 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Gentoo | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | Frama-C GIT, precise the release id | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
In the below snippet
1 int i = -1;
2 ...
3 /*@ assert rte: mem_access: \valid_read(srcbuf+i); */
4 if ((int)*(srcbuf + i) == (int)ch)
5 loc = i;
a buffer overflow occurs because of the initial negative value of i, however, assertion generated by E-ACSL features the following line:
__e_acsl_valid_read((void *)(srcbuf + (unsigned long)i), sizeof(char));
which casts i to an unsigned integer and further make the assertion wrongly pass. See the attached code for a more complete example. The code is taken from the ITC toyota benchmark.
## Attachments
- [bts2252.c](/uploads/a893c82edbd7b918f04be7ce1db2c29d/bts2252.c)https://git.frama-c.com/pub/frama-c/-/issues/344Functions that claim to return a struct but don't cause a crash2021-02-22T12:59:51Zmantis-gitlab-migrationFunctions that claim to return a struct but don't cause a crashID0002235:
**This issue was created automatically from Mantis Issue 2235. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002235:
**This issue was created automatically from Mantis Issue 2235. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002235 | Frama-C | Kernel | public | 2016-06-21 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
If a function returns a struct in its declaration, but it's method body does not return anything, Frama-C will warn about not finding a return value, and then crash.
While the kernel does warn you this is an issue, no invalid operation on the user's part should cause a crash. Instead, it should cause a user error.
### Additional Information :
Tested with Aluminum on Linux 64-bit.
### Steps To Reproduce :
== File bug.c:
struct s {
int i;
};
struct s foo() {}
== Run command:
frama-c bug.c
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug2.c:5:[kernel] warning: Body of function foo falls-through and cannot find an appropriate return value
bug2.c:5:[kernel] failure: Found return without value in function foo
[kernel] Current source was: bug.c:5
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 583, characters 30-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 577, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 580, characters 15-16
Called from file "src/kernel_internals/typing/oneret.ml", line 246, characters 8-87
Called from file "src/kernel_internals/typing/oneret.ml", line 354, characters 22-54
Called from file "src/kernel_internals/typing/oneret.ml", line 361, characters 13-35
Called from file "src/kernel_services/ast_queries/file.ml", line 891, characters 6-26
Called from file "list.ml", line 73, characters 12-15
Called from file "src/kernel_services/ast_queries/file.ml", line 1143, characters 5-43
Called from file "src/kernel_services/ast_queries/file.ml", line 1579, characters 2-22
Called from file "src/kernel_services/ast_queries/file.ml", line 1666, characters 4-27
Called from file "src/kernel_services/ast_data/ast.ml", line 111, characters 2-28
Called from file "src/kernel_services/ast_data/ast.ml", line 123, characters 53-71
Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 787, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 817, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
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_guidelineshttps://git.frama-c.com/pub/frama-c/-/issues/346E-ACSL type system crash2021-02-22T12:59:53ZKostyantyn VorobyovE-ACSL type system crashID0002284:
**This issue was created automatically from Mantis Issue 2284. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002284:
**This issue was created automatically from Mantis Issue 2284. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002284 | Frama-C | Plug-in > E-ACSL | public | 2017-02-24 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Gentoo | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
Run:
e-acsl-gcc.sh --rte=mem mesa_error.c
crashes E-ACSL with the following message:
[e-acsl] failure: expected an integral type for (int)((float)(*(red + i) * scale))
Base frama-C command:
frama-c -no-frama-c-stdlib a.c -rte -no-warn-signed-overflow -no-warn-unsigned-overflow -no-warn-signed-downcast -no-warn-unsigned-downcast -rte-no-div -rte-no-float-to-int -rte-mem -rte-no-pointer-call -rte-no-precond -rte-no-shift -rte-no-trivial-annotations -then -e-acsl -then-last -print -ocode a.out.frama.c
Supposedly this happens because integer interval is computed incorrectly due to casts
## Attachments
- [mesa_int_.c](/uploads/f3a468bf58a654a54205a4088c53f92b/mesa_int_.c)https://git.frama-c.com/pub/frama-c/-/issues/347type of float parameter changed unexpectedly to double2021-02-22T12:59:54Zmantis-gitlab-migrationtype of float parameter changed unexpectedly to doubleID0002283:
**This issue was created automatically from Mantis Issue 2283. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002283:
**This issue was created automatically from Mantis Issue 2283. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002283 | Frama-C | Plug-in > wp | public | 2017-02-24 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | widc | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | 16.04 LTS |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
Current source was: sgn.c:4
The full backtrace is:
Raised at file "hashtbl.ml", line 328, characters 23-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Frama-C aborted: internal error.
Your Frama-C version is Silicon-20161101.
From the floating_point.ml the following message is reported:
Could not parse floating point number "-0x1.0000000000000p0"
The code in the main pane shows:
float sgn(float u)
...
if ((double)u > 0.0) {
...
### Additional Information :
Quick solution would be appreciated.
### Steps To Reproduce :
C code of sgn.c :
/*@
ensures A: \result == 1.0 || \result == 0.0 || \result == -1.0 ;
*/
float sgn(float u)
{
float p; /* return value */
if (u > 0.0) {
p = 1.0;
} else if (u < 0.0) {
p = -1.0;
} else {
p = 0.0;
}
return p;
}
1. Run:
frama-c-gui sgn.c
2. Select the post-condition
3. In context menu - Prove property by WP
(When the three "float" strings in the above code are changed to "double", the tool works fine, no error is reported.)https://git.frama-c.com/pub/frama-c/-/issues/349sigsetjmp and siglongjmp in setjmp.h2021-02-22T12:59:58Zmantis-gitlab-migrationsigsetjmp and siglongjmp in setjmp.hID0002135:
**This issue was created automatically from Mantis Issue 2135. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002135:
**This issue was created automatically from Mantis Issue 2135. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002135 | Frama-C | Kernel > libc | public | 2015-06-25 | 2017-05-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mansour | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
Hello,
This patch adds the function prototypes of sigsetjmp and siglongjmp to the header setjmp.h.
The type definition of sigjmp_buf is like jmp_buf but one character longer.
## Attachments
- [frama-c-sigsetjmp.patch](/uploads/c11c75898be46a528d848476dc1e271b/frama-c-sigsetjmp.patch)https://git.frama-c.com/pub/frama-c/-/issues/350"loop assigns" clause ignored in presence of "for"-prefixed clauses2021-04-15T09:27:13ZJochen Burghardt"loop assigns" clause ignored in presence of "for"-prefixed clausesID0002298:
**This issue was created automatically from Mantis Issue 2298. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002298:
**This issue was created automatically from Mantis Issue 2298. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002298 | Frama-C | Plug-in > wp | public | 2017-05-08 | 2017-05-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp beh.c" on the attached program fails to prove ensures clause "x01" and assertion "x10". When the two clauses prefixed by "for five" are removed from the loop invariant, everything is proven (except ensures clause "x02", which is about behavior "five").
Apparently, the two "for five" clauses (in fact, the first of them alone does) make Frama-c ignore the following "loop assigns x06" clause.
If the two "for five" clauses are moved below the "loop assigns x06" clause, an internal error is raised (output see "Additional information" below). For this reason, I set the Severity to "crash".
### Additional Information :
Frama-C's output for the internal error:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing beh.c (with preprocessing)
[wp] failure: At most one loop assigns can be associated to a behavior
[kernel] Current source was: beh.c:11
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 568, characters 30-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 15-16
Called from file "src/plugins/wp/wpAnnot.ml", line 855, characters 14-43
Called from file "list.ml", line 84, characters 24-34
Called from file "hashtbl.ml", line 200, characters 23-35
Called from file "hashtbl.ml", line 204, characters 12-33
Called from file "src/kernel_services/ast_data/annotations.ml", line 499, characters 4-187
Called from file "src/plugins/wp/wpAnnot.ml", line 865, characters 4-46
Called from file "src/plugins/wp/wpAnnot.ml", line 1015, characters 36-62
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/wpAnnot.ml", line 1023, characters 2-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1094, characters 15-41
Called from file "src/plugins/wp/wpAnnot.ml", line 1273, characters 14-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1274, characters 9-22
Called from file "src/plugins/wp/wpAnnot.ml", line 1363, characters 2-47
Called from file "map.ml", line 168, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
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
## Attachments
- [beh.c](/uploads/76212e7a4f3bee138c94f155a5d71946/beh.c)
- [beh2.c](/uploads/649046670c48074897a180a4e2785cc5/beh2.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/351Some ACSL mathematical functions crash WP2021-04-15T09:25:54Zmantis-gitlab-migrationSome ACSL mathematical functions crash WPID0002299:
**This issue was created automatically from Mantis Issue 2299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002299:
**This issue was created automatically from Mantis Issue 2299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002299 | Frama-C | Plug-in > wp | public | 2017-05-10 | 2017-05-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boyer | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | VirtualBox (Host Win7) | **OS** | Ubuntu | **OS Version** | 16.04.2 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Some of the mathematical functions enumerated in http://frama-c.com/download/acsl.pdf, p24 are not correctly supported by Frama-c. For instance, the keywords \pow, \cos and \sin are recognized at parsing and supported by EVA whereas an error is reported for WP (builtin functions are not defined) followed by an internal error.
### Additional Information :
Console message:
[kernel] Parsing .opam/4.04.0/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing ex.c (with preprocessing)
[wp] Running WP plugin...
[wp] warning: Missing RTE guards
[wp] user error: Builtin \round_error(float32) not defined
[wp] failure: Logic '\round_error' undefined
==================================================================================
Crash report:
Current source was: :0
The full backtrace is:
Raised at file "hashtbl.ml", line 440, characters 17-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Plug-in wp aborted: internal error.
Reverting to previous state.
[...]
### Steps To Reproduce :
Using Example 2.9, p25 from the ACSL manual:
/*@ requires \abs(\exact(x)) <= 0x1p-5;
@ requires \round_error(x) <= 0x1p-20;
@ ensures \abs(\exact(\result)-\cos(\exact(x))) <= 0x1p-24;
@ ensures \round_error(\result) <= \round_error(x) + 0x3p-24;
@*/
float cosine(float x) {
return 1.0f - x * x * 0.5f;
}
Then:
frama-c-gui -wp cosine.c
## Attachments
- [wp-bug.zip](/uploads/df0c5400fe8b77153075db0a5a303098/wp-bug.zip)Loïc CorrensonLoïc Correnson