frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T14:02:26Zhttps://git.frama-c.com/pub/frama-c/-/issues/974Command line arguments (argc/argv) are not marked as valid2021-02-22T14:02:26ZArvid JakobssonCommand line arguments (argc/argv) are not marked as validID0001831:
**This issue was created automatically from Mantis Issue 1831. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001831:
**This issue was created automatically from Mantis Issue 1831. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001831 | Frama-C | Plug-in > E-ACSL | public | 2014-07-11 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 Neon-20140301 |
### Description :
See attached file for example. I have a fix coming for this.
## Attachments
- [bug-main-args.c](/uploads/60e1cc41c3422294c74dc182831652eb/bug-main-args.c)https://git.frama-c.com/pub/frama-c/-/issues/975Global variables are not marked as initialized2021-02-22T13:16:21ZArvid JakobssonGlobal variables are not marked as initializedID0001818:
**This issue was created automatically from Mantis Issue 1818. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001818:
**This issue was created automatically from Mantis Issue 1818. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001818 | Frama-C | Plug-in > E-ACSL | public | 2014-06-25 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **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 Neon-20140301 |
### Description :
Frama-C Git: b71d80efb3808c286f1a2f17dbf54bc3909824d0
E-ACSL Git: 19aea9a2202efc99fe3e268551e559358aa95751
Example:
int a = 0, b;
int main(void) {
int *p = &a, *q = &b;
/*@assert \initialized(&b) ; */
/*@assert \initialized(q) ; */
/*@assert \initialized(p) ; */
}
Both a and b should be marked as initialized in the generated __e_acsl_memory_init, but this is not the case:
void __e_acsl_memory_init(void)
{
__store_block((void *)(& a),sizeof(int));
__store_block((void *)(& b),sizeof(int));
return;
}https://git.frama-c.com/pub/frama-c/-/issues/976Instrumentation of statements with labels are not inserted at the correct loc...2021-02-22T13:28:15ZArvid JakobssonInstrumentation of statements with labels are not inserted at the correct locationID0001717:
**This issue was created automatically from Mantis Issue 1717. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001717:
**This issue was created automatically from Mantis Issue 1717. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001717 | Frama-C | Plug-in > E-ACSL | public | 2014-03-25 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 Neon-20140301 |
### Description :
The assertion on line 8 in the attached program fails since the call to __full_init is placed before the label on line 8, instead of after.
### Steps To Reproduce :
Frama-c run with the following parameters:
-machdep x86_64 -e-acsl bug-annotation-after-label.c -then-on e-acsl -print -ocode bug-annotation-after-label.gen.c
Compiled with the following flags:
export SHARE=`frama-c -print-share-path`
gcc -g -O0 -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o bug-annotation-after-label.c.out $SHARE/e-acsl/e_acsl.c $SHARE/e-acsl/memory_model/e_acsl_bittree.c $SHARE/e-acsl/memory_model/e_acsl_mmodel.c bug-annotation-after-label.gen.c -lgmp
## Attachments
- [bug-annotation-after-label.c](/uploads/9078d3eadf2e0e2badb8ef00c461a609/bug-annotation-after-label.c)https://git.frama-c.com/pub/frama-c/-/issues/977Dynamically allocated variables in body of while without break are not instru...2021-02-22T13:41:16ZArvid JakobssonDynamically allocated variables in body of while without break are not instrumentedID0001716:
**This issue was created automatically from Mantis Issue 1716. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001716:
**This issue was created automatically from Mantis Issue 1716. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001716 | Frama-C | Plug-in > E-ACSL | public | 2014-03-25 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 Neon-20140301 |
### Description :
The assertion on line 14 of the attached program fails even though p is a valid pointer at this point. However if the break on line 12 is uncommented, the assertion passes.
### Steps To Reproduce :
Frama-c run with the following parameters:
-machdep x86_64 -e-acsl bug-while-without-break.c -then-on e-acsl -print -ocode bug-while-without-break.gen.c
Compiled with the following flags:
export SHARE=`frama-c -print-share-path`
gcc -g -O0 -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o bug-while-without-break.c.out $SHARE/e-acsl/e_acsl.c $SHARE/e-acsl/memory_model/e_acsl_bittree.c $SHARE/e-acsl/memory_model/e_acsl_mmodel.c bug-while-without-break.gen.c -lgmp
## Attachments
- [bug-while-without-break.c](/uploads/23356798828425f202746243f69640df/bug-while-without-break.c)https://git.frama-c.com/pub/frama-c/-/issues/978"[...]/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed." using full m...2021-02-22T13:16:25ZArvid Jakobsson"[...]/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed." using full memory model, asserting validty of local varID0001715:
**This issue was created automatically from Mantis Issue 1715. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001715:
**This issue was created automatically from Mantis Issue 1715. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001715 | Frama-C | Plug-in > E-ACSL | public | 2014-03-25 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 Neon-20140301 |
### Description :
The attached program fails with the following message:
bug-full-mmodel.gen.c.out: /home/arvidj/dev/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed.
Aborted (core dumped)
### Steps To Reproduce :
Frama-c run with the following parameters:
-machdep x86_64 -e-acsl -e-acsl-full-mmodel bug-full-mmodel.c -then-on e-acsl -print -ocode bug-full-mmodel.gen.c
Compiled with the following flags:
export SHARE=`frama-c -print-share-path`
gcc -g -O0 -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o $1.out $SHARE/e-acsl/e_acsl.c $SHARE/e-acsl/memory_model/e_acsl_bittree.c $SHARE/e-acsl/memory_model/e_acsl_mmodel.c $1 -lgmp
## Attachments
- [bug-full-mmodel.c](/uploads/53251ca7aba31593a1ed0c3dabab3075/bug-full-mmodel.c)https://git.frama-c.com/pub/frama-c/-/issues/979warning: E_ACSL function 'initialize' called with null pointer - seems to aff...2021-02-22T13:28:19Zmantis-gitlab-migrationwarning: E_ACSL function 'initialize' called with null pointer - seems to affect the behaviorID0001696:
**This issue was created automatically from Mantis Issue 1696. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001696:
**This issue was created automatically from Mantis Issue 1696. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001696 | Frama-C | Plug-in > E-ACSL | public | 2014-03-14 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The file cpt.c contains a function. cpt.c alone is instrumented with e-acsl.
Then the main.c file calls this instrumented function.
When running the obtained binary, it prints this warning.
### Steps To Reproduce :
Run the script run.me
## Attachments
- [initialize.tgz](/uploads/3516eca6c69b56db8aae1edcc4d8f0cf/initialize.tgz)
- [initialize.v2.tgz](/uploads/c5e7cdbd85e74b4058fc179e3e04ffad/initialize.v2.tgz)https://git.frama-c.com/pub/frama-c/-/issues/980A pointer can be reported as belonging to an adjacent memory blocks in the bi...2021-02-22T13:16:29ZArvid JakobssonA pointer can be reported as belonging to an adjacent memory blocks in the bittree memory modelID0001836:
**This issue was created automatically from Mantis Issue 1836. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001836:
**This issue was created automatically from Mantis Issue 1836. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001836 | Frama-C | Plug-in > E-ACSL | public | 2014-07-16 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
There is a one-off error in the calculation of to which block a pointer. The following series of calls to the memory model triggers it (but I've got no simple program example which reproduces the error).
struct _block bk1 = {.ptr = 1, .size = 1};
__add_element(&bk1);
assert(__get_cont((void*)0) == NULL);
assert(__get_cont((void*)1) == &bk2);
assert(__get_cont((void*)2) == NULL); // will report 2 as belonging to bk1.
The offending line in e_acsl_bittree.c is:
else if((size_t)ptr <= tmp->leaf->size + tmp->addr)
where the comparison is strict and another clause should be added to handle the case of empty structs.https://git.frama-c.com/pub/frama-c/-/issues/981Impossible to compile the eacsl produced source2021-02-22T13:16:32Zmantis-gitlab-migrationImpossible to compile the eacsl produced sourceID0001695:
**This issue was created automatically from Mantis Issue 1695. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001695:
**This issue was created automatically from Mantis Issue 1695. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001695 | Frama-C | Plug-in > E-ACSL | public | 2014-03-14 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
This code is generated. It is compilable.
However when instrumented on a part of the code, gcc is not anymore able to compile it:
/tmp/cc3Hv08h.o: In function `__e_acsl_memory_init':
test4.c:(.text+0x43c): undefined reference to `__fc_stdout'
/tmp/cc3Hv08h.o: In function `main':
test4.c:(.text+0x52b): undefined reference to `__fc_stdout'
collect2: error: ld returned 1 exit status
Same behavior when applied on all the code.
### Steps To Reproduce :
Run the run.me script.
## Attachments
- [fc_stdout_gcc_error.tgz](/uploads/7442c231eee4ad08ed5f66893e8ea8fa/fc_stdout_gcc_error.tgz)
- [fc_stdout_gcc_error.v2.tgz](/uploads/e8ac870c04b639f8bbf1d03047fdce7d/fc_stdout_gcc_error.v2.tgz)https://git.frama-c.com/pub/frama-c/-/issues/982Wrong localisation of not yet supported constructs2023-10-09T13:44:38ZJulien SignolesWrong localisation of not yet supported constructsID0001692:
**This issue was created automatically from Mantis Issue 1692. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001692:
**This issue was created automatically from Mantis Issue 1692. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001692 | Frama-C | Plug-in > E-ACSL | public | 2014-03-13 | 2014-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | AMD 64 | **OS** | Linux | **OS Version** | Ubuntu |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
===== t.c =====
int main(void) {
//@ assert 2 >> 2 == 0;
return 1;
}
===========
$ frama-c -e-acsl t.c
t.c:1:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
Ignoring annotation.
The warning should be located at line 2, not at line 1.
### Additional Information :
Reported by P.-L. Garoche on Frama-C discuss.https://git.frama-c.com/pub/frama-c/-/issues/986Jessie crashes on incorrectly declared malloc2021-04-15T09:16:55Zmantis-gitlab-migrationJessie crashes on incorrectly declared mallocID0001913:
**This issue was created automatically from Mantis Issue 1913. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001913:
**This issue was created automatically from Mantis Issue 1913. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001913 | Frama-C | Plug-in > jessie | public | 2014-08-24 | 2014-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kornevgen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Linux localhost 3.10.7-gentoo-r1 | **OS** | Gentoo Linux | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
student@localhost ~/acslbyex/07/01 $ frama-c -jessie x.c
[kernel] preprocessing with "i686-pc-linux-gnu-gcc -C -E -I. -dD x.c"
x.c:18:[kernel] warning: Calling undeclared function malloc. Old style K&R code?
[jessie] Starting Jessie translation
x.c:16:[kernel] warning: Neither code nor specification for function malloc, generating default assigns from the prototype
[kernel] Current source was: x.c:18
The full backtrace is:
Called from file "src/kernel/ast_info.ml", line 394, characters 19-43
Called from file "interp.ml", line 1816, characters 22-50
Called from file "interp.ml", line 1953, characters 17-30
Called from file "list.ml", line 62, characters 22-25
Called from file "interp.ml", line 2119, characters 36-66
Called from file "interp.ml", line 2568, characters 40-71
Called from file "list.ml", line 62, characters 22-25
Called from file "interp.ml", line 2701, characters 27-66
Called from file "register.ml", line 176, characters 16-32
Called from file "register.ml", line 327, characters 6-12
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 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Unexpected error (File "src/kernel/ast_info.ml", line 391, characters 11-17: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
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
- [x.c](/uploads/3d6cd7ee3ca8cbb3127c4f9a880843f6/x.c)
- [frama-c-journal.ml](/uploads/edb37f80189e27784fbfbbdef1ca7588/frama-c-journal.ml)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/987Use of axioms in axiomatic specification is not supported2021-02-22T13:16:42Zmantis-gitlab-migrationUse of axioms in axiomatic specification is not supportedID0001858:
**This issue was created automatically from Mantis Issue 1858. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001858:
**This issue was created automatically from Mantis Issue 1858. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001858 | Frama-Clang | Plug-in > clang | public | 2014-07-25 | 2014-08-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | fvedrine | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | ubuntu 14.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
As soon as an axiom is written inside an axiomatic specification frama-c complains: problem309.cpp:5:9: axiom foo_1should be declared inside an axiomatic.
However this works in c.
### Additional Information :
The problem309.c file can also be found in the acslplusplus repository.
### Steps To Reproduce :
frama-c-gui.byte -wp -rte -pp-annot -no-unicode problem309.cpp
## Attachments
- [problem309.cpp](/uploads/22b08fde2d4fe63f6d5f560958e94f6e/problem309.cpp)https://git.frama-c.com/pub/frama-c/-/issues/988Static attribute can not be accessed2021-02-22T13:16:43Zmantis-gitlab-migrationStatic attribute can not be accessedID0001820:
**This issue was created automatically from Mantis Issue 1820. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001820:
**This issue was created automatically from Mantis Issue 1820. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001820 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2014-08-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | ubuntu 14.04 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Static attribute of a different object of the same class can not be accessed.
The error does not occur if the "static" is removed or the attribute belongs to the same object.
## Attachments
- [problem301.cpp](/uploads/f09f5c71368b0d5c21384fc7df9f087a/problem301.cpp)https://git.frama-c.com/pub/frama-c/-/issues/989Crash in the case of multiple pragma statements2021-02-22T14:02:27Zmantis-gitlab-migrationCrash in the case of multiple pragma statementsID0001906:
**This issue was created automatically from Mantis Issue 1906. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001906:
**This issue was created automatically from Mantis Issue 1906. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001906 | Frama-C | Plug-in > slicing | public | 2014-08-06 | 2014-08-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | zenscr | **Assigned To** | patrick | **Resolution** | duplicate |
| **Priority** | high | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Arch Linux | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the case of multiple pragma ctrl statements within the code to slice, the slicing plugin crashs immediately.
### Additional Information :
[kernel] preprocessing with "gcc -C -E -I. branches.c"
branches1-true.c:13:[kernel] warning: Body of function branches falls-through. Adding a return statement
[slicing] slicing requests in progress...
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
[value] computing for function __VERIFIER_nondet_int <- main.
Called from branches1-true.c:76.
branches1-true.c:76:[kernel] warning: Neither code nor specification for function __VERIFIER_nondet_int, generating default assigns from the prototype
[value] using specification for function __VERIFIER_nondet_int
[value] Done for function __VERIFIER_nondet_int
[value] computing for function __VERIFIER_nondet_int <- main.
Called from branches1-true.c:77.
[value] Done for function __VERIFIER_nondet_int
[value] computing for function __VERIFIER_nondet_int <- main.
Called from branches1-true.c:78.
[value] Done for function __VERIFIER_nondet_int
[value] computing for function __VERIFIER_nondet_int <- main.
Called from branches1-true.c:79.
[value] Done for function __VERIFIER_nondet_int
[value] computing for function __VERIFIER_nondet_int <- main.
Called from branches1-true.c:80.
[value] Done for function __VERIFIER_nondet_int
[value] computing for function __VERIFIER_nondet_int <- main.
Called from branches1-true.c:81.
[value] Done for function __VERIFIER_nondet_int
[value] computing for function branches <- main.
Called from branches1-true.c:90.
[value] computing for function __assert_fail <- branches <- main.
Called from branches1-true.c:66.
branches1-true.c:66:[kernel] warning: Neither code nor specification for function __assert_fail, generating default assigns from the prototype
[value] using specification for function __assert_fail
[value] Done for function __assert_fail
[value] computing for function __assert_fail <- branches <- main.
Called from branches1-true.c:55.
[value] Done for function __assert_fail
[value] computing for function __assert_fail <- branches <- main.
Called from branches1-true.c:59.
[value] Done for function __assert_fail
branches1-true.c:70:[value] Assertion got status invalid (stopping propagation).
[value] Recording results for branches
[value] Done for function branches
[value] computing for function exit <- main.
Called from branches1-true.c:93.
branches1-true.c:93:[kernel] warning: Neither code nor specification for function exit, generating default assigns from the prototype
[value] using specification for function exit
[value] Done for function exit
[value] Recording results for main
[value] done for function main
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[kernel] Current source was: branches.c:45
The full backtrace is:
Raised at file "src/logic/logic_interp.ml", line 820, characters 6-39
Called from file "list.ml", line 73, characters 12-15
Called from file "hashtbl.ml", line 188, characters 8-13
Called from file "hashtbl.ml", line 191, characters 4-19
Called from file "src/logic/annotations.ml", line 377, characters 4-116
Called from file "src/slicing/slicingCmds.ml", line 43, characters 27-33
Called from file "cil/src/cil.ml", line 1843, characters 15-31
Called from file "cil/src/cil.ml", line 2887, characters 5-86
Called from file "cil/src/cil.ml", line 1882, characters 13-16
Called from file "cil/src/cil.ml", line 3020, characters 16-40
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 2954, characters 33-42
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 2887, characters 5-86
Called from file "cil/src/cil.ml", line 1882, characters 13-16
Called from file "cil/src/cil.ml", line 3020, characters 16-40
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 2954, characters 11-20
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 2887, characters 5-86
Called from file "cil/src/cil.ml", line 1882, characters 13-16
Called from file "cil/src/cil.ml", line 3020, characters 16-40
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 2954, characters 33-42
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 2887, characters 5-86
Called from file "cil/src/cil.ml", line 1882, characters 13-16
Called from file "cil/src/cil.ml", line 3020, characters 16-40
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 2954, characters 11-20
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 2887, characters 5-86
Called from file "cil/src/cil.ml", line 1882, characters 13-16
Called from file "cil/src/cil.ml", line 3020, characters 16-40
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 3234, characters 14-39
Called from file "cil/src/cil.ml", line 1858, characters 21-41
Called from file "cil/src/cil.ml", line 3206, characters 5-91
Called from file "src/slicing/slicingCmds.ml", line 75, characters 11-62
Called from file "src/logic/logic_interp.ml", line 944, characters 9-44
Called from file "src/slicing/slicingCmds.ml", line 503, characters 4-260
Called from file "src/slicing/slicingCmds.ml", line 599, characters 31-64
Called from file "src/slicing/slicingCmds.ml", line 607, characters 13-274
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "src/slicing/slicingCmds.ml", line 595, characters 6-1023
Called from file "src/slicing/register.ml", line 1194, characters 4-54
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 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Unexpected error (File "src/logic/logic_interp.ml", line 820, characters 6-12: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
### Steps To Reproduce :
Using the attached program, execute Frama-C's slicing plugin as follows
frama-c branches.c -slice-pragma branches -then-on 'Slicing export' -print
## Attachments
- [branches.c](/uploads/4c5083da89954992376904645cffb7b7/branches.c)https://git.frama-c.com/pub/frama-c/-/issues/993Configure fails for GNU Make 4.02023-03-09T10:04:17Zmantis-gitlab-migrationConfigure fails for GNU Make 4.0ID0001903:
**This issue was created automatically from Mantis Issue 1903. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001903:
**This issue was created automatically from Mantis Issue 1903. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001903 | Frama-C | Kernel > configure | public | 2014-07-30 | 2014-08-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Julien_t | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Gnu/linux Debian | **OS Version** | Debian 3.14.12-1 |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
First I should probably say that I use opam to install frama-C.
The configure file test whether the Make version is greater than 3.81 but it check that major version is >= 3 (which is ok) and that minor version is >= 81, which is not the case for the version 4.0
### Additional Information :
test at line 2630 of the configure file should be modified.
### Steps To Reproduce :
./configure in an environment with version 4.0 of GNU Makehttps://git.frama-c.com/pub/frama-c/-/issues/994make version 4.0 is rejected2021-02-22T14:02:28Zmantis-gitlab-migrationmake version 4.0 is rejectedID0001574:
**This issue was created automatically from Mantis Issue 1574. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001574:
**This issue was created automatically from Mantis Issue 1574. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001574 | Frama-C | Kernel > configure | public | 2013-11-28 | 2014-08-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jowi24 | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
$./configure
configure: ******************
configure: * CONFIGURE MAKE *
configure: ******************
checking for make... make
make version is GNU Make 4.0:
configure: error: unsupported version; GNU Make version 3.81
or higher is required.
### Additional Information :
the following test in configure is buggy:
test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 -o "$MAKE_MINOR" -lt 81;https://git.frama-c.com/pub/frama-c/-/issues/99622446: unknown sizes of types and value initialization2021-02-22T14:02:04ZPascal Cuoq22446: unknown sizes of types and value initializationID0001416:
**This issue was created automatically from Mantis Issue 1416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001416:
**This issue was created automatically from Mantis Issue 1416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001416 | Frama-C | Plug-in > Eva | public | 2013-05-07 | 2014-07-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Commit 22446 transforms a crash when some types have unknown sizes into a clean exit, but there remains a problem with the test below:
Sending src/value/initial_state.ml
Transmitting file data .
Committed revision 22446.
~/ppc $ cat t.c
struct s;
struct larger {
struct s t[2];
int i;
} v;
int main(int c, char **v)
{
return 0;
}
~/ppc $ bin/toplevel.opt -val t.c
[kernel] warning: cannot load 5 plug-ins (incompatible with Fluorine-20130401+dev).
Aorai; Obfuscator; Report; Security_slicing;
Wp
[kernel] preprocessing with "gcc -C -E -I. t.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
t.c:6:[value] warning: during initialization of variable 'v', size of type 'struct s' cannot be
computed (abstract type 'struct s')
[value] Initial state computed
[value] Values of globals at initialization
[kernel] Current source was: t.c:6
The full backtrace is:
Raised at file "cil/src/cil.ml", line 4250, characters 40-64
Called from file "cil/src/cil.ml", line 4763, characters 17-35
Called from file "src/project/state_builder.ml", line 556, characters 17-22
Called from file "src/misc/bit_utils.ml", line 245, characters 37-66
Called from file "list.ml", line 86, characters 24-34
Called from file "src/misc/bit_utils.ml", line 242, characters 37-1023
Called from file "src/misc/bit_utils.ml", line 432, characters 4-58
Called from file "src/memory_state/offsetmap.ml", line 1726, characters 14-160
Called from file "src/memory_state/offsetmap.ml", line 424, characters 10-34
Called from file "format.ml", line 1166, characters 10-25
Called from file "format.ml", line 1166, characters 10-25
Called from file "src/lib/pretty_utils.ml", line 89, characters 2-121
Called from file "format.ml", line 1166, characters 10-25
Called from file "src/value/eval_funs.ml", line 317, characters 6-176
Called from file "src/value/eval_funs.ml", line 567, characters 11-40
Re-raised at file "src/value/eval_funs.ml", line 583, characters 47-50
Called from file "src/project/state_builder.ml", line 839, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 847, characters 15-18
Called from file "src/value/register.ml", line 82, characters 4-24
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Unexpected error (Cil.SizeOfError("abstract type 'struct s'", _)).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130401+dev.
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
~/ppc $https://git.frama-c.com/pub/frama-c/-/issues/1000Problem with _Bool(when casting to int or with ?:)2021-04-15T07:17:43Zmantis-gitlab-migrationProblem with _Bool(when casting to int or with ?:)ID0001847:
**This issue was created automatically from Mantis Issue 1847. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001847:
**This issue was created automatically from Mantis Issue 1847. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001847 | Frama-C | Plug-in > wp | public | 2014-07-21 | 2014-07-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davyg | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In this example the ensures seems to be impossible to prove whereas it should
be easy :
//@ensures (!\result) == (!x);
_Bool f(_Bool x) {
_Bool y;
return (y?x:x);
}
I put the bug in Wp category but it can be see as a framaC bug depending from where it comes from.
### Additional Information :
This must be due to the transformation of ?: into an if statement
with an int local variable which lead more or less to a function like
this that can't be proven :
//@ensures (!\result) == (!x);
_Bool g(_Bool x) {
int t = x;
return t;
}
This must be due to the lack of information about the cast.
I think that the transformation of ?: should use a _Bool temp
variable instead of an int. Or int cast should have a lemma like \forall _Bool x; (x != 0) <==> (((int) x) != 0);Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1001assigns crash on incorrect locations2021-04-15T08:29:05Zmantis-gitlab-migrationassigns crash on incorrect locationsID0001844:
**This issue was created automatically from Mantis Issue 1844. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001844:
**This issue was created automatically from Mantis Issue 1844. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001844 | Frama-C | Plug-in > wp | public | 2014-07-17 | 2014-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boulme | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux Ubuntu 14.04 LTS | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the file "crash_assigns.c",
an invalid assign clause makes wp crash with the message:
Current source was: crash_assigns.c:5
The full backtrace is:
Raised at file "hashtbl.ml", line 353, characters 18-27
Called from file "hashtbl.ml", line 361, characters 22-38
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
### Additional Information :
Replacing the invalid assigns clause with a valid one like
assigns t[0..9];
makes the pb disappear...
### Steps To Reproduce :
run frama-c-gui crash_assigns.c
and try to prove assigns clause using wp.
## Attachments
- [crash_assigns.c](/uploads/b195abe901a4302f8d3fab7fb4ce8458/crash_assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1002assigns clause appears unprovable2021-08-05T08:49:01ZJens Gerlachassigns clause appears unprovableID0001638:
**This issue was created automatically from Mantis Issue 1638. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001638:
**This issue was created automatically from Mantis Issue 1638. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001638 | Frama-C | Plug-in > wp | public | 2014-02-01 | 2014-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | urgent | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It appears that assigns clauses of functions that modify an array cannot be verified at all.
I attach a simple example of a function set_zero that sets all elements of an array to zero (file set_zero.c).
Attached is also an attempt to prove the assigns clause with Coq (see file wp0.script).
I do not see how from
0 <= n
0 < i
one can conclude
i <= n
Please, correct me if I am totally missing something.
### Additional Information :
Here is my proof attempt for the assigns clause:
Proof.
forward.
remember a_0 as a.
remember n_0 as n.
remember i_0 as i.
remember Mint_0 as M0.
remember Mint_1 as M1.
cut (i <= n).
auto with zarith.
assert(less_equal: 0 <= n).
assumption.
apply Zle_lt_or_eq in less_equal.
rewrite or_comm in less_equal.
destruct less_equal as [equal | less].
(* case equal *)
rewrite <- equal.
assert (~(i <= 0)).
auto with zarith.
contradict H7.
(* what now ? *)
Qed.
## Attachments
- [set_zero.c](/uploads/d5f6e570e7a4f9c0940b3c3d3b58509b/set_zero.c)
- [pb_assigns.c](/uploads/d4c0f6b7c5581fe712fd29c93c5cf800/pb_assigns.c) <- now verified.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1007Erreur de linkage de librarie ocaml avec des fichier objets2021-02-22T13:17:09Zmantis-gitlab-migrationErreur de linkage de librarie ocaml avec des fichier objetsID0001733:
**This issue was created automatically from Mantis Issue 1733. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001733:
**This issue was created automatically from Mantis Issue 1733. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001733 | Frama-C | Kernel > Makefile | public | 2014-04-05 | 2014-07-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | zuy | **Assigned To** | signoles | **Resolution** | unable to reproduce |
| **Priority** | urgent | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Lorsqu'on fait un makefile pour son plugin en linkant une librairie (cma, cmxa) et non des fichiers objets (cmo) à ce plugin, on se retrouve avec une erreur de pré-reference : Forward reference to Llvm in file.
### Additional Information :
Lorsque le makefile souhaite packager l'ensemble des fichiers objets de frama-c avec ceux du plugins on se retrouve face à un problème lorsque le plugin en question souhaite se linker avec non pas une fichier objet mais une bibliothèque de fichier objet. Autrement dit au lieu de charger un cmo, il souhaite charger un cma.
Il semblerait que le make de frama-c n'ai pas prévu cette possibilité.
L'option -pack de ocamlc qui attend uniquement des fichiers objets pour en créer un nouveau; semble ne pas gérer l'arrivé d'une librairie contenant plusieurs fichier objet parmis les fichiers donnés0.
Dans l'exemple ci-dessous avec llvm.cma.
Plusieurs tentatives tendent à montrer que le problème se trouve là. Des tentatives en utilisant des -for-packs uniquement avant la création de la lib partagé (cmxs) ont échouées ainsi que d'autres pour transformer les fichiers objets (en packageant les objet du frama-c et ceux du plugin) en une librairie cma et l'utiliser pour faire le fichier partagé. Voilà les pistes que j'ai suivi et que j'ai surement mal mené.
Est ce réellement un bug ou une mauvaise utilisation du système de makefile mis en place ?
Exemple:
sh -c 'for f in "$@"; do if test -e $f; then chmod u+w $f; fi done' chmod_rw ./.depend
ocamldep.opt -slash \
-I . -I "/usr/local/lib/frama-c" \
lv.ml llvmRegister.ml llvmPrinter.ml llvmMain.ml lv.mli llvmRegister.mli llvmPrinter.mli llvmMain.mli \
\
> ./.depend
touch FCLlvm_DEP
chmod a-w ./.depend
ocamlc.opt -c -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm lv.ml
File "lv.ml", line 9, characters 6-13:
Warning 26: unused variable f32x4_t.
File "lv.ml", line 10, characters 6-13:
Warning 26: unused variable builder.
File "lv.ml", line 15, characters 6-11:
Warning 26: unused variable d64_t.
ocamlc.opt -c -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm llvmRegister.ml
ocamlc.opt -c -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm llvmPrinter.ml
ocamlc.opt -c -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm llvmMain.ml
ocamlc.opt -o FCLlvm.cmo -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm -pack \
llvm.cma \
./lv.cmo ./llvmRegister.cmo ./llvmPrinter.cmo ./llvmMain.cmo
File "_none_", line 1:
Error: Forward reference to Llvm in file ./lv.cmo
make: *** [FCLlvm.cmo] Erreur 2
### Steps To Reproduce :
Créer un plugin nécessitant une librairie caml. Ici l'exemple concerne le byte code mais l'erreur se produit pour le natif aussi. Faire le make appelant le Makefile.dynamic de frama-c.
Puis faire une make.https://git.frama-c.com/pub/frama-c/-/issues/1016clause "n<9-1" normalized to "n-1<9"2021-02-22T13:17:26ZJochen Burghardtclause "n<9-1" normalized to "n-1<9"ID0001810:
**This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001810:
**This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001810 | Frama-Clang | Plug-in > clang | public | 2014-06-16 | 2014-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c-gui -wp -wp-rte 108.cpp -wp-out wp-out" on the attached program shows in the gui's normalized-code window the clause "requires 0 <= n-1 && n-1 < 9;" as translation of source line 5 ("requires 0 <= n < 9-1;").
The same error is found in alt-ergo's input file "_Z4push_assert_rte_index_bound_2.ergo". As a consequence, alt-ergo can't prove the index bound for line 9.
The error disappears if
* the file is renamed to "108.c",
* "9-1" is replaced by "9" in line 5.
The error appears unchanged if "n" is made a procedure parameter of "push".
## Attachments
- [108.cpp](/uploads/f07695abe8c21809455ab3b47fd664b3/108.cpp)
- [_Z4push_assert_rte_index_bound_2.ergo](/uploads/e6b954a9726185b9f5ecdbb9bd90990d/_Z4push_assert_rte_index_bound_2.ergo)
- [109.cpp](/uploads/6aac1934cfc40814903aafd21efbc26b/109.cpp)https://git.frama-c.com/pub/frama-c/-/issues/1017Frama-Clang fails to parse simple predicate2021-02-22T13:17:27ZJens GerlachFrama-Clang fails to parse simple predicateID0001808:
**This issue was created automatically from Mantis Issue 1808. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001808:
**This issue was created automatically from Mantis Issue 1808. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001808 | Frama-Clang | Plug-in > clang | public | 2014-06-13 | 2014-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
When Frama-Clang is called on the following code fragment
/*@
predicate IsValidRange(int* a, integer n) = (0 <= n) && \valid(a+(0.. n-1));
*/
void foo(int* a, int);
with the command line
frama-c -cpp-command 'gcc -C -E -nostdinc -I/opt/local/include -I/Users/jens/.opam/system/lib/frama-c/share/frama-c/libc' -cxx-clang-command="framaCIRGen" -cxx-demangling-full -wp -wp-rte -wp-out problem208.wp problem208.cpp
then the following error message occurs
Stack dump:
0. <eof> parser at end of file
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: skipping file "problem208.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
As far as I can see the problem is related to the predicate definition.
It is one of our simpler predicates in ACSL by Example.
### Steps To Reproduce :
The example is available also under acslplusplus/C++Examples/Problems/problem208.cpphttps://git.frama-c.com/pub/frama-c/-/issues/1018assigns, loop assigns and loop invariant2021-08-05T08:48:53ZVirgile Prevostoassigns, loop assigns and loop invariantID0001461:
**This issue was created automatically from Mantis Issue 1461. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001461:
**This issue was created automatically from Mantis Issue 1461. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001461 | Frama-C | Plug-in > wp | public | 2013-07-24 | 2014-06-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the following (admittedly contrived) example, the assigns of g is not proved by WP (in fact it is reduced to false by Qed), although it is correct from ACSL semantics: as long as the loop invariant states that x still has its old value, the fact that it is mentioned in the loop assigns should not impede its absence in the assigns.
--- test.c
```
int x;
/*@ assigns \nothing; */
int g() {
/*@ loop assigns i,x;
loop invariant x == \at(x,Pre);
*/
for (int i = 0; i<2; i++);
return x;
}
```
### Steps To Reproduce :
frama-c -wp test.cLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1019Assigns not respected in behaviors when using pointers to pointers2021-08-05T08:49:22Zmantis-gitlab-migrationAssigns not respected in behaviors when using pointers to pointersID0001812:
**This issue was created automatically from Mantis Issue 1812. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001812:
**This issue was created automatically from Mantis Issue 1812. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001812 | Frama-C | Plug-in > wp | public | 2014-06-16 | 2014-06-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Assigns defined in behaviors are not always respected. The example provided shows an assigns defined in complete behaviors that causes a different results than if defined outside the behaviors. The results are expected to be the same since the behaviors are complete.
### Steps To Reproduce :
Create file (attached: invalid.c):
```
/*@
@ requires \valid(a) && \valid(*a) && \separated(a, *a);
@ behavior all:
@ assumes \true;
@ assigns **a;
@ complete behaviors all;
@*/
void set_next_next(int **a){
**a = 0;
}
void main(){
int **a, *b, c;
b = &c;
a = &b;
pre_fct:
set_next_next(a);
//@ assert b == \at(b, pre_fct);
}
```
Run:
```
frama-c -cpp-command 'gcc -C -E' -wp invalid.c
```
Result:
Assertion in main does not validate.
By moving the assigns statement outside the behavior, the assertion is validated:
```
/*@
@ requires \valid(a) && \valid(*a) && \separated(a, *a);
@ assigns **a;
@ behavior all:
@ assumes \true;
@ complete behaviors all;
@*/
```
## Attachments
- [invalid.c](/uploads/3d4a401d6a5d55ab1cb43bcbb73e53c8/invalid.c)
- [valid.c](/uploads/a336506d1703a71e66da940fbdef2a11/valid.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1020syntax error for alt-ergo with memset spec2021-02-22T13:17:31Zmantis-gitlab-migrationsyntax error for alt-ergo with memset specID0001587:
**This issue was created automatically from Mantis Issue 1587. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001587:
**This issue was created automatically from Mantis Issue 1587. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001587 | Frama-C | Plug-in > wp | public | 2013-12-16 | 2014-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
When trying to prove the first loop invariant of this example, there is a message:
/tmp/wpd57f12.dir/typed/A_MemSet.ergo:10:[wp] user error:
Prover Alt-Ergo returns Failed
characters 6-106:typing error: syntax error
and neither the establishment nor the preservation can be proved.
### Additional Information :
Command line is :
frama-c -cpp-extra-args=-I`frama-c -print-share-path`/libc pb_wp.c -wp
## Attachments
- [pb_wp.c](/uploads/97bd3bebc043ed6808b7047aec5dd9d0/pb_wp.c)https://git.frama-c.com/pub/frama-c/-/issues/1021Frama-clang include problem with directory hierarchy2021-02-22T13:17:33ZJens GerlachFrama-clang include problem with directory hierarchyID0001797:
**This issue was created automatically from Mantis Issue 1797. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001797:
**This issue was created automatically from Mantis Issue 1797. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001797 | Frama-Clang | Plug-in > clang | public | 2014-06-04 | 2014-06-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached tar file contains a small directory hierarchy
problem206-dir
├── nonmutating
│ └── equal
│ ├── README
│ └── equal.c
└── typedefs.h
The file equal.c includes the file typedefs.h which is two layers up in the hierarchy.
When I call
frama-c.byte -cxx-clang-command="framaCIRGen -I../.." equal.c
then I receive the following error message
[kernel] preprocessing with "gcc -C -E -I. equal.c"
equal.c:2:20: fatal error: typedefs: No such file or directory
#include "typedefs"
^
compilation terminated.
[kernel] user error: failed to run: gcc -C -E -I. -o '/tmp/equal.c5f0bc4.i' 'equal.c'
you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".
[kernel] user error: skipping file "equal.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
I am particularly baffled by the kernels message to "use -cpp-command" because I thought this option is not to be used with frama-clang.
Also, the problem disappears when the header typedefs.h is only one level above equal.c.
(Of course, the command line has to be changed accordingly.)
The example can also be found in
acslplusplus/C++Examples/Problems/problem206-dir
## Attachments
- [problem206-dir.tar](/uploads/cca3489eeafcb5be7e26e3fdcc9308bb/problem206-dir.tar)https://git.frama-c.com/pub/frama-c/-/issues/1022double puzzle - precondition not proved using WP/Val plugin2021-02-22T13:17:35Zmantis-gitlab-migrationdouble puzzle - precondition not proved using WP/Val pluginID0001664:
**This issue was created automatically from Mantis Issue 1664. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001664:
**This issue was created automatically from Mantis Issue 1664. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001664 | Frama-C | Plug-in > Eva | public | 2014-02-28 | 2014-06-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
#include <stdio.h>
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int x = 0;
int main()
{
assert(x == (int)(double)x);
return 0;
}
### Additional Information :
[kernel] preprocessing with "gcc -C -E -I. -dD double_casting_puzzle.c"
[value] Analyzing an incomplete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
x ∈ [--..--]
[value] computing for function assert <- main.
Called from double_casting_puzzle.c:13.
[value] using specification for function assert
double_casting_puzzle.c:4:[value] Function assert: precondition got status unknown.
[value] Done for function assert
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
__retres ∈ {0}
### Steps To Reproduce :
frama-c -val double_casting_puzzle.c -pp-annot -lib-entryhttps://git.frama-c.com/pub/frama-c/-/issues/1024WP doesn't warn about volatile variables2021-04-15T07:10:32Zmantis-gitlab-migrationWP doesn't warn about volatile variablesID0001801:
**This issue was created automatically from Mantis Issue 1801. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001801:
**This issue was created automatically from Mantis Issue 1801. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001801 | Frama-C | Plug-in > wp | public | 2014-06-06 | 2014-06-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I noticed that WP doesn't handle volatile variables, which is not a problem, but the problem is that it proves properties about them without any warning at all, which a quiet embarrassing I suppose.
### Steps To Reproduce :
$ frama-c -wp-fct main test_volatile.c
volatile int v = 10;
//@ ensures \result == 10;
int main (void) {
int x = v;
//@ assert v == 10;
v = 3;
//@ assert v == 3;
return x;
}Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1025Cannot use quotes in comments in annotations2021-03-29T15:50:48Zmantis-gitlab-migrationCannot use quotes in comments in annotationsID0001800:
**This issue was created automatically from Mantis Issue 1800. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001800:
**This issue was created automatically from Mantis Issue 1800. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001800 | Frama-C | Kernel | public | 2014-06-05 | 2014-06-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using the //@ annotations, a comment at the end that has an unmatched ' or " causes the kernel to report an error.
### Steps To Reproduce :
create file comment_parse.c:
void f(){
//@assert \true;// Validates in 0'0"
}
Run:
frama-c -cpp-command 'gcc -C -E' -pp-annot comment_parse.c
Receive output:
[kernel] preprocessing with "gcc -C -E -dD comment_parse.c"
"comment_parse.c":5:[kernel] user error: Can't preprocess annotation: eof while parsing a char literal
Annotation will be kept as is
comment_parse.c:3:[kernel] user error: syntax error
[kernel] user error: skipping file "comment_parse.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
Removing the ' and " characters will cause no error to occur.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1026Signal -7 and then crashed.2021-02-22T13:47:19Zmantis-gitlab-migrationSignal -7 and then crashed.ID0001602:
**This issue was created automatically from Mantis Issue 1602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001602:
**This issue was created automatically from Mantis Issue 1602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001602 | Frama-C | Plug-in > wp | public | 2014-01-15 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | unable to reproduce |
| **Priority** | high | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
$ frama-c -wp -wp-rte test_frama.c -wp-fct=myFunc -wp-bhv=basic -main myFunc -lib-entry -wp-timeout=500
[kernel] preprocessing with "gcc -C -E -I. test_frama.c"
[wp] Running WP plugin...
[rte] annotating function myFunc
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_myFunc_basic_post : Failed
Error: Unix.SIGNAL -7
Any comments?
### Steps To Reproduce :
I used Alt-Ergo 0.95.2. Unfortunately, this code is somewhat complex and cannot disclose here although I would like to share.
## Attachments
- [ApLowAlm.mlw](/uploads/39c448b8eed5e0db531692fb99845956/ApLowAlm.mlw)https://git.frama-c.com/pub/frama-c/-/issues/1027Frama-C/WP does not warn about unsatisfied precondition2023-07-21T13:45:04ZJens GerlachFrama-C/WP does not warn about unsatisfied preconditionID0001678:
**This issue was created automatically from Mantis Issue 1678. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001678:
**This issue was created automatically from Mantis Issue 1678. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001678 | Frama-C | Plug-in > wp | public | 2014-03-07 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, OSX | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Here is the setup:
```c
/*@
requires 0 < a ;
assigns \nothing;
ensures 0 < \result < 10;
*/
int foo(int a);
/*@
assigns \nothing;
ensures 0 < \result < 30;
*/
int bar(int x)
{
int a = foo(1); // precondition satisfied
int b = foo(0); // precondition violated and recognized
int c = foo(x); // precondition not satisfied and not recognized
return a + b + c;
}
```
When I process this example with
frama-c-gui -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -no-unicode -wp-out ./out.wp
-wp-proof alt-ergo -wp-proof coq foo.c
then a green bullet appears next to the line
int c = foo(x); // precondition not satisfied and not recognized
However, it is unknown whether x satisfies the precondition "0 < x" of foo.
If, however, the lines are reverse like this
int c = foo(x);
int b = foo(0);
then both calls are correctly flagged as orange (yellow?)
### Additional Information :
The problem also appears in the release candidate for Neon.https://git.frama-c.com/pub/frama-c/-/issues/1029short int to float assertion not proved2021-02-22T14:02:32Zmantis-gitlab-migrationshort int to float assertion not provedID0001653:
**This issue was created automatically from Mantis Issue 1653. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001653:
**This issue was created automatically from Mantis Issue 1653. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001653 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Wonder why this assertion is not provable even though it is a valid one.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
float f = SHRT_MAX;
short int i = f;
assert(i == SHRT_MAX);
}
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte float_to_short_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD float_to_short_int_max_2.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (4ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (8ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknownhttps://git.frama-c.com/pub/frama-c/-/issues/1030int to double - assert not verified2021-02-22T14:02:32Zmantis-gitlab-migrationint to double - assert not verifiedID0001651:
**This issue was created automatically from Mantis Issue 1651. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001651:
**This issue was created automatically from Mantis Issue 1651. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001651 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
For this below program, the assert should be valid I think but the WP is not proving it.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
double f = INT_MAX;
int i = f;
assert(i == INT_MAX);
return 0;
}
### Additional Information :
The regular C assert was able to prove when I run the a.out after compiling the wrong (commenting the ACSL's assert).
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte double_to_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD double_to_int_max_2.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (4ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (12ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown (1s)https://git.frama-c.com/pub/frama-c/-/issues/1031WP: Assertion not proved -> conversion from float to int issue?2021-02-22T14:02:32Zmantis-gitlab-migrationWP: Assertion not proved -> conversion from float to int issue?ID0001655:
**This issue was created automatically from Mantis Issue 1655. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001655:
**This issue was created automatically from Mantis Issue 1655. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001655 | Frama-C | Plug-in > wp | public | 2014-02-27 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm using Frama-C for my course at UMD. Found it pretty helpful.
I tried this puzzle, but cannot get WP to prove the assertion, which is true.
I ran through the GDB and found that the value of i is INT_MIN, satisfying the assert.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
float f = INT_MAX;
int i = f;
assert(i == INT_MIN);
return 0;
}
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte float_to_int_assert.c
[kernel] preprocessing with "gcc -C -E -I. float_to_int_assert.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (8ms)
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (12ms)
[wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown
## Attachments
- [int_of_real_why3.diff](/uploads/3aadceb64f4a89ae445498f3e92952de/int_of_real_why3.diff)
- [floats_and_ints.diff](/uploads/b4984e6711b9343f82562f3dd284f08a/floats_and_ints.diff)https://git.frama-c.com/pub/frama-c/-/issues/1032WP - strcpy not proved2021-02-22T13:17:51Zmantis-gitlab-migrationWP - strcpy not provedID0001652:
**This issue was created automatically from Mantis Issue 1652. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001652:
**This issue was created automatically from Mantis Issue 1652. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001652 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | - | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I took the attached program from one of the WP tutorials but added the main function which calls strcpy. I wonder why the requires are not valid. I do not know what is wrong with my two strings in main.
### Steps To Reproduce :
[formal_verification]$ frama-c -pp-annot -wp -wp-rte -wp-proof why3:Z3,alt-ergo -wp-split -wp-model Typed+ref string_lib.c [kernel] preprocessing with "gcc -C -E -I. -dD string_lib.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] Collecting variable usage
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_ref_main_call_strcpy_pre_2_part1 : Valid [wp] [Qed] Goal typed_ref_main_call_strcpy_pre_2_part1 : Valid [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre : Unknown [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre_2_part2 : Unknown (Qed:4ms) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre_2_part2 : Unknown (Qed:4ms) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre : Unknown [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre_3 : Valid (24ms) (22) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre_3 : Valid (10ms)
## Attachments
- [string_lib.c](/uploads/83ca58d14714f50a83c5dbefcf99dec0/string_lib.c)https://git.frama-c.com/pub/frama-c/-/issues/1044Missing rte guard when assigning an unsigned int to an int2021-02-22T13:23:19ZJens GerlachMissing rte guard when assigning an unsigned int to an intID0001766:
**This issue was created automatically from Mantis Issue 1766. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001766:
**This issue was created automatically from Mantis Issue 1766. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001766 | Frama-C | Plug-in > RTE | public | 2014-04-30 | 2014-05-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | ubuntu 3.13 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following function assigns the unsigned int variable "a" to the int variable "b".
I do not see any generated rte assertions to guard this operation.
The C standard says in 6.3.1.3.3 about this kind of operation
Otherwise, the new type is signed and the value cannot be represented in it; either the result is
implementation-defined or an implementation-defined signal is raised.
On the other hand, for the operation involving "a" and "x", proper rte guards are generated.
/*@
requires \valid(x);
assigns *x;
*/
int f(unsigned int a, unsigned int* x)
{
*x = a + a;
int b = a;
return b;
}https://git.frama-c.com/pub/frama-c/-/issues/1045Unproven rte assertions for bit complement2023-10-09T13:44:38ZJens GerlachUnproven rte assertions for bit complementID0001769:
**This issue was created automatically from Mantis Issue 1769. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001769:
**This issue was created automatically from Mantis Issue 1769. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001769 | Frama-C | Plug-in > RTE | public | 2014-05-01 | 2014-05-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am struggling with unproven run time assertions in a some piece of code that heavily relies on bit operations.
In fact, I am not sure this an issue of the rte plug-in.
It is probably related to https://bts.frama-c.com/view.php?id=1750
which I submitted to the WP section.
However, I wonder if the rte plug-in could make the task of WP easier.
The attached file simply performs bitwise complement for various unsigned integer types.
For unsigned char and unsigned short the rte plugin generates unsigned_downcast assertion that
WP cannot discharge.
I understand that the promotion of the variable "a" to int is covered by the C standard.
On the other hand, the C standard says in 6.5.3.4 (4)
If the promoted type is an unsigned type, the expression ~E is equivalent to the maximum value
representable in that type minus E.
So, no overflow will occur.
### Steps To Reproduce :
I called the file with the following options
frama-c-gui.byte -cpp-command 'gcc -C -E -nostdinc -I/usr/local/share/frama-c/libc' -pp-annot -no-unicode -wp -warn-signed-downcast -warn-signed-overflow -warn-unsigned-downcast -warn-unsigned-overflow -wp-rte complement.c
## Attachments
- [complement.c](/uploads/5a515e096bc7eeb191a98c240d20e77e/complement.c)https://git.frama-c.com/pub/frama-c/-/issues/1114Compiling Wp-Coq library2021-02-22T13:28:53ZDillon ParienteCompiling Wp-Coq libraryID0001690:
**This issue was created automatically from Mantis Issue 1690. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001690:
**This issue was created automatically from Mantis Issue 1690. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001690 | Frama-C | Kernel > Makefile | public | 2014-03-13 | 2014-03-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Windows/Cygwin | **OS** | Win7 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
[STANCE]
In Frama-C Neon 20140301, when performing a 'make':
[...]
Compiling Wp-Coq Library
make[1] : on entre dans le répertoire « /frama-c-Neon-rc3/src/wp/share/coqwp »
coqc -R . -as "" BuiltIn.v
Don't know what to do with ./BuiltIn
Usage: coqtop <options>
...
It seems that in {-R . -as ""} the empty string is not managed as expected under Windows/Cygwin.
This topic was already discussed about the RC3.
This BTS record is open for traceability.
(Using coq 8.4pl3 with binaries pack for Windows)https://git.frama-c.com/pub/frama-c/-/issues/1131E-ACSL reports use of invalid pointer while in fact the pointer is valid2022-05-02T09:10:40ZDavid MentréE-ACSL reports use of invalid pointer while in fact the pointer is validID0001478:
**This issue was created automatically from Mantis Issue 1478. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001478:
**This issue was created automatically from Mantis Issue 1478. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001478 | Frama-C | Plug-in > E-ACSL | public | 2013-09-04 | 2014-03-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130601 |
### Description :
On attached program, E-ACSL reports use of invalid pointer:
"""
Precondition failed at line 7 in function loop.
The failing predicate is:
\valid(global_i_ptr).
"""
But in fact the pointer is valid.
This is checked by reading and executing the program, but also statically with WP and Value analysis.
The attached program is compiled with following script, replacing $1 with q7_invalid_under_eacsl.c.
"""
PATH=/usr/local/stow/frama-c-Fluorine-20130601/bin:$PATH
export PATH
eacsl_path=`frama-c -print-share-path`/e-acsl
frama-c \
-cpp-command 'gcc -C -E -I/usr/local/stow/frama-c-Fluorine-20130601/share/frama-c/libc -I SSI'\
-e-acsl \
$1 \
-then-on e-acsl -print -ocode a-e-acsl.c \
&& \
gcc -I$eacsl_path $eacsl_path/memory_model/e_acsl_bittree.c $eacsl_path/memory_model/e_acsl_mmodel.c $eacsl_path/e_acsl.c a-e-acsl.c
"""
## Attachments
- [q7_invalid_under_eacsl.c](/uploads/fc3279cdc60e5191500031773634387f/q7_invalid_under_eacsl.c)https://git.frama-c.com/pub/frama-c/-/issues/1133Very big integer constants2022-05-12T14:21:47ZJulien SignolesVery big integer constantsID0000745:
**This issue was created automatically from Mantis Issue 745. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000745:
**This issue was created automatically from Mantis Issue 745. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000745 | Frama-C | Kernel > ACSL implementation | public | 2011-03-04 | 2014-03-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Integer constants are de facto limited to int64 by Cil. Should use Big_int to accept any constant.
### Steps To Reproduce :
void main(void) {
/*@ assert 0xfffffffffffffffff == 0xfffffffffffffffff; */
}
$ frama-c a.c
a.c:1:[kernel] failure: Cannot represent on 64 bits the integer 0xfffffffffffffffffhttps://git.frama-c.com/pub/frama-c/-/issues/1134Too much type promotion for terms2021-02-22T13:20:54ZJulien SignolesToo much type promotion for termsID0000744:
**This issue was created automatically from Mantis Issue 744. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000744:
**This issue was created automatically from Mantis Issue 744. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000744 | Frama-C | Kernel > ACSL implementation | public | 2011-03-04 | 2014-03-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
on the above example, C typing rules should apply. Thus no logic term should be logic integer. Unfortunately, in the current implementation, all of them are integer.
void main(void) {
int x = 0, y = 0;
long z = 0L;
/*@ assert x == y; */ // x and y are promoted to integer; should be promoted to int instead
/*@ assert x == z; */ // x and z are promoted to integer. x should be promoted to long instead
}https://git.frama-c.com/pub/frama-c/-/issues/1135evaluation of && and || in term position2021-02-22T13:20:56ZJulien Signolesevaluation of && and || in term positionID0001072:
**This issue was created automatically from Mantis Issue 1072. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001072:
**This issue was created automatically from Mantis Issue 1072. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001072 | Frama-C | Plug-in > Eva | public | 2012-01-26 | 2014-03-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
=== bug.i ===
int main(void) {
int x = 0, y = 1;
/*@ assert (x || y) == y; */
/*@ assert (x && y) == x; */
return 0;
}
===============
julien@is006613:~/frama-c$ frama-c -val bug.i
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
[kernel] The full backtrace is:
Called from file "src/value/eval_logic.ml", line 237, characters 16-57
Called from file "src/value/eval_logic.ml", line 249, characters 30-39
Called from file "src/value/eval_logic.ml", line 224, characters 17-40
Called from file "src/value/eval_logic.ml", line 729, characters 31-57
Called from file "src/value/eval_logic.ml", line 58, characters 15-18
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval_logic.ml", line 56, characters 5-230
Called from file "src/value/eval_stmts.ml", line 955, characters 21-211
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval_stmts.ml", line 1069, characters 8-128
Called from file "cil/src/ext/dataflow.ml", line 305, characters 12-27
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 115, characters 14-37
Called from file "src/value/eval_funs.ml", line 442, characters 6-69
Called from file "src/value/eval_funs.ml", line 546, characters 11-44
Re-raised at file "src/value/eval_funs.ml", line 562, characters 47-50
Called from file "src/project/state_builder.ml", line 1068, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 1072, characters 15-18
Called from file "src/value/register.ml", line 46, characters 4-24
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 719, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Unexpected error (File "src/value/eval_exprs.ml", line 419, characters 6-12: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001+dev.
Note that a version and a backtrace alone often does not have 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/1136e-acsl translation: unexpected error2021-02-22T13:28:57Zmantis-gitlab-migratione-acsl translation: unexpected errorID0001634:
**This issue was created automatically from Mantis Issue 1634. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001634:
**This issue was created automatically from Mantis Issue 1634. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001634 | Frama-C | Plug-in > E-ACSL | public | 2014-01-27 | 2014-03-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ThomasJ | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Ubuntu | **OS Version** | 12.04 LTS |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I'm trying to create a E-ACSL code for ARM Processors. Therefore i use the arm-gcc instead of the usual gcc. Preprocessing works fine but the e-acsl translation fails.
journal.ml included in project.
### Additional Information :
[e-acsl] beginning translation.
[kernel] Current source was: System_XMC4500.c:347
The full backtrace is:
Called from file "error.ml", line 53, characters 4-7
Called from file "visit.ml", line 574, characters 6-55
Called from file "visit.ml", line 588, characters 3-41
Called from file "cil/src/cil.ml", line 2832, characters 5-52
Called from file "cil/src/cil.ml", line 2958, characters 14-21
Called from file "cil/src/cil.ml", line 1847, characters 21-41
Called from file "cil/src/cil.ml", line 2876, characters 5-86
Called from file "cil/src/cil.ml", line 1871, characters 13-16
Called from file "cil/src/cil.ml", line 3009, characters 16-40
Called from file "cil/src/cil.ml", line 1847, characters 21-41
Called from file "cil/src/cil.ml", line 3223, characters 14-39
Called from file "cil/src/cil.ml", line 1847, characters 21-41
Called from file "cil/src/cil.ml", line 3195, characters 5-91
Called from file "cil/src/cil.ml", line 3275, characters 16-38
Called from file "cil/src/cil.ml", line 1871, characters 13-16
Called from file "cil/src/cil.ml", line 1916, characters 24-57
Called from file "cil/src/cil.ml", line 3269, characters 5-53
Called from file "cil/src/cil.ml", line 5895, characters 17-37
Called from file "cil/src/cil.ml", line 5902, characters 3-20
Called from file "cil/src/cil.ml", line 1847, characters 21-41
Called from file "src/kernel/file.ml", line 1948, characters 14-42
Called from file "src/kernel/file.ml", line 1977, characters 2-48
Called from file "main.ml", line 152, characters 12-55
Called from file "src/project/project.ml", line 345, characters 12-15
Called from file "src/project/project.ml", line 350, characters 17-22
Re-raised at file "src/project/project.ml", line 350, characters 56-57
Called from file "main.ml", line 146, characters 5-572
Called from file "src/project/project.ml", line 345, characters 12-15
Called from file "src/project/project.ml", line 350, characters 17-22
Re-raised at file "src/project/project.ml", line 350, characters 56-57
Called from file "main.ml", line 116, characters 12-34
Called from file "src/project/state_builder.ml", line 556, characters 17-22
Called from file "src/kernel/journal.ml", line 434, characters 21-32
Re-raised at file "src/kernel/journal.ml", line 449, characters 18-19
Called from file "main.ml", line 199, characters 11-56
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 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Unexpected error (File "pre_analysis.ml", line 694, characters 18-24: Assertion failed).
### Steps To Reproduce :
frama-c -journal-enable -journal-name blink4500 -e-acsl -cpp-command 'arm-linux-gnueabi-gcc-4.6 -C -E -DUC_ID=4503 -mfloat-abi=softfp -Wall -std=gnu99 -fmessage-length=0 -mcpu=cortex-m4 -mfpu=fpv4-sp-d16 -mthumb -g3 -gdwarf-2 -I. -IXMC4500 -I/usr/arm-linux-gnueabi/include/' Blinky.c LED.c System_XMC4500.c -then-on e-acsl -print -ocode monitored_arm.c
## Attachments
- [Blinky_ARM.zip](/uploads/d3777e008da2b3ee3882101d9950e0f8/Blinky_ARM.zip)
- [preprocessed.i](/uploads/a17ecac1bec1d4a4b5d8ece091b8625a/preprocessed.i)https://git.frama-c.com/pub/frama-c/-/issues/1138Statically reject programs that jump over VLA declaration.2021-03-29T15:47:00ZPascal CuoqStatically reject programs that jump over VLA declaration.ID0001712:
**This issue was created automatically from Mantis Issue 1712. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001712:
**This issue was created automatically from Mantis Issue 1712. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001712 | Frama-C | Kernel | public | 2014-03-24 | 2014-03-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following program contains UB (jumping over the declaration of t):
int main(int c, char **v){
goto label;
{
char t[c];
f(t);
label:
return t[0];
}
}
It would be nice it was rejected by the front-end.
This is not absolutely necessary, in the sense that Frama-C has historically focused on bugs not found by compilers and neglected those that could be found reliably by compilers (both GCC and Clang reject the program). But it would be nice.
### Steps To Reproduce :
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:4:[kernel] warning: Variable-sized local variable t
t.c:5:[kernel] warning: Calling undeclared function f. Old style K&R code?
/* Generated by Frama-C */
/* compiler builtin:
void *__builtin_alloca(unsigned int); */
extern int ( /* missing proto */ f)(char *x_0);
int main(int c, char **v)
{
int __retres;
goto label;
{
char *t;
unsigned int __lengthoft;
{
/*sequence*/
__lengthoft = (unsigned int)c;
t = (char *)__builtin_alloca(sizeof(*t) * __lengthoft);
}
f(t);
label: ;
__retres = (int)*(t + 0);
return __retres;
}
}Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1141Unbound value Base.get_varinfo (Neon)2021-02-22T13:21:03ZDillon ParienteUnbound value Base.get_varinfo (Neon)ID0001691:
**This issue was created automatically from Mantis Issue 1691. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001691:
**This issue was created automatically from Mantis Issue 1691. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001691 | Frama-C | Plug-in > Eva | public | 2014-03-13 | 2014-03-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | yakobowski | **Resolution** | no change required |
| **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 :
[STANCE]
Base.get_varinfo disappeared from the API.
What can replace it?https://git.frama-c.com/pub/frama-c/-/issues/1142Configure script's autolocation of local OcamlGraph breaks out of tree builds2021-03-29T13:54:27Zmantis-gitlab-migrationConfigure script's autolocation of local OcamlGraph breaks out of tree buildsID0001454:
**This issue was created automatically from Mantis Issue 1454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001454:
**This issue was created automatically from Mantis Issue 1454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001454 | Frama-C | Kernel > configure | public | 2013-07-08 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sstewartgallus | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I prefer to build my software packages out of tree. My personal arrangement is to have one sources directory, and one builds directory. I would then run my packages configure script inside a subdirectory of the sources directory specifically for that package, and build from there.
It is great that a version of OcamlGraph is distributed with Frama-C but unfortunately the configure script can only find it if the current directory is the source directory, and this breaks out of tree builds.
The problematic line in configure.in appears to be:
AC_CHECK_FILE($OCAMLGRAPH_LOCAL,OCAMLGRAPH_EXISTS=yes)
This line could probable be fixed in multiple ways. There's probably an autoconf macro for looking for a file in the source directory that's better than AC_CHECK_FILE, or one could define OCAMLGRAPH_LOCAL to use the invocation of ./configure to locate the directory it's located in (which would be something like ("$(cd $(dirname $0) && pwd)/ocamlgraph".)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1145Develop strategies to efficiently run WP with different ATP and Coq2021-09-21T13:22:14ZJens GerlachDevelop strategies to efficiently run WP with different ATP and CoqID0001699:
**This issue was created automatically from Mantis Issue 1699. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001699:
**This issue was created automatically from Mantis Issue 1699. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001699 | Frama-C | Plug-in > wp | public | 2014-03-14 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This strategy should be controlled by a view options that also take into account how many processes are available.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1146Generate footprint from reads clauses of logic declarations2021-08-05T09:15:35ZJens GerlachGenerate footprint from reads clauses of logic declarationsID0001693:
**This issue was created automatically from Mantis Issue 1693. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001693:
**This issue was created automatically from Mantis Issue 1693. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001693 | Frama-C | Plug-in > wp | public | 2014-03-13 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | high | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It would be helpful if the reads clause of an axiomatic definition would be
used to generate additional hypothesis for coq proofs.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1147Generate proof obligation for drivers when driver instantiate a logic acsl de...2023-07-21T13:21:41ZJens GerlachGenerate proof obligation for drivers when driver instantiate a logic acsl declarationID0001694:
**This issue was created automatically from Mantis Issue 1694. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001694:
**This issue was created automatically from Mantis Issue 1694. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001694 | Frama-C | Plug-in > wp | public | 2014-03-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This would be helpful for proving (in coq) that a model of an ACSL logic function actually exists.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1152strange warning "postcondition got status invalid"2022-08-29T14:56:07ZJochen Burghardtstrange warning "postcondition got status invalid"ID0001369:
**This issue was created automatically from Mantis Issue 1369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001369:
**This issue was created automatically from Mantis Issue 1369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001369 | Frama-C | Plug-in > Eva | public | 2013-02-15 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Running "frama-c -val ftest.c" on the attached program produces a "[value] Function foo: postcondition got status invalid" in line 6, although the ensures clause looks quite reasonable. (I don't understand the notion of a "postcondition status": shouldn't the postconditions of a function be satisfied automatically if all its preconditions are?) The warning disappears if the ensures clause in line 5 is removed or an appropriate function body (e.g. the one commented out at the end of line 6) is added.
## Attachments
- [ftest.c](/uploads/0c897adefea2db69ea93598a19ce19bc/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/1153Error message could be better2022-09-20T08:59:24ZJulien SignolesError message could be betterID0001352:
**This issue was created automatically from Mantis Issue 1352. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001352:
**This issue was created automatically from Mantis Issue 1352. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001352 | Frama-C | Kernel | public | 2013-01-28 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
On the following incorrect file:
=== bug.i ===
int main(void) {
int t /* [5] missing */ = { 1, 2, 3, 4, 5 };
}
=============
frama-c reports:
$ frama-c bug.i
bug.i:2:[kernel] failure: doInit: unexpected NEXT_INIT for int
[kernel] user error: skipping file "tests/fusy/lval.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
This message is not very helpful...https://git.frama-c.com/pub/frama-c/-/issues/1155Frama-C should not honor -save if when it aborts2021-02-22T13:21:26ZBoris YakobowskiFrama-C should not honor -save if when it abortsID0001388:
**This issue was created automatically from Mantis Issue 1388. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001388:
**This issue was created automatically from Mantis Issue 1388. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001388 | Frama-C | Kernel | public | 2013-04-11 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | low | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
This is problematic because it complicates the use of Makefile. Typical pattern:
Makefile:
foo.sav: $(DEPS)
frama-c <options> -save $@
make foo.sav
<Frama-C aborts on an user or something else>
<change something to your configuration/plugin/etc>
make foo.sav
make: `foo.sav' is up to date.
Frama-c not creating a foo.sav on the first invocation would solve the problem. What do you think? Are there some good cases when dumping partial saves is useful? In fact, what do those saves contain, since at least one plugin failed. Is the internal state really consistent?https://git.frama-c.com/pub/frama-c/-/issues/1157Logging just enough information for failed pre-conditions2022-10-03T08:07:55ZPascal CuoqLogging just enough information for failed pre-conditionsID0001415:
**This issue was created automatically from Mantis Issue 1415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001415:
**This issue was created automatically from Mantis Issue 1415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001415 | Frama-C | Plug-in > Eva | public | 2013-05-03 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
There was a bit of a discussion over an analysis made on an example provided by a StackOverflow user:
http://stackoverflow.com/a/16356519/139746
The current message is:
.../libc/string.h:54:[value] Function memcpy: precondition got status invalid.
That is a bit frustrating. The localization of the call to memcpy() can be found just above in the log:
[value] computing for function memcpy <- main.
Called from mem.c:13.
but the exact nature of the detected issue is only printed as a reference to libc/string.h, a file that the user did not even provide emself.
There are at least two solutions suggested by the discussion:
- annotate the libc preconditions with nice labels, and when a pre-condition fails, print any label it may have, or
- print the entire ACSL pre-condition that failed, including any label it may have.https://git.frama-c.com/pub/frama-c/-/issues/1159AST integrity check failure with kernel-debug2021-02-22T13:21:33ZGuillaume PetiotAST integrity check failure with kernel-debugID0001440:
**This issue was created automatically from Mantis Issue 1440. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001440:
**This issue was created automatically from Mantis Issue 1440. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001440 | Frama-C | Kernel | public | 2013-06-03 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | guillaume-petiot | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
a.c:6:[kernel] failure: [AST Integrity Check] initial AST
Following functions and variables are present in global tables but not in AST:
Functions:
__builtin_va_arg(158) __builtin_stdarg_start(162) __builtin_next_arg(310)
__builtin_expect(350) __builtin_va_start(357) __builtin_va_arg(541)
__builtin_stdarg_start(545) __builtin_next_arg(693) __builtin_expect(733)
__builtin_va_start(740)
Fatal error: exception Log.AbortFatal("kernel")
Raised at file "src/kernel/log.ml", line 523, characters 30-31
Called from file "src/kernel/log.ml", line 517, characters 9-16
Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
Called from file "src/kernel/file.ml", line 717, characters 8-413
Called from file "cil/src/cil.ml", line 5887, characters 7-84
Called from file "src/kernel/file.ml", line 1449, characters 36-147
Called from file "src/kernel/file.ml", line 2020, characters 4-27
Called from file "src/kernel/ast.ml", line 103, characters 2-28
Called from file "src/kernel/ast.ml", line 114, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Re-raised at file "src/kernel/cmdline.ml", line 226, characters 14-17
Called from file "src/kernel/boot.ml", line 66, characters 2-355
### Steps To Reproduce :
$ frama-c a.c -check -kernel-debug 1
## Attachments
- [a.c](/uploads/206b5b7c43303793821044d13c13132b/a.c)https://git.frama-c.com/pub/frama-c/-/issues/1160The post-conditon of [gets] got status invalid2021-02-22T13:21:34Zmantis-gitlab-migrationThe post-conditon of [gets] got status invalidID0001435:
**This issue was created automatically from Mantis Issue 1435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001435:
**This issue was created automatically from Mantis Issue 1435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001435 | Frama-C | Plug-in > Eva | public | 2013-05-30 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
When using 'gets' from Frama-C include files, the value analysis gives :
:/usr/local/share/frama-c/libc/stdio.h:225:
[value] Function gets: postcondition got status invalid.
I don't really understand how Value can say something about the post-condition of an undefined function, but anyway, then I get "This call never terminates".
It seems that a fix is to add :
@ assigns \result \from s, *__fc_stdin;
but maybe it could be more correct to also add :
@ assigns *__fc_stdin \from *__fc_stdin ;
### Additional Information :
Example :
$ frama-c -val toto.c -cpp-extra-args="-I`frama-c -print-path`/libc -nostdinc"
#include <stdio.h>
void main () {
char line[100];
char * p = gets (line);
}https://git.frama-c.com/pub/frama-c/-/issues/1164frama-c.toplevel not working anymore2022-09-28T12:04:10Zmantis-gitlab-migrationframa-c.toplevel not working anymoreID0001441:
**This issue was created automatically from Mantis Issue 1441. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001441:
**This issue was created automatically from Mantis Issue 1441. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001441 | Frama-C | Kernel | public | 2013-06-04 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I already reported this in the mailing list, and I understand that you don't have time to fix this, but I open an issue anyway to store some information.
I noticed two different problems :
(1) $ make top
report conflicts (warning 31) about ocaml and frama-c modules Subst and Config.
1a/ Subst seems not used anymore : could be removed ?
1b/ maybe Config could be renamed ?
(2) $ bin/toplevel.top -h
shows frama-c help. So it seems that this is not an ocaml toplevel.
At the end of toplevel_boot.ml, replacing :
< Cmdline.catch_toplevel_run ...
by
> !Db.Toplevel.run (fun () -> ())
and compiling again gives back an ocaml toplevel
(but still not fully working because of the module problem (1)).https://git.frama-c.com/pub/frama-c/-/issues/1165Incorrect printing of designated initializers2022-10-27T21:14:36ZBoris YakobowskiIncorrect printing of designated initializersID0001457:
**This issue was created automatically from Mantis Issue 1457. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001457:
**This issue was created automatically from Mantis Issue 1457. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001457 | Frama-C | Kernel | public | 2013-07-11 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The code below is incorrectly pretty-printed back, although the internal AST seems to be correct.
int t[10] = { [4 ... 6] = 5};
int u[10] = { [4] = 3};
void main() {
}https://git.frama-c.com/pub/frama-c/-/issues/1173ACSL label LoopEntry not handled by WP2022-10-06T14:57:24Zmantis-gitlab-migrationACSL label LoopEntry not handled by WPID0001353:
**This issue was created automatically from Mantis Issue 1353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001353:
**This issue was created automatically from Mantis Issue 1353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001353 | Frama-C | Plug-in > wp | public | 2013-01-30 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
As said in the title, the ACSL label LoopEntry seems to be not handled by WP but it is accepted by the kernel.
Using the -wp-warnings option I got warnings like :
- Warning: Generalization of un-labeled values
Reason: Some labels may escape the control flow
but it took me some time to understand the problem.
In the example below, changing LoopEntry by L in the loop invariant makes it work.
BTW, in the example below, it doesn't work either when removing the first (c++;) statement !
### Additional Information :
int G;
//@ requires G == 0; ensures G == 0;
void f (int c) {
c++;
L: //@ loop invariant G == \at (G, LoopEntry);
while (c) c++;
}https://git.frama-c.com/pub/frama-c/-/issues/1177Journalisation of -no-unicode option2022-10-21T09:15:36ZPatrick BaudinJournalisation of -no-unicode optionID0001451:
**This issue was created automatically from Mantis Issue 1451. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001451:
**This issue was created automatically from Mantis Issue 1451. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001451 | Frama-C | Kernel | public | 2013-07-04 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The -no-unicode option is a execution mode for frama-c printers.
That option is not used as a debug option by the end-user of Frama-C.
So, it would be nice if that option could be journalized.
Anyway, adding -no-unicode option to the -load-script command does no effect.
Unicode are still pretty printed.https://git.frama-c.com/pub/frama-c/-/issues/1178uninitialized value can be passed through pointer, through return, but not t...2021-02-22T13:22:22ZJochen Burghardtuninitialized value can be passed through pointer, through return, but not through function argumentID0001447:
**This issue was created automatically from Mantis Issue 1447. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001447:
**This issue was created automatically from Mantis Issue 1447. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001447 | Frama-C | Plug-in > Eva | public | 2013-06-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Running "frama-c -val ftest.c" on the attached program doesn't produce any warning, although the uninitialized value of variable "undf" is passed to variable "i" and "k" via assignment to a pointer and via return in line 7 and 9, respectively.
If it is passed also to variable "j" via function argument (uncomment line 8 to do this), a warning is issued, as expected, even although "j" is never used.
I would have expected similar behavior in all 3 cases, preferrable issuing always a warning.
## Attachments
- [ftest.c](/uploads/0fe3a52d968a24b302d37eb327e5b80f/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/1179Frama-C Kernel on a specific C file (unexpected error, assertion failed)2022-10-21T11:21:18ZDavid MentréFrama-C Kernel on a specific C file (unexpected error, assertion failed)ID0001475:
**This issue was created automatically from Mantis Issue 1475. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001475:
**This issue was created automatically from Mantis Issue 1475. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001475 | Frama-C | Kernel | public | 2013-09-03 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
When Frama-C is launched on attached file, I get an exception.
$ frama-c q4_error_static_fun.c
[kernel] preprocessing with "gcc -C -E -I. questions/q4_error_static_fun.c"
[kernel] failure: Some globals contain dangling references after link:
F4:f5;
[kernel] Current source was: questions/q4_error_static_fun.c:35
The full backtrace is:
Raised at file "cil/src/mergecil.ml", line 2842, characters 2-167
Called from file "cil/src/mergecil.ml", line 2903, characters 16-37
Called from file "src/kernel/file.ml", line 1082, characters 20-56
Called from file "src/kernel/file.ml", line 1936, characters 12-30
Called from file "src/kernel/file.ml", line 2020, characters 4-27
Called from file "src/kernel/ast.ml", line 103, characters 2-28
Called from file "src/kernel/ast.ml", line 114, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Unexpected error (File "cil/src/mergecil.ml", line 2842, characters 2-8: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601.
## Attachments
- [q4_error_static_fun.c](/uploads/101d5f158fda1dda3691b247e573920d/q4_error_static_fun.c)https://git.frama-c.com/pub/frama-c/-/issues/1180Unsound transformation of ACSL annotations2021-02-22T13:22:25ZPascal CuoqUnsound transformation of ACSL annotationsID0001469:
**This issue was created automatically from Mantis Issue 1469. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001469:
**This issue was created automatically from Mantis Issue 1469. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001469 | Frama-C | Kernel | public | 2013-08-21 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Test in SVN 23392: tests/misc/logic_ptr_cast.i
Obtained result:
[value] Called Frama_C_show_each({{ &t + {0; 4; 8; 12; 16; 20; 24; 28} }})
...
/*@
assert
((((((p == (int *)t || p == (int *)(&t[1])) || p == (int *)(&t[2])) ||
p == (int *)(&t[3]))
|| p == (int *)(&t[4]))
|| p == (int *)(&t[5]))
|| p == (int *)(&t[6]))
|| p == (int *)(&t[7]); */
Expected result:
[value] Called Frama_C_show_each({{ &t + {0; 1; 2; 3; 4; 5; 6; 7} }})
and the same assert as the one written in the program.https://git.frama-c.com/pub/frama-c/-/issues/1181invalid loop invariant marked as valid (without pending hypothesis)2021-02-22T13:30:09ZVirgile Prevostoinvalid loop invariant marked as valid (without pending hypothesis)ID0001462:
**This issue was created automatically from Mantis Issue 1462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001462:
**This issue was created automatically from Mantis Issue 1462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001462 | Frama-C | Plug-in > wp | public | 2013-07-29 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **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** | Frama-C Neon-20140301 |
### Description :
Given the program below, wp discharges all proof obligations, including the first loop invariant whose preservation is false. This allows then to prove the invalid assertion after the loop. It seems that all three loop invariants (with their \at() term) are necessary to reproduce the issue.
### Additional Information :
-- file.c
void f(int c) {
int x = 0;
int y = 0;
/*@ assert for_value: c<= 0 || c == 1 || c>=2; */
if (c==2) { x=1; y=1; }
L:
/*@
loop invariant \at(x==0,L) ==> i!=0 ==> y == 0;
loop invariant \at(x==1,L) ==> i!=0 ==> x == 1;
loop invariant \at(c==0,Pre) ==> i==0 ==> x == 0;
loop assigns i,x,y;
*/
for (int i = 0; i<10; i++) {
if (c == 0) { x = 0; }
if (c == 1) { y = 1; }
if (c == 2) { x = 1; }
}
if (c==1) { /*@ assert consequence_of_false_invariant: y==0; */ }
}
### Steps To Reproduce :
frama-c -wp file.c
One can see the inconsistent status (green/black bullet) of the assert with
frama-c-gui -wp file.c -then -val -main f -slevel 100https://git.frama-c.com/pub/frama-c/-/issues/1182goto L; with L: in a if/else branch2021-02-22T13:46:04ZDillon Parientegoto L; with L: in a if/else branchID0001502:
**This issue was created automatically from Mantis Issue 1502. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001502:
**This issue was created automatically from Mantis Issue 1502. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001502 | Frama-C | Kernel | public | 2013-10-16 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
[STANCE]
The following code:
void f(int a)
{
goto _LOR_0;
if (a) _LOR_0: ;
}
analyzed by:
frama-c ../skip.c -print -ocode ../skip2.c
(with or without -no-simplify-cfg)
generates a warning:
[kernel] user error: Label _LOR_0 not found
and an error when parsing pretty-printed code in skip2.c:
frama-c ../skip2.c
[kernel] user error: Label _LOR_0 not found
It seems that the branch containing the label is pruned as considered as empty!
Typically, modifying cabs2cil.ml (line 1142) so that Instr (Skip _) is no more considered as an empty stmt solves the problem (of course this is just a workaround!). Is something more robust available?
## Attachments
- [bts1502.patch](/uploads/9d5770006929f966bf768c169c8c6b21/bts1502.patch)https://git.frama-c.com/pub/frama-c/-/issues/1183r24011: failure: Invalid combination of type specifiers2021-02-22T13:42:18ZPascal Cuoqr24011: failure: Invalid combination of type specifiersID0001500:
**This issue was created automatically from Mantis Issue 1500. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001500:
**This issue was created automatically from Mantis Issue 1500. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001500 | Frama-C | Kernel | public | 2013-10-09 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The following program is accepted by gcc:
$ cat l.c
typedef int digit;
struct S {
int const digit;
};
$ gcc -c l.c
But Frama-C fails to parse it:
$ frama-c l.c
[kernel] preprocessing with "gcc -C -E -I. l.c"
l.c:3:[kernel] failure: Invalid combination of type specifiers:
int digit
[kernel] user error: skipping file "l.c" that has errors.
[kernel] Frama-C aborted: invalid user input.https://git.frama-c.com/pub/frama-c/-/issues/1184Obfuscator for C Labels2021-02-22T13:22:32ZPatrick BaudinObfuscator for C LabelsID0001562:
**This issue was created automatically from Mantis Issue 1562. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001562:
**This issue was created automatically from Mantis Issue 1562. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001562 | Frama-C | Plug-in > obfuscator | public | 2013-11-21 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
C Label names to to be obfuscated.
### Additional Information :
> frama-c -obfuscate file.c
int main(int f1)
{
int V1;
V1 = 0;
if (f1) goto end;
V1 ++;
end: ;
return V1;
}https://git.frama-c.com/pub/frama-c/-/issues/1185Binding of label in annotations is strange2021-02-22T13:22:33ZFrançois BobotBinding of label in annotations is strangeID0001536:
**This issue was created automatically from Mantis Issue 1536. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001536:
**This issue was created automatically from Mantis Issue 1536. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001536 | Frama-C | Kernel > ACSL implementation | public | 2013-10-28 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The following function without "LLoop:" type-check, with it doesn't.
======================
void f() {
int i;
LInit:
{
LLoop:
i = 0;
//@ assert \at(1,LInit) == 1;
}
}
======================
[kernel] preprocessing with "gcc -C -E -I. error_typer.c"
error_typer.c:8:[kernel] user error: logic label `LInit' not found in annotation.
[kernel] user error: skipping file "error_typer.c" that has errors.
[kernel] Frama-C aborted: invalid user input.https://git.frama-c.com/pub/frama-c/-/issues/1186Assertion failure in Ival.scale_div2021-02-22T13:22:35ZBoris YakobowskiAssertion failure in Ival.scale_divID0001584:
**This issue was created automatically from Mantis Issue 1584. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001584:
**This issue was created automatically from Mantis Issue 1584. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001584 | Frama-C | Plug-in > Eva | public | 2013-12-09 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
(Csmith-found program, reduced by creduce)
To be analyzed with -slevel 4.
Interesting part of the backtrace:
Called from file "src/ai/ival.ml", line 1011, characters 3-123
Called from file "src/ai/ival.ml", line 1166, characters 2-35
Called from file "src/ai/ival.ml", line 2370, characters 20-48
## Attachments
- [small3.i](/uploads/5eae9a679e659d4b5d94d6604e24c457/small3.i)https://git.frama-c.com/pub/frama-c/-/issues/1190access to volatile variable is eliminated from AST2021-02-22T13:22:42ZPascal Cuoqaccess to volatile variable is eliminated from ASTID0001589:
**This issue was created automatically from Mantis Issue 1589. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001589:
**This issue was created automatically from Mantis Issue 1589. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001589 | Frama-C | Kernel | public | 2013-12-26 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **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 Neon-20140301 |
### Description :
~ $ cat n.c
volatile int x;
int main(){
x; x; x;
}
~ $ ~/ppc/bin/toplevel.opt -print n.c
[kernel] preprocessing with "gcc -C -E -I. n.c"
/* Generated by Frama-C */
int volatile x;
int main(void)
{
int __retres;
__retres = 0;
return __retres;
}
This transformation does not respect the semantics of the program because x is volatile.https://git.frama-c.com/pub/frama-c/-/issues/1191WP ignores some goal2021-02-22T14:02:45Zmantis-gitlab-migrationWP ignores some goalID0001588:
**This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001588:
**This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001588 | Frama-C | Plug-in > wp | public | 2013-12-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
On this example, WP ignore some of the goals. There should be 3 goals, but :
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_loop_inv_l1_2_established : Valid
Loop invariant preservation and assertion are ignore.
### Additional Information :
I simplified the example as much as possible, but it seems that the number of statements is important to reproduce the problem 8-/
### Steps To Reproduce :
frama-c wp.c -wp
## Attachments
- [wp.c](/uploads/f296e3e3d81e278bf5e25179c5d16e29/wp.c)https://git.frama-c.com/pub/frama-c/-/issues/1192Bug in let-elimination (due to <==> and assert false).2023-02-03T12:18:59ZLoïc CorrensonBug in let-elimination (due to <==> and assert false).ID0001586:
**This issue was created automatically from Mantis Issue 1586. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001586:
**This issue was created automatically from Mantis Issue 1586. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001586 | Frama-C | Plug-in > wp | public | 2013-12-16 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Bug in let-elimination (due to <==> and assert false).
Using -wp-no-let makes the assert false not-proved as expected.
### Additional Information :
In the attached program, we have no assumption and everything is proved
with WP (Frama-C Fluorine June), including the assert 1==2 in case N!
frama-c-gui -pp-annot -wp -wp-rte q19_switch_fun_call.c
It appears that the issue is coming from the equivalences used in the
behaviours of compute_trans(). If we replace "<==>" by "==>", then the
1==2 assert is not proved (substitute call to compute_trans() by
compute_trans2() in main()).
In both cases (compute_trans() and compute_trans2()), the contract is
always proved.
## Attachments
- [q19_switch_fun_call.c](/uploads/fa377321dbdcb32a2de9f013fc50164f/q19_switch_fun_call.c)
- [q20_switch_fun_call.c](/uploads/3a712d89800fa2c38926aac03f141f57/q20_switch_fun_call.c)https://git.frama-c.com/pub/frama-c/-/issues/1194Feedback from -remove-redundant-alarms2023-01-04T11:04:21Zmantis-gitlab-migrationFeedback from -remove-redundant-alarmsID0001590:
**This issue was created automatically from Mantis Issue 1590. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001590:
**This issue was created automatically from Mantis Issue 1590. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001590 | Frama-C | Plug-in > scope | public | 2014-01-02 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | low | **Severity** | text | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
It would be nice to have the list of the removed annotations when -remove-redundant-alarms is used. At the moment, it is a debug message, but I think that it should be a feedback message instead (could be only printed for -scope-verbose 2 for instance).https://git.frama-c.com/pub/frama-c/-/issues/1195Qedlib.v definition of tactic "replace by" clashes with standard tactic "repl...2023-01-04T11:04:20ZJens GerlachQedlib.v definition of tactic "replace by" clashes with standard tactic "replace with"ID0001626:
**This issue was created automatically from Mantis Issue 1626. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001626:
**This issue was created automatically from Mantis Issue 1626. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001626 | Frama-C | Plug-in > wp | public | 2014-01-22 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I cannot use the standard coq tactic "replace with" because it clashes (apparently with
"replace by" defined in Qedlib.v)
### Steps To Reproduce :
Just try to use "replace A by B" in a coq proof of a wp proof obligationhttps://git.frama-c.com/pub/frama-c/-/issues/1197Allow starting coq from Frama-C GUI also for proven obligations2021-02-22T13:30:12ZJens GerlachAllow starting coq from Frama-C GUI also for proven obligationsID0001623:
**This issue was created automatically from Mantis Issue 1623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001623:
**This issue was created automatically from Mantis Issue 1623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001623 | Frama-C | Plug-in > wp | public | 2014-01-21 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, OSX | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Currently it is not possible to start the codide from the Frama-C GUI
for a proof obligation that has already been proven by Coq.
However, it would be desirable to do so in order to improve/refactor an already existing proof.https://git.frama-c.com/pub/frama-c/-/issues/1199Confusing bullets for unproven obligations under OSX2021-02-22T13:30:17ZJens GerlachConfusing bullets for unproven obligations under OSXID0001631:
**This issue was created automatically from Mantis Issue 1631. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001631:
**This issue was created automatically from Mantis Issue 1631. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001631 | Frama-C | Plug-in > wp | public | 2014-01-24 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | OSX | **OS** | - | **OS Version** | 10.9.1 |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Under OSX an unproven obligation is depicted by a red bullet.
It appears as if that po is actually wrong.
Under Linux a cross (x) is shown instead, which I find better.
I think I would prefer a question mark for a proof obligation that could neither be verified nor refuted.
I attach two screen shots: one from osx and one from linux that show the differences.
### Additional Information :
might be related to issue 0001485
## Attachments
- [gui-osx-and-xubuntu.pdf](/uploads/df960fcf66544389a56320c9d25012b9/gui-osx-and-xubuntu.pdf)https://git.frama-c.com/pub/frama-c/-/issues/1201syntax error in value binary assignment2023-01-31T17:32:45Zmantis-gitlab-migrationsyntax error in value binary assignmentID0000929:
**This issue was created automatically from Mantis Issue 929. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000929:
**This issue was created automatically from Mantis Issue 929. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000929 | Frama-C | Kernel | public | 2011-08-18 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | inti | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I am developing a microcontroller, My code is like this assignment:
LPC_IOCON->PIO0_1=0b00000000000000000000000000000000;
and all of this kind of assignment cause this error in frama-c value analysis
[kernel] preprocessing with "gcc -C -E -I. peripheral-gpio.c"
peripheral-gpio.c:28:[kernel] user error: syntax error
[kernel] user error: skipping file "peripheral-gpio.c" that has errors.
I think the problem is the binary value because when I assign a integer or hexa value the problem disappear.https://git.frama-c.com/pub/frama-c/-/issues/1202Logging huge messages makes kernel crashing2021-02-22T14:02:46Zmantis-gitlab-migrationLogging huge messages makes kernel crashingID0000624:
**This issue was created automatically from Mantis Issue 624. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000624:
**This issue was created automatically from Mantis Issue 624. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000624 | Frama-C | Kernel | public | 2010-11-10 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | teamod | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The environment is exactly the same as described in 0000623, below is the output.
[kernel] The full backtrace is:
Raised by primitive operation at file "src/kernel/log.ml", line 201, characters 9-24
Called from file "format.ml", line 299, characters 4-28
Called from file "format.ml", line 428, characters 6-72
Called from file "format.ml", line 435, characters 6-24
Called from file "format.ml", line 1152, characters 8-28
Called from file "format.ml", line 1157, characters 10-25
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "external/ptmap.ml", line 153, characters 3-15
Called from file "format.ml", line 1157, characters 10-25
Called from file "format.ml", line 1157, characters 10-25
Called from file "format.ml", line 1157, characters 10-25
Called from file "src/memory_state/offsetmap.ml", line 265, characters 6-66
Called from file "src/lib/rangemap.ml", line 172, characters 20-25
Called from file "format.ml", line 1157, characters 10-25
Called from file "format.ml", line 1157, characters 10-25
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "external/ptmap.ml", line 535, characters 16-35
Called from file "src/memory_state/lmap.ml", line 290, characters 4-43
Called from file "src/memory_state/relations_type.ml", line 750, characters 4-43
Called from file "format.ml", line 1157, characters 10-25
Called from file "queue.ml", line 134, characters 6-20
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 50, characters 4-20
Called from file "src/kernel/cmdline.ml", line 170, characters 4-8
Unexpected error (Invalid_argument("String.create")).
Please report as 'crash' at http://bts.frama-c.comhttps://git.frama-c.com/pub/frama-c/-/issues/1203inconsistent redefinition of type undetected2021-02-22T13:30:27ZJochen Burghardtinconsistent redefinition of type undetectedID0001330:
**This issue was created automatically from Mantis Issue 1330. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001330:
**This issue was created automatically from Mantis Issue 1330. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001330 | Frama-C | Kernel | public | 2012-12-14 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The attached program defines a type "ftest_t" as "int*" in line 2, but as "double" in line 3. This inconsistently defined type is used as parameter type in line 5. Nevertheless, the command "frama-c ftest.c" does not report any error (under Nitrogen; I can't yet test it here under Oxygen).
## Attachments
- [ftest.c](/uploads/fdd52731c6f37a8300774480ecb86eaf/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/1204Smarter access to array of struct of array2021-02-22T13:23:20ZPascal CuoqSmarter access to array of struct of arrayID0001044:
**This issue was created automatically from Mantis Issue 1044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001044:
**This issue was created automatically from Mantis Issue 1044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001044 | Frama-C | Plug-in > Eva | public | 2011-12-10 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Smarter access to array of struct of array
## Attachments
- [test1.c](/uploads/c77a0f373169ebe36d95a11954412e2c/test1.c)https://git.frama-c.com/pub/frama-c/-/issues/1205Property reported as inconditionnally valid when its dependency graph shows s...2021-02-22T13:30:33ZVirgile PrevostoProperty reported as inconditionnally valid when its dependency graph shows some orange boxID0001443:
**This issue was created automatically from Mantis Issue 1443. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001443:
**This issue was created automatically from Mantis Issue 1443. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001443 | Frama-C | Plug-in > wp | public | 2013-06-11 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Using wp on the attached files, the rte-generated asserts (and some loop invariants) are reported as valid (green bullet), while they are dependent of some unproved loop invariant.
I flag it as WP bug, as it occurs only when specifying two provers with -wp-proof, so that I suspect some issue in reporting dependencies in this setting.
### Steps To Reproduce :
command line used:
frama-c-gui -wp -wp-model Typed+ref -wp-split binary_search_proved.c -wp-rte -wp-proof alt-ergo,why3:Z3
## Attachments
- [binary_search_proved.c](/uploads/4339976a1729dbee33172d7fad3defb5/binary_search_proved.c)https://git.frama-c.com/pub/frama-c/-/issues/1206Stack overflow when computing a PDG2021-02-22T13:23:23ZJulien SignolesStack overflow when computing a PDGID0001436:
**This issue was created automatically from Mantis Issue 1436. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001436:
**This issue was created automatically from Mantis Issue 1436. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001436 | Frama-C | Plug-in > pdg | public | 2013-05-30 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
==== test.c ====
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR: goto ERROR;
}
return;
}
#define a (2)
int main(unsigned int loop1, unsigned int m1) {
int sn=0;
unsigned int x=0;
while(1){
sn = sn + a;
x++;
__VERIFIER_assert(sn==x*a || sn == 0);
}
}
==========
$ frama-c -pdg test.c
<skip value's trace>
[pdg] computing for function __VERIFIER_assert
[pdg] done for function __VERIFIER_assert
[pdg] computing for function main
[kernel] Current source was: sum03_safe.c:5
The full backtrace is:
Called from file "set.ml", line 216, characters 18-33
Called from file "list.ml", line 195, characters 17-20
Called from file "src/kernel/stmts_graph.ml", line 418, characters 6-65
Called from file "src/pdg/ctrlDpds.ml", line 217, characters 35-59
Called from file "list.ml", line 86, characters 24-34
Called from file "src/pdg/ctrlDpds.ml", line 237, characters 29-39
Called from file "src/pdg/ctrlDpds.ml", line 257, characters 22-31
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
<skip the rest of the backrace>
### Additional Information :
Bug coming from Checkofv...https://git.frama-c.com/pub/frama-c/-/issues/1208assigns \result \from ...; in the AST should be pretty-printed as any other a...2021-02-22T13:23:28ZLoïc Corrensonassigns \result \from ...; in the AST should be pretty-printed as any other assigns clauseID0001480:
**This issue was created automatically from Mantis Issue 1480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001480:
**This issue was created automatically from Mantis Issue 1480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001480 | Frama-C | Kernel > ACSL implementation | public | 2013-09-17 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
int x,y;
//@ assigns x \from y ;
void f (void);
//@ assigns \result \from y ;
int g (void);
Pour f : la clause "assigns x" est visible dans l'AST.
Pour g : il manque la clause "assigns \nothing" dans l'AST (qui est pourtant prouvée par le WP).https://git.frama-c.com/pub/frama-c/-/issues/1209Interpretation of @ assigns \result;2023-05-16T12:35:51Zmantis-gitlab-migrationInterpretation of @ assigns \result;ID0001448:
**This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001448:
**This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001448 | Frama-C | Plug-in > Eva | public | 2013-06-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Sorry for the title which is not very informative, but here is the problem :
in this example :
//@ assigns \result;
extern char * get_ptr (void);
int main (void) { char * p = get_ptr (); int x = p ? 0 : 1; return x; }
The value analysis tells me that the else branch is dead, so x is always 0.
If I change the assigns property into :
//@ assigns \result \from \nothing;
The problem disappears.https://git.frama-c.com/pub/frama-c/-/issues/1210Crash when selecting the calls to an unterminating functions2021-02-22T13:30:25ZJulien SignolesCrash when selecting the calls to an unterminating functionsID0001445:
**This issue was created automatically from Mantis Issue 1445. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001445:
**This issue was created automatically from Mantis Issue 1445. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001445 | Frama-C | Plug-in > slicing | public | 2013-06-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | high | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Fluorine-20130501 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
$ less bug.i
int x = 0;
int main() {
while(1)
x=0;
return 0;
}
$ frama-c.byte -slice-calls main bug.i
[slicing] slicing requests in progress...
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
x ? {0}
bug.i:4:[value] entering loop for the first time
[value] Recording results for main
[value] done for function main
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[pdg] computing for function main
bug.i:6:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function main
[kernel] Current source was: bug.i:5
The full backtrace is:
Raised at file "src/slicing/register.ml", line 150, characters 23-35
Called from file "src/slicing/slicingCmds.ml", line 200, characters 25-96https://git.frama-c.com/pub/frama-c/-/issues/1211validity of a field defined in an abstract struct typedef2021-02-22T13:30:31ZDillon Parientevalidity of a field defined in an abstract struct typedefID0001486:
**This issue was created automatically from Mantis Issue 1486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001486:
**This issue was created automatically from Mantis Issue 1486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001486 | Frama-C | Plug-in > Eva | public | 2013-09-26 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
[STANCE]
The small source code snippet is extracted from an Apache server module.
//------------------------------------
struct core_dir_config { int server_signature; } core_dir_config;
typedef struct core_dir_config core_dir_config;
struct request_rec { struct ap_conf_vector_t *per_dir_config; } request_rec;
typedef struct request_rec request_rec;
//@ requires \valid(r->per_dir_config);
const char * app(request_rec *r)
{
core_dir_config *conf;
conf = (core_dir_config *)(((void **)(r->per_dir_config))[0]);
if (conf->server_signature == 1) { return ""; }
return " ";
}
//------------------------------------
When analyzed by:
frama-c -val -main app bug.c -lib-entry -no-unicode
Value generates an error:
$ Internal error 835; debug info:
{{ NULL -> {0}; S_r -> {0} }} (size:<32>)
Is it "abstract struct type" related?
Is there any workaround?
## Attachments
- [patch-stance](/uploads/e7a7207756d1fab4453eae629c1694c0/patch-stance)https://git.frama-c.com/pub/frama-c/-/issues/1217Error message when a solver is not installed2021-02-22T13:30:54ZLoïc CorrensonError message when a solver is not installedID0001549:
**This issue was created automatically from Mantis Issue 1549. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001549:
**This issue was created automatically from Mantis Issue 1549. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001549 | Frama-C | Plug-in > wp | public | 2013-11-07 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
On error status 127.
### Additional Information :
your current error message when alt-ergo is not installed is:
[wp] [Alt-Ergo] Goal typed_main_loop_inv_preserved : Failed
Error: Alt-Ergo exits with status [127]
You might want to change this, it sounds like alt-ergo is installed :)https://git.frama-c.com/pub/frama-c/-/issues/1220Obfuscator for tags names in ACSL terms, properties, behaviors2023-11-21T14:40:58ZPatrick BaudinObfuscator for tags names in ACSL terms, properties, behaviorsID0001563:
**This issue was created automatically from Mantis Issue 1563. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001563:
**This issue was created automatically from Mantis Issue 1563. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001563 | Frama-C | Plug-in > obfuscator | public | 2013-11-21 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Tags names in ACSL terms, properties, behaviors need to be obfucated.
### Additional Information :
> frama-c -obfuscate file.c
/*@ behavior bhv:
exits never: \false;
complete behaviors bhv; */
int main(int f1)
{
int V1;
V1 = 0;
if (f1) goto end;
V1 ++;
/*@ assert property: V1 ? 1; */ ;
end: ;
return V1;
}https://git.frama-c.com/pub/frama-c/-/issues/1221pointer comparable assert generated between void* and unsigned long2021-02-22T13:23:55ZDillon Parientepointer comparable assert generated between void* and unsigned longID0001559:
**This issue was created automatically from Mantis Issue 1559. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001559:
**This issue was created automatically from Mantis Issue 1559. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001559 | Frama-C | Plug-in > Eva | public | 2013-11-19 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
[STANCE]
The following code:
/*------------------------------------------*/
typedef unsigned long size_t;
struct apr_file_t;
typedef struct apr_file_t apr_file_t;
struct apr_file_t {char *fname ;};
int apr_file_write(apr_file_t *thefile, unsigned long *nbytes);
int apr_file_write_full(apr_file_t *thefile, unsigned long nbytes, unsigned long *bytes_written)
{ int status;
unsigned long a;
a = nbytes;
status = apr_file_write(thefile,& a);
nbytes -= a;
if (! (nbytes > (unsigned long)0)) return 0;
return 1;
}
/*------------------------------------------*/
analyzed by:
frama-c.exe -val -main apr_file_write_full -lib-entry foo.c -no-unicode
generates an assert:
[kernel] warning: pointer comparison:
assert \pointer_comparable((void *)nbytes, (unsigned long)0);
which, once the project is pretty-printed (-print -ocode ...),
yields an error on the generated C file:
[kernel] user error: no such predicate or logic function \pointer_comparable(void *, unsigned long) in annotation.
(... indeed it might be an issue at Kernel level!)
## Attachments
- [patch-ptr-comparable](/uploads/93c9deb5551e847fe57e42df72977385/patch-ptr-comparable)https://git.frama-c.com/pub/frama-c/-/issues/1223Syntax error because of pause instruction in inline assebly2023-03-27T07:28:17Zmantis-gitlab-migrationSyntax error because of pause instruction in inline asseblyID0001573:
**This issue was created automatically from Mantis Issue 1573. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001573:
**This issue was created automatically from Mantis Issue 1573. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001573 | Frama-C | Kernel | public | 2013-11-27 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | valor | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Presence of construction like
-----------------------------------------
static inline void cpu_pause(void)
{
__asm__ volatile ("pause":::);
}
-----------------------------------------
lead to syntax error
Adding some "changed" (like <:::"memory");>) improves the situation
### Additional Information :
GUI output
-----------------------------------------
Current source was: :0
The full backtrace is:
Raised at file "hashtbl.ml", line 353, characters 18-27
Called from file "hashtbl.ml", line 361, characters 22-38
Unexpected error (Parsing.Parse_error).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601.
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
---------------------------------------------https://git.frama-c.com/pub/frama-c/-/issues/1224Multiple contracts merge twice resutling in Kernel error2021-02-22T13:30:51ZDavid MentréMultiple contracts merge twice resutling in Kernel errorID0001572:
**This issue was created automatically from Mantis Issue 1572. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001572:
**This issue was created automatically from Mantis Issue 1572. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001572 | Frama-C | Kernel | public | 2013-11-27 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
With the attached files, when I call the following command I get a backtrace:
frama-c questions/q18_a.c questions/q18_b.c
"""
[kernel] preprocessing with "gcc -C -E -I. questions/q18_a.c"
questions/q18_a.h:6:[kernel] warning: found two contracts. Merging them
[kernel] preprocessing with "gcc -C -E -I. questions/q18_b.c"
questions/q18_a.c:18:[kernel] warning: found two contracts. Merging them
questions/q18_a.c:18:[kernel] warning: found two contracts. Merging them
[kernel] failure: trying to register twice property `requires
p ? 10'.
That is forbidden (kernel invariant broken).
[kernel] Current source was: questions/q18_b.c:8
The full backtrace is:
Raised at file "src/kernel/log.ml", line 523, characters 30-31
Called from file "src/kernel/log.ml", line 517, characters 9-16
Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
Called from file "src/logic/property_status.ml", line 292, characters 4-132
Called from file "list.ml", line 75, characters 12-15
Called from file "set.ml", line 305, characters 38-41
Called from file "src/kernel/file.ml", line 1487, characters 2-53
Called from file "src/kernel/file.ml", line 2020, characters 4-27
Called from file "src/kernel/ast.ml", line 103, characters 2-28
Called from file "src/kernel/ast.ml", line 114, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
"""
Strangely enough, I call frama-c on the files in the reverse order, everything goes well:
frama-c questions/q18_b.c questions/q18_a.c
"""
[kernel] preprocessing with "gcc -C -E -I. questions/q18_b.c"
[kernel] preprocessing with "gcc -C -E -I. questions/q18_a.c"
questions/q18_a.h:6:[kernel] warning: found two contracts. Merging them
questions/q18_a.c:18:[kernel] warning: found two contracts. Merging them
"""
## Attachments
- [q18_a.c](/uploads/10f04c0db051498b932d92fdd22e9db9/q18_a.c)
- [q18_a.h](/uploads/7f819244d8d7735ba6fe1091fda5263d/q18_a.h)
- [q18_b.c](/uploads/16ee6ccbd60257bd93b2d638f80ab9b3/q18_b.c)https://git.frama-c.com/pub/frama-c/-/issues/1226WP Plugin with Alt-Ergo - unable to prove?2023-03-06T17:48:30Zmantis-gitlab-migrationWP Plugin with Alt-Ergo - unable to prove?ID0001601:
**This issue was created automatically from Mantis Issue 1601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001601:
**This issue was created automatically from Mantis Issue 1601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001601 | Frama-C | Plug-in > wp | public | 2014-01-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | block | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I'm trying to test WP plugin with Alt-Ergo on a fairly complex function. Unfortunately, I am not able to figure out what's wrong with the "basic" behavior given below.
This behavior should be true because there is no other place tenumRMode is updated except the first conditional statement's else section.
The weird thing is that if I comment some lines arbitrarily (after the first if-else block) I always get "valid" from Alt-ergo.
Any comments? The below code might be lengthy, but the behavior is easy to verify manually because the variables mentioned in the behavior are never updated after the first if-else block.
I also discussed with a alt-ergo developer, see http://stackoverflow.com/questions/21036098/wp-plugin-with-alt-ergo-unable-to-prove
### Steps To Reproduce :
/*@ behavior basic:
@ assumes fRrValue == 0;
@ ensures tenumRMode == SS_A_MODE;
@
*/
$ frama-c -wp -wp-rte -wp-bhv=basic foo.c -wp-out t -lib-entry -main foo -wp-model ref -wp-timeout=50 -wp-fct=foo -wp-out t
[kernel] preprocessing with "gcc -C -E -I. foo.c"
[wp] Running WP plugin...
[rte] annotating function foo
[wp] Collecting axiomatic usage
[wp] Collecting variable usage
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_ref_foo_basic_post : Unknown (Qed:20ms)
typedef unsigned char BOOL;
#define TRUE 1
#define FALSE 0
typedef unsigned char uint8;
typedef unsigned short int uint16;
typedef unsigned long uint32;
uint16 F_MIN_R = 15;
const uint8 RESP_STATE = 30;
typedef enum
{
RESP_MODE,
SS_A_MODE
}tenumMode;
tenumMode tenumRMode;
BOOL gbCaMStatus;
BOOL gbCaaStatus;
uint8 mnPb;
BOOL mbApLYRange;
BOOL mbApLRange;
float gfApYLineSlope;
float gfApYLineConst;
float gfApRLineSlope;
float gfApRLineConst;
float mfAp;
uint16 almC;
uint16 nApLYL = 0;
uint16 nApLRL = 0;
uint16 Ap_Y_L_Ui = 0;
uint16 Ap_R_L_Ui = 0;
float fCaValue=0.0;
float fRrValue = 0.0;
uint16 nCaLYL=0;
uint16 nCaLRL=0;
/*@ behavior basic:
@ assumes fRrValue == 0;
@ ensures tenumRMode == SS_A_MODE;
@
*/
void foo()
{
float mfNewAp = 0;
BOOL bYAp = FALSE;
BOOL bRAp = FALSE;
BOOL bApAlmC = FALSE;
if (fRrValue != 0)
{
/* Some code here */
}
else
{
if (mnPb == 1)
{
mfAp = RESP_STATE;
mnPb = 2;
}
tenumRMode = SS_A_MODE;
}
if ( (mfAp >= F_MIN_R) &&
((gbCaMStatus == TRUE) && (gbCaaStatus == FALSE)) )
{
bApAlmC = TRUE;
almC = 1;
}
else
{
almC = 0;
}
if ( (bApAlmC == TRUE)
&& (mfAp < nApLYL)
&& (fCaValue >= nCaLYL) )
{
float fmultval = 0;
fmultval = gfApYLineSlope*fCaValue;
mfNewAp = fmultval + gfApYLineConst;
if (mfAp >= mfNewAp)
bYAp = TRUE;
else
bYAp = FALSE;
Ap_Y_L_Ui = (uint16)mfNewAp;
}
if ((bApAlmC == TRUE) && (fCaValue > (float)nCaLYL))
{
mfNewAp = ((gfApYLineSlope*fCaValue) + gfApYLineConst);
if (mfNewAp < (float)nApLYL);
Ap_Y_L_Ui = (uint16)mfNewAp;
}
else if ((bApAlmC == TRUE) && (fCaValue <= (float)nCaLYL))
Ap_Y_L_Ui = F_MIN_R;
if ( (bApAlmC == TRUE) && (fCaValue >= nCaLRL) )
{
float fmultval = 0;
fmultval = gfApRLineSlope*fCaValue;
mfNewAp = fmultval + gfApRLineConst;
if (mfAp >= mfNewAp)
bRAp = TRUE;
else
bRAp = FALSE;
Ap_R_L_Ui = (uint16)mfNewAp;
}
else if ( (bApAlmC == TRUE) && (fCaValue < nCaLRL) )
Ap_R_L_Ui = F_MIN_R;
if ( (mfAp >= nApLYL)
|| ((bApAlmC == TRUE) && (fCaValue < nCaLYL))
|| ((bYAp == TRUE)
&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) )
{
mbApLYRange = TRUE;
}
else
mbApLYRange = FALSE;
if ( (mfAp >= nApLRL)
|| ((bApAlmC == TRUE) && (fCaValue < nCaLRL))
|| ((bRAp == TRUE)
&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) )
{
/* Some code here */
}
}https://git.frama-c.com/pub/frama-c/-/issues/1228Field 'find' required but not provided in src/ai/abstract_interp.cmi2023-03-09T16:58:29Zmantis-gitlab-migrationField 'find' required but not provided in src/ai/abstract_interp.cmiID0001575:
**This issue was created automatically from Mantis Issue 1575. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001575:
**This issue was created automatically from Mantis Issue 1575. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001575 | Frama-C | Kernel | public | 2013-11-28 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jowi24 | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
$./make
Ocamlc src/ai/abstract_interp.cmi
File "src/ai/abstract_interp.mli", line 166, characters 4-33:
Error: In this `with' constraint, the new definition of O
does not match its original definition in the constrained signature:
...
The field `find' is required but not provided
share/Makefile.common:315: recipe for target 'src/ai/abstract_interp.cmi' failed
make: *** [src/ai/abstract_interp.cmi] Error 2
### Additional Information :
$ocaml -version
The OCaml toplevel, version 4.01.0
$gcc -v
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-unknown-linux-gnu/4.8.2/lto-wrapper
Ziel: x86_64-unknown-linux-gnu
Konfiguriert mit: /build/gcc/src/gcc-4.8.2/configure --prefix=/usr --libdir=/usr/lib --libexecdir=/usr/lib --mandir=/usr/share/man --infodir=/usr/share/info --with-bugurl=https://bugs.archlinux.org/ --enable-languages=c,c++,ada,fortran,go,lto,objc,obj-c++ --enable-shared --enable-threads=posix --with-system-zlib --enable-__cxa_atexit --disable-libunwind-exceptions --enable-clocale=gnu --disable-libstdcxx-pch --enable-gnu-unique-object --enable-linker-build-id --enable-cloog-backend=isl --disable-cloog-version-check --enable-lto --enable-gold --enable-ld=default --enable-plugin --with-plugin-ld=ld.gold --with-linker-hash-style=gnu --disable-install-libiberty --disable-multilib --disable-libssp --disable-werror --enable-checking=release
Thread-Modell: posix
gcc-Version 4.8.2 (GCC)https://git.frama-c.com/pub/frama-c/-/issues/1230WP: This term has type real but is expected to have type int2023-03-09T16:58:29Zmantis-gitlab-migrationWP: This term has type real but is expected to have type intID0001622:
**This issue was created automatically from Mantis Issue 1622. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001622:
**This issue was created automatically from Mantis Issue 1622. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001622 | Frama-C | Plug-in > wp | public | 2014-01-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Hi,
I'm not sure "This term has type real but is expected to have type int" when using WP with Z3 (Z3 version 4.3.1).
Please note that I do not have this error when I used alt-ergo (0.95.2).
$ frama-c -wp-proof=z3 -wp -wp-rte foo.c -wp-fct=foo -wp-bhv=basic -wp-out=t -pp-annot
[kernel] preprocessing with "gcc -C -E -I. -dD foo.c"
[wp] Running WP plugin...
[rte] annotating function foo
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
File "t/typed/foo_Why3_ide.why", line 60, characters 14-17:
This term has type real but is expected to have type int
------------------------------------------------------------
[wp] [Z3] Goal typed_foo_basic_post : Failed
Error: Why3 exits with status [1]
### Steps To Reproduce :
The generated why file is attached for your reference. foo.c is given below.
typedef unsigned char BOOL;
#define TRUE 1
#define FALSE 0
typedef unsigned char uint8;
typedef unsigned short int uint16;
typedef unsigned long uint32;
uint16 F_MIN_R = 15;
const uint8 RESP_STATE = 30;
typedef enum
{
RESP_MODE,
SS_A_MODE
}tenumMode;
tenumMode tenumRMode;
BOOL gbCaMStatus;
BOOL gbCaaStatus;
uint8 mnPb;
BOOL mbApLYRange;
float gfApYLineSlope;
float gfApYLineConst;
float gfApRLineSlope;
float gfApRLineConst;
float mfAp;
uint16 almC;
uint16 nApLYL = 0;
uint16 nApLRL = 0;
uint16 Ap_Y_L_Ui = 0;
uint16 Ap_R_L_Ui = 0;
float fCaValue=0.0;
float fRrValue = 0.0;
uint16 nCaLYL=0;
uint16 nCaLRL=0;
/*@
@ behavior basic:
@ assumes fRrValue == 0;
@ ensures tenumRMode == SS_A_MODE;
@
*/
void foo()
{
float mfNewAp = 0;
BOOL bYAp = FALSE;
BOOL bRAp = FALSE;
BOOL bApAlmC = FALSE;
if (fRrValue != 0)
{
/* Some code here */
}
else
{
if (mnPb == 1)
{
mfAp = RESP_STATE;
mnPb = 2;
}
tenumRMode = SS_A_MODE;
}
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ( (mfAp >= F_MIN_R) &&
((gbCaMStatus == TRUE) && (gbCaaStatus == FALSE)) )
{
bApAlmC = TRUE;
almC = 1;
}
else
{
almC = 0;
}
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ( (bApAlmC == TRUE)
&& (mfAp < nApLYL)
&& (fCaValue >= nCaLYL) )
{
float fmultval = 0;
fmultval = gfApYLineSlope*fCaValue;
mfNewAp = fmultval + gfApYLineConst;
if (mfAp >= mfNewAp)
bYAp = TRUE;
else
bYAp = FALSE;
Ap_Y_L_Ui = (uint16)mfNewAp;
}
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ((bApAlmC == TRUE) && (fCaValue > (float)nCaLYL))
{
mfNewAp = ((gfApYLineSlope*fCaValue) + gfApYLineConst);
if (mfNewAp < (float)nApLYL);
Ap_Y_L_Ui = (uint16)mfNewAp;
}
else if ((bApAlmC == TRUE) && (fCaValue <= (float)nCaLYL))
Ap_Y_L_Ui = F_MIN_R;
if ( (bApAlmC == TRUE) && (fCaValue >= nCaLRL) )
{
float fmultval = 0;
fmultval = gfApRLineSlope*fCaValue;
mfNewAp = fmultval + gfApRLineConst;
if (mfAp >= mfNewAp)
bRAp = TRUE;
else
bRAp = FALSE;
Ap_R_L_Ui = (uint16)mfNewAp;
}
else if ( (bApAlmC == TRUE) && (fCaValue < nCaLRL) )
Ap_R_L_Ui = F_MIN_R;
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ( (mfAp >= nApLYL)
|| ((bApAlmC == TRUE) && (fCaValue < nCaLYL))
|| ((bYAp == TRUE)
&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) )
{
mbApLYRange = TRUE;
}
else
mbApLYRange = FALSE;
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ( (mfAp >= nApLRL)
|| ((bApAlmC == TRUE) && (fCaValue < nCaLRL))
|| ((bRAp == TRUE)
&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) )
{
}
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
}
## Attachments
- [foo_Why3_ide.why](/uploads/1e4aa501f0fc2649d40235d8589c9976/foo_Why3_ide.why)https://git.frama-c.com/pub/frama-c/-/issues/1231Errors in coq files generated by WP2021-02-22T13:24:10Zmantis-gitlab-migrationErrors in coq files generated by WPID0001603:
**This issue was created automatically from Mantis Issue 1603. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001603:
**This issue was created automatically from Mantis Issue 1603. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001603 | Frama-C | Plug-in > wp | public | 2014-01-16 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I noticed some errors in the coq files generated by WP:
- real_of_int not defined,
- is_float32 : R -> Prop but used as bool (is_float32 f_0%R))%R=true)
- let x_0 := ((Zeq_bool 1 t_0))%Z in ... x_0 used both as bool and as Prop
### Additional Information :
The example is the foo.c file posted on [Frama-c-discuss] by David Mentre yesterday evening (15/01/2014 - 18:30)https://git.frama-c.com/pub/frama-c/-/issues/1234aorai causes failed assertion2021-02-22T13:31:22ZJochen Burghardtaorai causes failed assertionID0001289:
**This issue was created automatically from Mantis Issue 1289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001289:
**This issue was created automatically from Mantis Issue 1289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001289 | Frama-C | Plug-in > aoraï | public | 2012-10-25 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Running "frama-c ftest.c -aorai-automata ftest.ya" on the attached program causes an unexpectyed error in file cil_datatype.ml; see attached stdout log.
## Attachments
- [ftest.c](/uploads/00b0a24a7ad13eb171b46cdba01964c0/ftest.c)
- [ftest.ya](/uploads/9991a7f542c1b39583bf6d5770b4d0ba/ftest.ya)
- [log.txt](/uploads/79e5a6ac1f6b4465b46a3c7b5078777e/log.txt)https://git.frama-c.com/pub/frama-c/-/issues/1236Few fixes in libc/sys/socket.h2021-02-22T13:31:11Zmantis-gitlab-migrationFew fixes in libc/sys/socket.hID0001439:
**This issue was created automatically from Mantis Issue 1439. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001439:
**This issue was created automatically from Mantis Issue 1439. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001439 | Frama-C | Kernel | public | 2013-06-03 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | Matthieu Lemerre | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
In libc/sys/socket.h, some "../" are missing for some includes :
< #include "__fc_machdep.h"
> #include "../__fc_machdep.h"
< #include "__fc_define_ssize_t.h"
> #include "../__fc_define_ssize_t.h"
< #include "__fc_define_iovec.h"
> #include "../__fc_define_iovec.h"https://git.frama-c.com/pub/frama-c/-/issues/1238Value analysis: bad type conversion plus unassigned fields in a struct leads ...2021-02-22T13:24:25Zmantis-gitlab-migrationValue analysis: bad type conversion plus unassigned fields in a struct leads to crashID0001477:
**This issue was created automatically from Mantis Issue 1477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001477:
**This issue was created automatically from Mantis Issue 1477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001477 | Frama-C | Plug-in > Eva | public | 2013-09-04 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | djs52 | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The attached code crashes value analysis for me (with frama-c -val testcase.c):
[kernel] preprocessing with "gcc -C -E -I. testcase.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
testcase.c:3:[kernel] warning: overflow in conversion of - 1.0f (-1.) from floating-point to integer.
assert -1 < -1.0f < 256;
[kernel] Current source was: testcase.c:3
The full backtrace is:
Called from file "src/value/initial_state.ml", line 498, characters 14-70
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/initial_state.ml", line 461, characters 10-1023
Called from file "src/value/initial_state.ml", line 590, characters 20-70
Called from file "list.ml", line 69, characters 12-15
Called from file "src/value/initial_state.ml", line 565, characters 6-1023
Called from file "src/value/initial_state.ml", line 617, characters 13-23
Called from file "src/project/state_builder.ml", line 394, characters 17-21
Called from file "src/value/eval_funs.ml", line 313, characters 14-39
Called from file "src/value/eval_funs.ml", line 564, characters 11-40
Re-raised at file "src/value/eval_funs.ml", line 580, characters 47-50
Called from file "src/project/state_builder.ml", line 839, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 847, characters 15-18
Called from file "src/value/register.ml", line 46, characters 4-24
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 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Unexpected error (File "src/memory_state/lmap.ml", line 289, characters 18-24: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601.
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
- [testcase.c](/uploads/e8ac990612384bf1ede4018d69ea375e/testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/1240Frama-C GUI discards candidate coq proof2021-04-15T08:23:28ZJens GerlachFrama-C GUI discards candidate coq proofID0001687:
**This issue was created automatically from Mantis Issue 1687. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001687:
**This issue was created automatically from Mantis Issue 1687. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001687 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2014-03-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **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 problem is as follows:
In a Coq proof we add the line
repeat (rewrite shift_zero in *).
When quitting the Coq IDE, coq complains (correctly) about the token "*)" and restores the original proof,
thus completely discarding the proof attempt.
The proof attempt should at least be saved, somehow.
### Additional Information :
Running release candidate of Frama-C Neon.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1246Comments parsing2023-04-11T09:34:10ZVictoria Moya LamielComments parsingID0000616:
**This issue was created automatically from Mantis Issue 616. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000616:
**This issue was created automatically from Mantis Issue 616. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000616 | Frama-C | Kernel | public | 2010-10-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
When comments from the code are parsed by Frama-C and stored into Cabshelper.commentsGA, it seems that the first character from the comment disappears.
In the following example, we would find "est1" and "est2" instead of "test1" and "test2" :
//test1
/*test2*/
extern void test();https://git.frama-c.com/pub/frama-c/-/issues/1247possible unsoundness in r118662021-02-22T13:24:39ZJohn Regherpossible unsoundness in r11866ID0000718:
**This issue was created automatically from Mantis Issue 718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000718:
**This issue was created automatically from Mantis Issue 718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000718 | Frama-C | Plug-in > Eva | public | 2011-02-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **Assigned To** | pascal | **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 Nitrogen-20111001 |
### Description :
Analyzing the attached program like this:
~/z/frama-c/bin/toplevel.opt -val -slevel 46 foo_pp.c
Gives this assertion:
*(int*)&g_23 == -10
However, running the program gives value "-9" instead.
## Attachments
- [foo_pp.c](/uploads/df59ba5d2cd54d534cdf2e0f4299ed62/foo_pp.c)