frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:27:13Zhttps://git.frama-c.com/pub/frama-c/-/issues/896ACSL comment rejected in function template2021-02-22T13:27:13ZJochen BurghardtACSL comment rejected in function templateID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002048 | Frama-Clang | Plug-in > clang | public | 2015-01-12 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 430.cpp (external front-end)
inadequate comment at 430.cpp:5:2
If line 2 is commented-in and line 3 is commented-out, the error message disappears.
## Attachments
- [430.cpp](/uploads/fb7c1b9a2c7e740eb0e5c7200661ce99/430.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/865bitwise negation of uint introduces "-1" in Alt-Ergo obligation2021-02-22T13:41:06ZJochen Burghardtbitwise negation of uint introduces "-1" in Alt-Ergo obligationID0002023:
**This issue was created automatically from Mantis Issue 2023. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002023:
**This issue was created automatically from Mantis Issue 2023. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002023 | Frama-Clang | Documentation > ACSL | public | 2014-12-08 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
For the assertion in line 3 of the attached file "198.c", Frama-c generates the following proof obligation for Alt-Ergo: "goal foo_assert: forall i : int. is_uint32(i) -> ((-1) = i)". However, axiom "is_uint32_def" in line 430 of file "foo_assert_Alt-Ergo.mlw" says: "is_uint32(x) -> (0 <= x)", while "0 <= -1" is false (and unprovable as an own goal by Alt-Ergo).
As a consequence, there exists no (satisfiable) precondition "requires p(i)" that could be added as contract of "foo()" such that the assertion in line 3 becomes satisfiable, since "forall i : int. p(i) -> is_uint32(i) -> ((-1) = i)" implies "forall i : int. p(i) -> is_uint32(-1)". For example, requiring "i == 0xffffffffu" doesn't make line 3 provable, nor does any similar equation.
## Attachments
- [198.c](/uploads/43894779f84ecb85c5bbca9c5d4f60c5/198.c)
- [foo_assert_Alt-Ergo.mlw](/uploads/2d9028c59b5be767e57c7919eccb4d8b/foo_assert_Alt-Ergo.mlw)
- [198a.c](/uploads/387d28aa89210ab23bd7de97f80871b9/198a.c)
- [2compl.txt](/uploads/5886d302a5d8d0deae8deb56309ab3fe/2compl.txt)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/903can't compare pointer and reference for equality in contract2021-02-22T13:14:31ZJochen Burghardtcan't compare pointer and reference for equality in contractID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002060 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 441.cpp (external front-end)
441.cpp:2:22: invalid implicit conversion
441.cpp:2:22: unknown type comparison for the operator ==
Now output intermediate result
When line 2 is commented out, the comparison in C++ code in line 3 is accepted.
## Attachments
- [441.cpp](/uploads/da2cc8f3623d5563d069827341da0b18/441.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2641can't parse __int1282023-05-16T06:53:28ZYurii Rashkovskiican't parse __int128<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Expect this to be processed:
```c
__int128 i;
```
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Get a syntax error:
```
syntax error:
Location: between <unknown> and 1:9, before or at token: v
1 __int128 v;
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 26
- Plug-in used: WP
- OS name: macOS
- OS version: 13.1
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/179Can't use e-acsl on a dynamic library containing all the instrumentations2023-03-22T03:49:51Zmantis-gitlab-migrationCan't use e-acsl on a dynamic library containing all the instrumentationsID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002422 | Frama-C | Plug-in > E-ACSL | public | 2019-01-22 | 2019-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.19 Ocaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 19-Potassium | **Fixed in Version** | - |
### Description :
Hi !
main.c contains the entry point : the main function and is not instrumented by frama-c
it calls instrumented func.c (e-acsl.func.c containing the __e_acsl_memory_init call) compiled as a dynamic library libe-acsl.func.so
then the e-acsl code segfault at
e_acsl_segment_tracking.h:815
### Additional Information :
Why the hell am I doing this ? :)
Contiki-NG is an IoT OS. It can be build as a firmware for several IoT devices, as a ELF for Linux x86/x86_64, and as a shared library loaded by the Java Cooja network simulator (with some JNI).
Before experimenting with dlopen in C and JNI in Java, which is going to fail because of the __executable_start symbol at ./share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h:47
(this will the subject of another future post)
I would like to be able, as a first step, to use a e-acsl instrumented dynamic library used by a non-instrumented program (containing main or not).
I am open to a solution that eventually needs some change inside the C E-ACSL code.
### Steps To Reproduce :
$ make
rm -vf *.*o ./loader ./main *e-acsl*
frama-c -main func -variadic-no-translation -machdep gcc_x86_64 -c11 -cpp-extra-args="-std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64" -no-frama-c-stdlib func.c -e-acsl-prepare -rte -warn-signed-overflow -warn-unsigned-overflow -warn-signed-downcast -warn-unsigned-downcast -rte-div -rte-float-to-int -rte-mem -rte-pointer-call -rte-shift -rte-no-trivial-annotations -then -e-acsl -e-acsl-full-mmodel -then-last -print -ocode e-acsl.func.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing func.c (with preprocessing)
[rte] annotating function __bswap_16
[rte] annotating function __bswap_32
[rte] annotating function __bswap_64
[rte] annotating function __uint16_identity
[rte] annotating function __uint32_identity
[rte] annotating function __uint64_identity
[rte] annotating function func
[e-acsl] beginning translation.
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap16, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap32, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap64, generating default assigns from the prototype
[kernel:annot:missing-spec] /usr/include/stdio.h:332: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
gcc -shared -fPIC -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_STACK_SIZE=32 -DE_ACSL_HEAP_SIZE=128 -std=c99 -m64 -O0 -g -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jean/local-frama-c/share/frama-c/e-acsl/ -o libe-acsl.func.so e-acsl.func.c /home/jean/local-frama-c/share/frama-c/e-acsl/e_acsl_rtl.c /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-dlmalloc.a /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-gmp.a -lm
gcc -o main main.c -L. -le-acsl.func
LD_LIBRARY_PATH=:./ ./main
Segmentation fault
make: *** [Makefile:11: e-acsl-main-shared] Error 139
## Attachments
- [e-acsl-is-fun.tar](/uploads/c1c5ac773627666455f1b0a93e66da53/e-acsl-is-fun.tar)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/898catching a superclass causes crash2021-02-22T13:14:26ZJochen Burghardtcatching a superclass causes crashID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002051 | Frama-Clang | Plug-in > clang | public | 2015-01-15 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
[fclang] failure: Did not find struct for mangled class name _Z9Underflow
[kernel] Current source was: 432.cpp:6
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_link.ml", line 71, characters 36-53
Called from file "src/lib/FCSet.ml", line 332, characters 37-58
Called from file "src/frama-clang/convert_link.ml", line 86, characters 16-112
Called from file "src/frama-clang/convert_link.ml", line 104, characters 16-62
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert_link.ml", line 102, characters 12-142
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2046, characters 15-31
Called from file "cil/src/cil.ml", line 3095, characters 5-86
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 3255, characters 16-40
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3484, characters 14-39
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3446, characters 5-91
Called from file "cil/src/cil.ml", line 3538, characters 16-38
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 2130, characters 24-57
Called from file "cil/src/cil.ml", line 3532, characters 5-53
Called from file "cil/src/cil.ml", line 6151, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5741, characters 3-30
Called from file "cil/src/cil.ml", line 6152, characters 2-420
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 6185, characters 7-84
Called from file "src/kernel/file.ml", line 1803, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1880, characters 2-36
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
The problem remains if some member variable (e.g. "int x;") is added to the body of class "Matherr" in line 2 or/and the body of class "Underflow" in line 3.
The problem disappears if either:
(1) the definition of "Underflow" in line 3 is deleted,
(2) the definition of "foo" in line 5-10 is deleted,
(3) "Matherr" is changed to "Underflow" in the catch statement in line 8, or
(4) "public" is changed to "private" in line 3.
## Attachments
- [432.cpp](/uploads/c3a89685372790a4946ec88f8e54c293/432.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/660CLASSNAME::PREDICATENAME not recognized as predicate (or even as term)2021-02-22T13:39:56ZJochen BurghardtCLASSNAME::PREDICATENAME not recognized as predicate (or even as term)ID0001944:
**This issue was created automatically from Mantis Issue 1944. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001944:
**This issue was created automatically from Mantis Issue 1944. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001944 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-04-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
113.cpp:13:28: expecting a term or predicate
113.cpp:13:28: the term is not a predicate
Now output intermediate result
Note that the 2nd message claims a term while the 1st denies a term; no message should appear.
If the prefix "Queue::" is omitted in line 10 before "IsValid", no message is issued, while "unknown identifier 'IsValid'" should be reported.
If the definition of Queue() and its contract are moved inside the class, no message is issued, which is ok.
Probably related to issue #1606.
## Attachments
- [113.cpp](/uploads/4926913e5616dc5c301dabd76eac5c74/113.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/885constructor overloading resolution with templates causes dubious "contract me...2021-02-22T13:27:09ZJochen Burghardtconstructor overloading resolution with templates causes dubious "contract merge" warningID0002043:
**This issue was created automatically from Mantis Issue 2043. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002043:
**This issue was created automatically from Mantis Issue 2043. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002043 | Frama-Clang | Plug-in > clang | public | 2015-01-05 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 426.cpp" produces the output:
Now output intermediate result
426.cpp:5:[kernel] warning: found two contracts. Merging them
[wp] Running WP plugin...
The warning remains if
(1) the contract in line 7 is activated, or
(2) the contract in line 11 is deactivated.
The warning disappears if
(3) lines 4-5 are deleted,
(4) line 8 is deleted, or
(5) "char" is changed to "int" in line 13.
Even if the warning is printed, the proof obligation for the constructor call in line 13 seems to be correct, viz.:
(* ---------------------------------------------------------- *)
(* --- Instance of 'Pre-condition (file 426.cpp, line 4) in '_ZN7complexIcEEC1vci'' in 'main' at call '_ZN7complexIcEEC1vci' (file 426.cpp, line 13)
--- *)
(* ---------------------------------------------------------- *)
goal main_call__ZN7complexIcEEC1vci_pre:
forall i : int.
forall t : int farray.
(i <= 6) ->
linked(t) ->
is_sint32(i) ->
(1 = i)
So it is not clear which contracts are merged. Possibly this is a revival of issue #1611. However, it could also indicate that the contract in line 4 is merged with the (empty) contract of the constructor in line 8 (since the warning disappears when line 8 is removed) - which would be wrong in general.
## Attachments
- [426.cpp](/uploads/83b16ec11a724e4803101543fe3e06de/426.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/851Declaration order of static class member2021-02-22T13:13:26ZJens GerlachDeclaration order of static class memberID0001950:
**This issue was created automatically from Mantis Issue 1950. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001950:
**This issue was created automatically from Mantis Issue 1950. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001950 | Frama-Clang | Plug-in > clang | public | 2014-11-02 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | high | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following file contains two classes A and B that contain a single static variable count.
A::count is declared at the beginning of class A. Everything is fine.
B::count, however, is defined at the end of class B. Here Frama-Clang complains.
problem209.cpp:26:[fclang] failure: Unknown global variable B::count
### Additional Information :
Note, the problem does not occur, when B::count is a non-static member.
## Attachments
- [problem209.cpp](/uploads/12b2d0b16ba9d25bf52bd8af599cf33c/problem209.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/640declarations of static variable of class type in function body causes crash2021-03-29T17:24:55ZJochen Burghardtdeclarations of static variable of class type in function body causes crashID0002001:
**This issue was created automatically from Mantis Issue 2001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002001:
**This issue was created automatically from Mantis Issue 2001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002001 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
161.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 161.cpp:3
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 317, characters 18-77
Called from file "src/frama-clang/convert_acsl.ml", line 303, characters 13-52
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 272, characters 4-30
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 385, characters 13-38
Called from file "src/frama-clang/convert_acsl.ml", line 363, characters 11-42
Called from file "src/frama-clang/convert_acsl.ml", line 586, characters 14-40
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1179, characters 18-70
Called from file "src/frama-clang/convert.ml", line 1275, characters 20-46
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1265, characters 17-40
Called from file "src/frama-clang/convert.ml", line 2151, characters 21-44
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The problem disappears if
(1) the "static" is deleted in line 5, or
(2) "cls" is changed to "int" in line 5.
Could be related to #1997, since the crash messages agree. I dind't check the full call stack, however.
## Attachments
- [173.cpp](/uploads/bc77682336214d038cb4267b460d0df8/173.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/872different error messages for "0<x" and "0<x<9" when x is of class type2021-02-22T13:13:50ZJochen Burghardtdifferent error messages for "0<x" and "0<x<9" when x is of class typeID0002007:
**This issue was created automatically from Mantis Issue 2007. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002007:
**This issue was created automatically from Mantis Issue 2007. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002007 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Output of "frama-c -wp 185.cpp" in its current version:
185.cpp:4:24: comparison of incompatible types
Now output intermediate result
185.cpp:4:[kernel] user error: comparison of incompatible types: struct _Z1X and ℤ in annotation.
[kernel] user error: skipping file "185.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
Output of the same command after deleting "< 9" (or, alternatively, deleting "0 <") in line 4:
185.cpp:4:20: comparison of incompatible types
185.cpp:4:20: expecting a term or predicate
185.cpp:4:20: expecting a predicate
Now output intermediate result
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
While both behaviors of Frama-C are ok, their difference (in particular not running / running the Wp plugin) could indicate a bug.
## Attachments
- [185.cpp](/uploads/b1c887234898b1febb2313938115a12a/185.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/866"do"-loop with body interspersed with "case" labels of surrounding "switch" n...2021-02-22T13:26:56ZJochen Burghardt"do"-loop with body interspersed with "case" labels of surrounding "switch" not parsedID0001994:
**This issue was created automatically from Mantis Issue 1994. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001994:
**This issue was created automatically from Mantis Issue 1994. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001994 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Unsupported Statement:
DefaultStmt 0x2caf430 <158.cpp:6:2, col:15>
`-UnaryOperator 0x2c64b68 <col:12, col:15> 'int' postfix '++'
`-DeclRefExpr 0x2c64b40 <col:12> 'int' lvalue Var 0x2c649a0 'sum' 'int'
Aborting
The program has been boiled down from that an exercise in Stroustrup's C++ book, see attached file "stroustrup_06_06_15.cpp" for full example.
## Attachments
- [158.cpp](/uploads/7f019adb35c3e1fa16d757db41c9f50c/158.cpp)
- [stroustrup_06_06_15.cpp](/uploads/420758addbd603cbf270e95b7f67b154/stroustrup_06_06_15.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/883"ensures" clause of function template not supplied to Alt-Ergo2021-02-22T13:27:02ZJochen Burghardt"ensures" clause of function template not supplied to Alt-ErgoID0002034:
**This issue was created automatically from Mantis Issue 2034. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002034:
**This issue was created automatically from Mantis Issue 2034. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002034 | Frama-Clang | Plug-in > clang | public | 2014-12-15 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 411.cpp" generates, from the "assert" in line 12, an unprovable obligation (for Alt-Ergo), viz: "goal main_assert: forall i : int. is_sint32(i) -> (1 = i)", see line 570 of file "main_assert_Alt-Ergo.mlw".
If the function "nop" is made a non-template function (by uncommenting the typedef in line 4, and commenting-out the "template<class T>" prefix in line 7), the obligation reads "goal main_assert: forall i : int. (2 = (2 * i)) -> is_sint32(i) -> (1 = i)", and is proven without problems by Alt-Ergo.
## Attachments
- [411.cpp](/uploads/f4d3734df967c73ae7c415efd8c5d1de/411.cpp)
- [main_assert_Alt-Ergo.mlw](/uploads/13ed07ef6485c5aa5d0eafa5599fabbf/main_assert_Alt-Ergo.mlw)
- [411a.cpp](/uploads/0ffcaa8993e4cb1ec8e78eb5d2774ac2/411a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/859enum types in contract cause syntax error2021-02-22T13:26:57ZJochen Burghardtenum types in contract cause syntax errorID0001982:
**This issue was created automatically from Mantis Issue 1982. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001982:
**This issue was created automatically from Mantis Issue 1982. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001982 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
144.cpp:4:22: keyword 'keyword -> enum' encountered when parsing a type
Now output intermediate result
The message disappears if the file is renamed to "144.c".
## Attachments
- [144.cpp](/uploads/cfc01750842b55273e7a3094dc5cba83/144.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/833error message "unknown identifier 'xxx'" causes Frama-C to forget previous mo...2021-02-22T14:01:54ZJochen Burghardterror message "unknown identifier 'xxx'" causes Frama-C to forget previous more severe errorsID0002033:
**This issue was created automatically from Mantis Issue 2033. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002033:
**This issue was created automatically from Mantis Issue 2033. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002033 | Frama-Clang | Plug-in > clang | public | 2014-12-15 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In its current form (cf. issue #2032), the complete output of "frama-c -wp 405.cpp" looks like:
Now output intermediate result
405.cpp:6:[kernel] user error: Cannot find field salary
[kernel] user error: skipping file "405.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
However, if a non-declared variable (e.g. "xxx") is added to the "assigns" clause in line 5, the subsequent call to the wp plugin is no longer suppressed; the complete output then looks:
405.cpp:5:26: unknown identifier 'xxx'
Now output intermediate result
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
If there is some Frama-C-internal variable holding the severity of
errors detected so far, the "Cannot find field salary" error seems to
set it to a high level (thus suppressing the wp call), which is ok;
however the "unknown identifier 'xxx'" seems to lower that level again
(thus re-enabling the wp call), which is probably not ok.
## Attachments
- [405.cpp](/uploads/fe7b7b538990b1a71e7de87d63e0922a/405.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/906exception identifier from catch() statement unknown in contracts, but not in ...2021-02-22T13:28:04ZJochen Burghardtexception identifier from catch() statement unknown in contracts, but not in codeID0002071:
**This issue was created automatically from Mantis Issue 2071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002071:
**This issue was created automatically from Mantis Issue 2071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002071 | Frama-Clang | Plug-in > clang | public | 2015-02-02 | 2015-02-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 447.cpp (external front-end)
447.cpp:6:17: unknown identifier 'e'
Now output intermediate result
The message disappears if the "assert" in line 6 is deactivated.
## Attachments
- [447.cpp](/uploads/25b6f25f7846390e808821adc8820019/447.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/845Frama-C-clang does not unfold typedef2021-02-22T14:02:14ZJens GerlachFrama-C-clang does not unfold typedefID0001805:
**This issue was created automatically from Mantis Issue 1805. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001805:
**This issue was created automatically from Mantis Issue 1805. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001805 | Frama-Clang | Kernel | public | 2014-06-12 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When Frama-Clang analyses the following code example
struct A
{
int n;
};
typedef struct A B;
/*@
requires \valid(b);
assigns \nothing;
ensures \result == b->n;
*/
int foo(B* b)
{
return b->n;
}
then it complains
problem207.cpp:12:29: expecting a struct with field
problem207.cpp:12:29: type is not a pointer type
### Steps To Reproduce :
The source code of the example is available under acslplusplus/C++Examples/Problems/problem207.cpp
It was analysed with the following command line:
frama-c.byte -cxx-clang-command="framaCIRGen" -wp problem207.cppVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/850Frama-Clang does allow access to private fields within annotations2021-02-22T13:13:24ZJens GerlachFrama-Clang does allow access to private fields within annotationsID0001791:
**This issue was created automatically from Mantis Issue 1791. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001791:
**This issue was created automatically from Mantis Issue 1791. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001791 | Frama-Clang | Kernel | public | 2014-05-30 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following example shows that the private field A::i can be accessed in an annotation.
In my opinion the access rules in annotations should be the same as for code.
struct A
{
private:
int i;
public:
explicit A(int k) : i(k) {}
/*@
assigns \nothing;
ensures \result == i;
*/
int get() const
{
return i;
}
};
int foo(const A& a)
{
int b = a.get();
//@ assert b == a.i;
// Frama-Clang allows access to private field of A
// a.i cannot be accessed here because it is private
// this is recognized by Frama-Clang
// int c = a.i;
return b;
}Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/863how to specify equality of references, rather than of values, in contract?2021-02-22T13:13:38ZJochen Burghardthow to specify equality of references, rather than of values, in contract?ID0001990:
**This issue was created automatically from Mantis Issue 1990. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001990:
**This issue was created automatically from Mantis Issue 1990. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001990 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The contract of the function "fst" in line 4 of the attached program intends to specify that "fst(ppp)" returns a reference to "ppp.xxx".
However, it is interpreted by Frama-C as specifying that "fst(ppp)" and "ppp.xxx" have the same value. As a consequence, the assertion in line 10 cannot be proven; the generated obligation essentially amounts to "t_2[a_1] = t_2[a] -> 222 = t_2[a_1 <- 222][a]"; cf. the attached .mlw file. If the precondition would state reference equality (i.e. "a_1 = a") instead of value equality (i.e. "t_2[a_1] = t_2[a]"), the goal would follow trivially.
Frama-C's interpretation is not a bug, but is perfectly valid.
However, the question arises how the intended meaning (i.e. reference equality) could be formalized in the contract. Maybe another equality operator ( named e.g. "===") should be introduced into ACSL++ for this purpose.
## Attachments
- [152.cpp](/uploads/ae9fb734c8266aae29f014361aee8f4f/152.cpp)
- [_Z3bar_assert_Alt-Ergo.mlw](/uploads/f53057cf4583330c0dba0cd5ac99de4f/_Z3bar_assert_Alt-Ergo.mlw)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/290How to use the "Callers ..." context menu item2021-02-22T12:58:22Zmantis-gitlab-migrationHow to use the "Callers ..." context menu itemID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001431 | Frama-C | Graphical User Interface | public | 2013-05-27 | 2018-01-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Pardon the ignorance, but I couldn't find this on the manual...
I have a program where, after parsing, some warnings of this form are emitted:
"Calling undeclared function __builtin_swap32. Old style K&R code?"
I know there is a missing source file somewhere in my project, but I'd like to know who is calling these functions (since they are never directly called in my code). So I right-click on the function prototype on the GUI, and the last button in the context menu is "Callers ...". If I click on it, the "Launching analysis" window is displayed, with no indication of which analysis to choose.
I suppose the analysis I'd like is "Syntactic callgraph". So I choose it, without customizing any options, click Execute, but nothing changes. The "Callers ..." button is always visible when right-clicking the function declaration.
I noticed that if I choose the "Users" analysis, when right-clicking afterwards there is no more "Callers ..." button on the context menu, but I fail to see how any of the new options (e.g. Dependencies) could help me identify the function callers.
Is there a simpler way, other than by manually parsing the DOT file (the produced graph is too large for me to visually inspect it), to obtain information about function callers?Andre MaronezeAndre Maroneze