frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:59:47Zhttps://git.frama-c.com/pub/frama-c/-/issues/341Operability depends on the order of options changes2021-02-22T12:59:47Zmantis-gitlab-migrationOperability depends on the order of options changesID0002277:
**This issue was created automatically from Mantis Issue 2277. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002277:
**This issue was created automatically from Mantis Issue 2277. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002277 | Frama-C | Plug-in > Eva | public | 2017-02-03 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
If value analysis is run on attached file with default options Frama-C makes no warnings. If you then turn on -warn-signed-downcast and repeat the analysis, a warning appears on the Message tab:
main.c:13:[value] warning: signed downcast. assert 128 ≤ 127;
If you reload Frama-C and turn on -warn-signed-downcast before first running of analysis, analysis will not run.
On Console tab will be output:
[value] Initial state computed
[value:initial-state] Values of globals at initialization
NOT ACCESSIBLE
[value] Value analysis not started because globals initialization is not computable.
If you then turn off -warn-signed-downcast and repeat the analysis, nothing changes.
### Steps To Reproduce :
1. Run Frama-C GUI.
2. Add attached file.
3. Turn on -warn-signed-downcast option.
4. Run value analysis.
5. Turn off -warn-signed-downcast option.
6. Run value analysis.
7. Reload Frama-C GUI.
8. Add attached file.
9. Run value analysis.
10. Turn on -warn-signed-downcast option.
11. Run value analysis.
## Attachments
- [main.c](/uploads/6fa38af626b269dcd5cb4e77024b802e/main.c)https://git.frama-c.com/pub/frama-c/-/issues/340EVA analysis does not start with click on "Execution" button.2021-02-22T12:59:44Zmantis-gitlab-migrationEVA analysis does not start with click on "Execution" button.ID0002279:
**This issue was created automatically from Mantis Issue 2279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002279:
**This issue was created automatically from Mantis Issue 2279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002279 | Frama-C | Plug-in > Eva | public | 2017-02-10 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
EVA analysis does not start with click on "Execution" button. But if select -val option it does it.
User have to click on "Run" button to start EVA analysis. This is unusual behavior.
### Steps To Reproduce :
1. [Customize EVA analysis]
2. Click on "Execution" button.
3. Verify that analysis did not started.
4. Select -val option.https://git.frama-c.com/pub/frama-c/-/issues/339Invalid results in presence of pseudo-recursive calls in inout and from2021-02-22T12:59:43ZBoris YakobowskiInvalid results in presence of pseudo-recursive calls in inout and fromID0000733:
**This issue was created automatically from Mantis Issue 733. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000733:
**This issue was created automatically from Mantis Issue 733. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000733 | Frama-C | Plug-in > inout | public | 2011-02-20 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
The Inout and From plugins are apparently designed to handle "pseudo" recursive calls, ie. when the value analysis does not detect a recursive call, but the plugin see a circularity in the stacks of examined functions. However, they are all buggy, because of the way the results are cached.
Indeed, when a circularity is encountered, the analysis is stopped immediately. This means that the results for the first function in the cycle is correct, but not those for the intermediate functions.
This can be seen with the example file: the inputs (option -input) for function h2 should include x.
### Additional Information :
Commit 12050 has removed most of the warnings the plugins printed unnecessarily when those pseudo recursive calls were encountered, so the error can now be completely silent (however, even with the warnings the plugins were buggy, as they implied that the analysis was correct if the value analysis was happy).
I have some (quite obvious) suggestions for correcting the bug, but they are not very efficient wrt to time complexity. Suggestions are welcome.
## Attachments
- [recursion2.i](/uploads/8eb737ed45eea708129388baa739b6db/recursion2.i)https://git.frama-c.com/pub/frama-c/-/issues/338Incorrectness when early exiting a block2021-02-22T12:59:41ZJulien SignolesIncorrectness when early exiting a blockID0001740:
**This issue was created automatically from Mantis Issue 1740. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001740:
**This issue was created automatically from Mantis Issue 1740. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001740 | Frama-C | Plug-in > E-ACSL | public | 2014-04-07 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
Local variables of a block are de-allocated at the end of the block. However, they are not de-allocated when exiting a block earlier (e.g. by a goto or a break). That may lead to incorrectness as in the attached example.
$ frama-c -e-acsl a.i -then-on e-acsl -print -ocode b.i
$ ./gcc.sh b.i
compiling b.i
executing b.i
Assertion failed at line 13 in function main.
The failing predicate is:
!\valid(p).
No error should be detected.
## Attachments
- [a.i](/uploads/6d82b2b9c687fba962ef8c594c4645d2/a.i)https://git.frama-c.com/pub/frama-c/-/issues/337suggest to check (loop) assigns clauses by data flow analysis2021-08-05T09:22:29ZJochen Burghardtsuggest to check (loop) assigns clauses by data flow analysisID0002308:
**This issue was created automatically from Mantis Issue 2308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002308:
**This issue was created automatically from Mantis Issue 2308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002308 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | low | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | n/a | **OS** | n/a | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp ifft_assigns.c -wp-prop check -wp-prover cvc4" on the attached file proved \false in line 339, which was intentionally inserted as a consistency check at the file's end. The reason for the inconsistency turned out to be a missing variable in a loop assigns clause (commented out for demo purposes in line 237). The detailled argument doesn't matter here; nevertheless it is given in (*) below for convenience.
I guess it would be easy for Frama-C to perform some coarse data-flow analysis and issue a warning about "nu2" being modified in line 295, but missing in the "loop assigns" clauses for the loop in line 242-302. Such an analysis could ignore nontrivial aliases, dead code, and array subranges, thus making it straight-forward to implement.
The example shows the value of warnings that such an analysis is able to issue. Already in this tiny example, it is easy to lose overview (cf. the many experimental "asserts", most of which a probably unncessary, or even nonsensical), and any tool help that doesn't cost much additional computation time is appreciated.
As a further application, it could print suggestions for "assigns" clauses of loops and procedure contracts.
(*): In fact, property "a2" from line 214 implies "nu1!=65536", if the latter variable remained unchanged during the loop in line 242-302, then property "c2" in line 232 boild down to "nu1+l==nu", which is false after the loop since then the termination condition "nu<l" has to hold, and "nu1" is unsigned.
## Attachments
- [ifft_assigns.c](/uploads/c813b7d252cb81e38d9f4fe871139244/ifft_assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/336naming the default behavior influences proven obligations2021-04-15T09:29:03ZJochen Burghardtnaming the default behavior influences proven obligationsID0002309:
**This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002309:
**This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002309 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp ilog2_beh.c -wp-prop ilog2 -wp-prover alt-ergo -wp-prover cvc4" on the attached program proves everything except (the lemmas and) loop invariant "a".
However, when lines 16,27,30,36,41 are uncommented, i.e. the default behavior is assigned an explicit name, everything except (the lemmas and) the loop variant is proven instead.
Naming vs. not naming a behavior shouldn't have such an influence.
## Attachments
- [ilog2_beh.c](/uploads/61d5de2e4e4cfecc8959933e484a3108/ilog2_beh.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/334poor errors message texts for Hoare memory model checks2021-09-21T13:21:18ZJochen Burghardtpoor errors message texts for Hoare memory model checksID0002311:
**This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002311:
**This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002311 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | sometimes |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-model Hoare memmodel_Hoare.c" on the attached program produces the output:
...
[rte] annotating function foo
memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:8:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:8:[wp] warning: No validity
memmodel_Hoare.c:4:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:3:[wp] warning: No validity
[wp] 4 goals scheduled
...
The name of the memory model is "Hoare" on the command line and in the WP manual (Sect.3.2, p.44), but it is called "Empty" in the error message output.
Moreover, the message "No validity" should be expanded to be more understandable. As an additional convenience, Frama-C could mention in each message the variable it refers to ("x" resp. "*x") in all cases in the example).
## Attachments
- [memmodel_Hoare.c](/uploads/913f6495cac3874938af5d592e39d609/memmodel_Hoare.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/333false postcondition shouldn't be verified in default memory-model setting2021-04-15T09:30:17ZJochen Burghardtfalse postcondition shouldn't be verified in default memory-model settingID0002312:
**This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002312:
**This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002312 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte memmodel_default.c" verifies all 11 proof obligations, while the assert clase in line 21 is obviously violated. The reason for Frama-C's behavior is that it assumes the "Hoare Variables mixed with Pointers" memory model as a default (in accordance with WP manual sect.3.4, p.45) without checking its preconditions, viz. the absence of any address-taking of a variable.
A novice user who doesn't yet know about the subtleties of memory models will assume after the above Frama-c run that the program is ok, as is has been formally verified. This may build up unjustified trust in the program, and discredit Frama-C (or even the whole field of formal methods) once the bug is detected at runtime, possibly causing severe damage.
I suggest to either
1. check the applicability of the "Hoare Variables mixed with Pointers" model (this should be easily achievable, if only the source code needs to be scanned for a unary "&"), or
2. use another, less restrictive, model as default.
## Attachments
- [memmodel_default.c](/uploads/05c89d93d3c5c3dde72d94f83901958d/memmodel_default.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/332value analysis introduces weird pointer assert with variable length arrays2021-02-22T12:59:35Zmantis-gitlab-migrationvalue analysis introduces weird pointer assert with variable length arraysID0002137:
**This issue was created automatically from Mantis Issue 2137. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002137:
**This issue was created automatically from Mantis Issue 2137. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002137 | Frama-C | Plug-in > Eva | public | 2015-06-26 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rcl | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
The value analysis plugin generates an assertion of the form
/*@ assert
Value: ptr_comparison:
\pointer_comparable((void *)*(arr+0), (void *)val);
*/
when arr is a VLA. This assertion looks bogus; it doesn't make any sense and doesn't even type check.
### Steps To Reproduce :
Run the value analysis plugin on the attached source code form.
## Attachments
- [ptrcmp.c](/uploads/11abeaa22c5401127f5cbb7d5985a107/ptrcmp.c)
- [ptrcmp.2.c](/uploads/4f5a1ba7e847d9950b81756c1170a3f0/ptrcmp.2.c)https://git.frama-c.com/pub/frama-c/-/issues/331suggestions for improvement of Sect.3.6 and 3.7 of the wp manual2023-07-24T10:43:54ZJochen Burghardtsuggestions for improvement of Sect.3.6 and 3.7 of the wp manualID0002313:
**This issue was created automatically from Mantis Issue 2313. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002313:
**This issue was created automatically from Mantis Issue 2313. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002313 | Frama-C | Documentation > manuals | public | 2017-06-15 | 2017-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | wp-manual-Phosphorus-20170501.pd | **OS** | n/a | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the WP manual, section 3.6 "The Typed Memory Model", instead of explaining the "Typed" memory model, refers to an old "Store" memory model and only describes the differences. However, few (and increasingly fewer) users are familiar with that old model, let alone availability issues of old WP manuals. Therefore, the "Typed" model should be described from scratch. Also, the section should initially state that it is about the model named "Typed".
In section 3.7, I found the following senteces hard to understand, and added my questions in "{}":
This detection is more clever than the standard one {That is, the one of the "Typed" model?} since it only takes into account local usage {What is local and global usage of a function? How can an approach being more clever than another one although it is based on less information?} of each function (not global ones).
Additionally, the Caveat memory model of Frama-C performs a local allocation {What is a local allocation? Shouldn't Frama-C's allocation reflect those made by the C compiler, which pushes actual parameters on the local stack in a new stack-frame, and expects formal parameters on the local stack in the current stack frame?} of formal parameters with pointer types that cannot be treated as reference parameters.
This makes explicit the separation hypothesis of memory regions pointed by formals in the Caveat tool. The major benefit of the WP version {Compared to what? To the Caveat tool? To the plain "Typed" model?} is that aliases are taken into account by the Typed memory model, hence, there are no more suspicious aliasing warnings.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/330unsoundness after external function call2021-02-22T12:59:30Zmantis-gitlab-migrationunsoundness after external function callID0002315:
**This issue was created automatically from Mantis Issue 2315. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002315:
**This issue was created automatically from Mantis Issue 2315. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002315 | Frama-C | Plug-in > Eva | public | 2017-07-01 | 2017-07-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | maxime | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi everyone,
Frama-C is unsound after an external function call. See the attached file.
Running frama-c -val unsound.c gives me:
[value] Called Frama_C_show_each_r({1})
This is wrong. The call to the external function f can update **x, and so *y can be anything.
At the call to f(x), I think you should grab all the base addresses that are reachable by the arguments and set them to TOP.
### Steps To Reproduce :
frama-c -val unsound.c
## Attachments
- [unsound.c](/uploads/f18a6127d86087eb32b6b831193aceb8/unsound.c)https://git.frama-c.com/pub/frama-c/-/issues/328suggest to clarify semantics of statement contract in ACSL implementation manual2021-02-22T14:01:24ZJochen Burghardtsuggest to clarify semantics of statement contract in ACSL implementation manualID0002300:
**This issue was created automatically from Mantis Issue 2300. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002300:
**This issue was created automatically from Mantis Issue 2300. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002300 | Frama-C | Documentation > ACSL | public | 2017-05-11 | 2017-07-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | patrick | **Resolution** | no change required |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | Silicon/Phosphorus | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
We were wondering about the semantical difference between assertions and a statement contract. Therefore, we ran "frama-c -wp contractTest.c" on the attached program (Frama-c version Phosphorus-20170501-beta1). The assertion "bar" couldn't be proven (without the statement contract, it could). This supports our hypothesis that a statement contract completely overrides the standard Hoare-calculus semantics.
However, this isn't explicitly stated in the ACSL Implementation manual (version Silicon-20161101), where statement contracts are mentioned on p.12 and 36, and mainly in their own section (2.4.4) on p.44-45.
We therefore wonder if the observed "override behavior" is just special to the WP plugin, or if it is part of the ACSL language definition and obligatory for all plug-ins. An appropriate sentence in section 2.4.4 could clarify this question.
## Attachments
- [contractTest.c](/uploads/2b83abb09390db63e48f41428c49a323/contractTest.c)https://git.frama-c.com/pub/frama-c/-/issues/327Statement contracts and WP2023-07-24T10:25:01ZJens GerlachStatement contracts and WPID0002317:
**This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002317:
**This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002317 | Frama-C | Documentation > manuals | public | 2017-07-18 | 2017-07-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a follow-up on issue https://bts.frama-c.com/view.php?id=2300 which was rather briskly closed.
I can understand that the question on the semantics of statement contracts in WP is not discussed in the ACSL implementation manual. However, in my opinion, it should then be discussed in the WP manual.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/324statement contract apparently confuses parser2021-04-15T09:31:56ZJochen Burghardtstatement contract apparently confuses parserID0002301:
**This issue was created automatically from Mantis Issue 2301. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002301:
**This issue was created automatically from Mantis Issue 2301. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002301 | Frama-C | Plug-in > wp | public | 2017-05-11 | 2017-07-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp assigns.c" on the attached program produces a warning:
assigns.c:12:[wp] warning: Missing assigns clause (assigns 'everything' instead)
The warning is unjustified since the loop in line 12 does have a "loop assigns" clauses, and loops don't use (plain) "assigns" clauses.
If the trivial assertion in line 9 is activated, the warning disappears, and everything is proven.
If instead the braces in line 5 and 7 are removed, Frama-c reports a crash (text see "Additional Information").
### Additional Information :
Crash message:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing assigns.c (with preprocessing)
[wp] failure: Several assigns ?
[kernel] Current source was: assigns.c:2
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 568, characters 30-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 15-16
Called from file "src/plugins/wp/wpStrategy.ml", line 470, characters 13-63
Called from file "src/plugins/wp/wpStrategy.ml", line 505, characters 8-34
Called from file "list.ml", line 73, characters 12-15
Called from file "src/plugins/wp/wpStrategy.ml", line 541, characters 2-34
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/wpAnnot.ml", line 1023, characters 2-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1094, characters 15-41
Called from file "src/plugins/wp/wpAnnot.ml", line 1273, characters 14-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1274, characters 9-22
Called from file "src/plugins/wp/wpAnnot.ml", line 1363, characters 2-47
Called from file "map.ml", line 168, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [assigns.c](/uploads/f5df9089249e50094cfbca65b1a403f3/assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/323Configure step fails on bytecode architectures2021-02-22T12:59:21Zmantis-gitlab-migrationConfigure step fails on bytecode architecturesID0001763:
**This issue was created automatically from Mantis Issue 1763. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001763:
**This issue was created automatically from Mantis Issue 1763. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001763 | Frama-C | Kernel > configure | public | 2014-04-28 | 2017-08-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The configure step fails on pure bytecode architectures with the following message:
checking for /usr/lib/ocaml/ocamlgraph/graph.cmo... yes
configure: OcamlGraph 1.8.5 > 1.8.4 found: should be compatible, but no warranty. Use it at your own risk!
configure: OcamlGraph 1.8.5 is incompatible with Frama-C.
configure: switching to OcamlGraph provided by Frama-C
checking for ocamlgraph... no
checking for ocamlgraph.tar.gz... no
configure: error: cannot find OcamlGraph in the current directory.
Quite strange: would your Frama-C distribution be corrupted?
Anyway:
1. download the latest version from http://ocamlgraph.lri.fr/download
2. install it by './configure && make && make install'
3. rerun ./configure here
make[1]: *** [override_dh_auto_configure] Error 1
It is due to the fact that the script tries to compile a test program linking against the OCamlgraph library in the native case and calls ocamlgraph_error in the bytecode case instead of trying to compile the test program.
In order to make Frama-C build on bytecode architecture, I've disabled that call to ocamlgraph_error.https://git.frama-c.com/pub/frama-c/-/issues/322Port to OCaml 4.052021-02-22T12:59:20Zmantis-gitlab-migrationPort to OCaml 4.05ID0002324:
**This issue was created automatically from Mantis Issue 2324. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002324:
**This issue was created automatically from Mantis Issue 2324. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002324 | Frama-C | Kernel | public | 2017-08-11 | 2017-08-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
In order to make Frama-C build with OCaml 4.05. Please a find patch attached that introduces a few minor changes and make it compile again.
## Attachments
- [0007-Fix-FTBFS-with-OCaml-4.05.0.patch](/uploads/03c4935869f9dc001ab55e76af16df0b/0007-Fix-FTBFS-with-OCaml-4.05.0.patch)https://git.frama-c.com/pub/frama-c/-/issues/321Value.cmo needs LoopAnalysis.cmo2021-02-22T12:59:17Zmantis-gitlab-migrationValue.cmo needs LoopAnalysis.cmoID0002326:
**This issue was created automatically from Mantis Issue 2326. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002326:
**This issue was created automatically from Mantis Issue 2326. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002326 | Frama-C | Plug-in > Eva | public | 2017-08-11 | 2017-09-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Value plugin needs LoopAnalysis, but appears first during the linking
phase. In order to workaround that, we move it before Value.cmo in the
PLUGIN_CMO_LIST variable.
Please find attached a simple patch which fixes this in the Makefile.
## Attachments
- [0005-Value.cmo-needs-LoopAnalysis.cmo.patch](/uploads/10d367477191926bad9aa0e5fae200dd/0005-Value.cmo-needs-LoopAnalysis.cmo.patch)https://git.frama-c.com/pub/frama-c/-/issues/320Spelling errors2021-02-22T12:59:16Zmantis-gitlab-migrationSpelling errorsID0002323:
**This issue was created automatically from Mantis Issue 2323. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002323:
**This issue was created automatically from Mantis Issue 2323. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002323 | Frama-C | Documentation | public | 2017-08-11 | 2017-09-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Hi,
I've found some spelling errors in Frama-C's source code. Please find attached a patch to fixe them.
## Attachments
- [0008-More-fixes-of-spelling-errors.patch](/uploads/202926e102b518e7e14b24d4d1de7011/0008-More-fixes-of-spelling-errors.patch)
- [0001-Fix-spelling-error-in-binary.patch](/uploads/78cca8ddcb2d7003d2128aae12eb17ce/0001-Fix-spelling-error-in-binary.patch)https://git.frama-c.com/pub/frama-c/-/issues/319Make it build on bytecode architectures2021-02-22T12:59:14Zmantis-gitlab-migrationMake it build on bytecode architecturesID0002325:
**This issue was created automatically from Mantis Issue 2325. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002325:
**This issue was created automatically from Mantis Issue 2325. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002325 | Frama-C | Graphical User Interface | public | 2017-08-11 | 2017-09-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Hi,
Frama-C's GUI doesn't build on bytecode only architecture because the Makefile always depend on TARGET_GUI which may contain native objects.
Please find attached a simple patch that fixes this issue.
## Attachments
- [0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch](/uploads/1f211d8c6be79ada3a7ab5a60cd9838e/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch)https://git.frama-c.com/pub/frama-c/-/issues/318Duplicates are created on the tab "Messages"2022-09-28T11:26:37Zmantis-gitlab-migrationDuplicates are created on the tab "Messages"ID0002276:
**This issue was created automatically from Mantis Issue 2276. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002276:
**This issue was created automatically from Mantis Issue 2276. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002276 | Frama-C | Graphical User Interface | public | 2017-02-03 | 2017-11-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | maroneze | **Resolution** | reopened |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
New messages append to old messages on the tab "Messages" if an analysis are rerun with new options.
### Steps To Reproduce :
1. Run Value analysis.
2. Change any option.
3. Run Value analysis.Andre MaronezeAndre Maroneze