frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:08:16Zhttps://git.frama-c.com/pub/frama-c/-/issues/657logic function with typedef'd result type causes crash2021-02-22T13:08:16ZJochen Burghardtlogic function with typedef'd result type causes crashID0002056:
**This issue was created automatically from Mantis Issue 2056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002056:
**This issue was created automatically from Mantis Issue 2056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002056 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 437.cpp (external front-end)
Now output intermediate result
437.cpp:6:[fclang] failure: predicate definition with a term as body
[kernel] Current source was: 437.cpp:6
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 622, characters 12-76
Called from file "src/frama-clang/convert.ml", line 2233, characters 18-54
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2241, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2554, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2558, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
The problem disappears if the return type is changed to "int" in line 6.
Line 7 just demonstrates that the same expression is accepted in C++ code.
## Attachments
- [437.cpp](/uploads/b80e0c84f1ccd4254f37a850575ad463/437.cpp)https://git.frama-c.com/pub/frama-c/-/issues/656extra "//" comment within "//@" annotation causes abort2021-02-22T13:08:15ZJochen Burghardtextra "//" comment within "//@" annotation causes abortID0002013:
**This issue was created automatically from Mantis Issue 2013. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002013:
**This issue was created automatically from Mantis Issue 2013. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002013 | Frama-Clang | Plug-in > clang | public | 2014-12-04 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
framaCIRGen: src/frama-clang/ACSLToken.h:563: Acsl::DLexer::AbstractToken Acsl::DLexer::Token::getFullToken() const: Assertion `_type != 0' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if "// comment" is deleted in line 2, or if the file is renamed to "190.c".
## Attachments
- [190.cpp](/uploads/6e7ae2cf72d87f620e534fcf2c6a03dd/190.cpp)https://git.frama-c.com/pub/frama-c/-/issues/654"__is_trivial" causes abort2021-02-22T13:08:13ZJochen Burghardt"__is_trivial" causes abortID0001967:
**This issue was created automatically from Mantis Issue 1967. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001967:
**This issue was created automatically from Mantis Issue 1967. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001967 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Unsupported expressions:UnaryTypeTraitExpr 0x253e888 <134.cpp:2:10, col:26> '_Bool'
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
(Importance: this code is used via #include <vector>.)
## Attachments
- [134.cpp](/uploads/fc0e0514a33ec9a94e33e11fd592e5b0/134.cpp)https://git.frama-c.com/pub/frama-c/-/issues/641no label accepted in "assigns \nothing"2021-02-22T13:07:56ZJochen Burghardtno label accepted in "assigns \nothing"ID0002113:
**This issue was created automatically from Mantis Issue 2113. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002113:
**This issue was created automatically from Mantis Issue 2113. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002113 | Frama-Clang | Kernel | public | 2015-05-04 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c 478.c" on the attached program yields the output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 478.c (with preprocessing)
478.c:6:[kernel] user error: unexpected token '\nothing'
[kernel] user error: stopping on file "478.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
Some modifications, using / omitting a label, using "\nothing" / a variable name have been tried, and the result is documented in the respetive line of the file. It seems that "\nothing" is accepted by the parser only immediately after "assigns", such that not even a label is accepted in between.
## Attachments
- [478.c](/uploads/589fcbdd46108b9edbc78f9b7106b8f7/478.c)https://git.frama-c.com/pub/frama-c/-/issues/631*i == *j cannot be proven from i == j2021-02-22T13:07:43Zmantis-gitlab-migration*i == *j cannot be proven from i == jID0002128:
**This issue was created automatically from Mantis Issue 2128. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002128:
**This issue was created automatically from Mantis Issue 2128. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002128 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | virgile | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Nitrogen-20111001
alt-ergo 0.94
The following assertion cannot be proven.
void pointer_testcase(int *i, int *j) {
/*@ assert i == j ==> *i == *j; */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [pointer_testcase.c](/uploads/ec0d97eb74499b149912f74f57f48a94/pointer_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/628*off == off_cpy cannot be proven just after the assignment *off = off_cpy2021-02-22T13:07:41Zmantis-gitlab-migration*off == off_cpy cannot be proven just after the assignment *off = off_cpyID0002130:
**This issue was created automatically from Mantis Issue 2130. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002130:
**This issue was created automatically from Mantis Issue 2130. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002130 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Nitrogen-20111001
alt-ergo 0.94
#include <stddef.h>
/*
* Can memory zones be declared disjoint? For instance:
* \disjoint(off, buf + *off)
*
* wp does not accept and thus gracefully skips the following try:
* @ requires \forall size_t i;
* 0 <= i < sizeof(*off) ==> (char *) off != buf + (*off + i);
*/
/*@
@ requires \valid(off) && \valid(buf + *off);
@ assigns *off, buf[*off];
@ ensures *off == \old(*off) + 1;
@ ensures buf[\old(*off)] == '\0';
@*/
void alias_testcase_0(char *const buf, size_t *const off) {
size_t off_cpy = *off; /* restricted pointers cannot be required */
buf[off_cpy++] = '\0';
/*@ assert off_cpy - 1 == \at(*off, Pre); */ /* OK */
/*@ assert buf[off_cpy - 1] == '\0'; */ /* OK */
*off = off_cpy;
/*@ assert *off == off_cpy; */ /* NOK, cannot be proven */
/*@ assert buf[\at(*off, Pre)] == '\0'; */ /* NOK, cannot be proven */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [alias_testcase.c](/uploads/65a0be19399d07141588a8edf1eeb1c0/alias_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/627Range of remainder of two positive integers, wrong and missing assertions.2021-02-22T13:07:39Zmantis-gitlab-migrationRange of remainder of two positive integers, wrong and missing assertions.ID0002129:
**This issue was created automatically from Mantis Issue 2129. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002129:
**This issue was created automatically from Mantis Issue 2129. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002129 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Nitrogen-20111001
alt-ergo 0.94
False negative and false positive int the following code.
/*@ requires 0 <= n; */
void modulo_testcase_0(unsigned n) {
/*@ ghost unsigned q = n / 2; */
/*@ ghost unsigned r = n % 2; */
/*@ assert 0 <= n; */ /* OK */
/*@ assert n == 2*q + r; */ /* OK */
/*@ assert 0 <= q; */ /* OK */
/*@ assert 0 <= r < 1; */ /* NOK, cannot be proven */
}
/*@ requires 0 <= n && 0 < d; */
void modulo_testcase_1(int n, int d) {
/*@ assert n <= d * (n / d); */ /* NOK, cannot be proven */
/*@ ghost int q = n / d; */ /* OK */
/*@ ghost int r = n % d; */ /* OK */
/*@ assert 0 <= r < 1; */ /* NOK, r < d is true */
/*@ assert n <= d * (n / d); */ /* OK */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [modulo_testcase.c](/uploads/b725efd4758f124867c970e99d059011/modulo_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/623Frama-C GUI crashes under OS X2021-02-22T13:07:34ZJens GerlachFrama-C GUI crashes under OS XID0002099:
**This issue was created automatically from Mantis Issue 2099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002099:
**This issue was created automatically from Mantis Issue 2099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002099 | Frama-C | Graphical User Interface | public | 2015-03-31 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
If I start the Frama-C GUI on the attached program with 'frama-c-gui lemma.c',
then the GUI starts normally.
In the 'Source' panel I can see 'lemma.c.
When I try to see the lemma inside the file by clicking on the filename (or the little triangle left of it),
then the GUI crashes.
This does not happen under Linux.
### Additional Information :
frama-c was installed with opam
OS X (10.10.3 (14D127a))
opam --version: 1.2.0
frama-c -version
Version: Sodium-20150201
Compilation date: Tue Mar 31 09:48:58 CEST 2015
## Attachments
- [lemma.c](/uploads/f1e70f11f828611cc31af293e127a3c4/lemma.c)https://git.frama-c.com/pub/frama-c/-/issues/618Sessions and WP do not interact properly2021-02-22T13:07:24Zmantis-gitlab-migrationSessions and WP do not interact properlyID0002044:
**This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002044:
**This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002044 | Frama-C | Plug-in > wp | public | 2015-01-06 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | correnson | **Resolution** | no change required |
| **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 :
Bonjour, quelques problèmes avec le -save et le -load des sessions conjugés avec WP/Why3 et l'option no-let !!!!
1. Si on utilise pas -wp-out les fichiers temporaires de wp sont supprimés et lors du prochain appel de frama-c avec le -load, il se plaint de l'absence des fichiers
2. Si on specifie -wp-out, avec le -load, Frama-C retrouve les fichiers générés mais il ne semble pas retrouver tout ce dont il a besoin.
3. Enfin lors de l'utilisation de coq comme prover lors d'un run (avec -load et -save), au prochain appel avec toujours -load et -save, frama-c appelle systématiquement coq, y compris si on specifie -wp-prover altergo par exemple.
### Steps To Reproduce :
Pour les points 1 et 2:
Par exemple, pour le fichier C suivant:
$ cat essai.c
struct greycounter_mem {_Bool _first; };
/*@ requires \valid(self);
@ ensures ((*self)._first ==1);
@ assigns *self;*/
void greycounter_reset (struct greycounter_mem *self) {
self->_first = 1;;
return;
}
Le script suivant active les différents problemes:
#!bin/bash
src=essai.c
# Error 1: temporary wp folder with no-let option and why3 solver (eg. altergo or CVC4)
frama-c -save session -wp-prop "@ensures" -wp-prover why3:altergo -wp-no-let $src
frama-c -load session -save session -wp-prop "@assigns" $src
# Error 2: no-let with why3:cvc4
frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-no-let -wp-out wp
frama-c -load session -save session -wp-prop "@assigns" $src
# Here it works
frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-out wp
frama-c -load session -save session -wp-prop "@assigns" $srchttps://git.frama-c.com/pub/frama-c/-/issues/617deficient axioms2021-02-22T13:07:23ZDavid Cokdeficient axiomsID0002138:
**This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002138:
**This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002138 | Frama-C | Plug-in > wp | public | 2015-06-29 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The proof of the following with -WP and alt-ergo fails:
/*@
requires (int)(x+y) == x+y;
ensures \result == x+y;
*/
int f(int x, int y) {
return x+y;
}
On inspecting the intermediate artifacts, we identified the problem as inadequate axioms. Two solutions requiring changes in axioms worked for us.
However, I don't know if either change would have wider ramifications.
1)
axiom is_to_sint32 :
(forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))
The effect of the triggers in this axiom is simply to allow is_sint32(to_sint32(x)) to be reduced to true. In fact the more common need is to know that to_sint32(x) satisfies is_sint32. The proof above goes through if the trigger is changed to
axiom is_to_sint32 :
(forall x:int [to_sint32(x)]. is_sint32(to_sint32(x)))
2)
axiom id_sint32 :
(forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and
(x < 2147483648)) -> (to_sint32(x) = x)))
This axiom is much more useful if it is written as an equivalence instead of an implication. Doing so also enables the proof of the program above to go through.https://git.frama-c.com/pub/frama-c/-/issues/83wrong test path given in Compiling from source - Quick Start"2021-02-22T13:07:21Zmantis-gitlab-migrationwrong test path given in Compiling from source - Quick Start"ID0002469:
**This issue was created automatically from Mantis Issue 2469. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002469:
**This issue was created automatically from Mantis Issue 2469. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002469 | Frama-C | Documentation > website | public | 2019-08-07 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abutterfield | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
In
https://frama-c.com/install-19.0-Potassium.html#compiling-from-source
step 6 suggests a test involving "tests/misc/CruiseControl*.c".
In the Potassium distribution, that needs to be "tests/value/CruiseControl*.c".
I installed from source as a non-superuser, which works
### Steps To Reproduce :
Follow the Quick Start instructions - or simple look at the contents of tests/misc and tests/value in the source distribution.https://git.frama-c.com/pub/frama-c/-/issues/604suggest to warn about ensures clauses containing only \old variables2021-02-22T13:06:57ZJochen Burghardtsuggest to warn about ensures clauses containing only \old variablesID0001017:
**This issue was created automatically from Mantis Issue 1017. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001017:
**This issue was created automatically from Mantis Issue 1017. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001017 | Frama-C | Kernel > ACSL implementation | public | 2011-11-10 | 2015-08-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
A novice student wrote "ensures 0<=\old(n)<10;" when he actually meant "requires 0<=n<10;" in his solution to an Acsl exercise.
As this kind of error can be detected easily (ensures clauses should contain at least one identifier outside of \old), I suggest to add a warning in these cases.
See attached file for an own minimal example.
## Attachments
- [ftest.c](/uploads/843b644ab8a3c44a7e6e286c4b05969e/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/597typo in grammar2021-02-22T13:06:42ZDavid Coktypo in grammarID0001784:
**This issue was created automatically from Mantis Issue 1784. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001784:
**This issue was created automatically from Mantis Issue 1784. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001784 | Frama-C | Documentation > ACSL | public | 2014-05-25 | 2015-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The ACSL Neon documentation, in Fig 2.12, uses 'lemma-def' but defines 'lemma-decl'.
Presumably these should both be 'lemma-def'https://git.frama-c.com/pub/frama-c/-/issues/591set of set2021-02-22T13:06:36ZPatrick Baudinset of setID0000575:
**This issue was created automatically from Mantis Issue 575. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000575:
**This issue was created automatically from Mantis Issue 575. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000575 | Frama-C | Kernel > ACSL implementation | public | 2010-08-25 | 2015-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
For exemple, there is not way to build the set containing the empty set without using comprehension set construct.
The proposition is to extend the actual ACSL grammar in order to allow "{" term "}" as set expression.https://git.frama-c.com/pub/frama-c/-/issues/565Symbolic links in tar ball2021-02-22T13:05:59Zmantis-gitlab-migrationSymbolic links in tar ballID0002121:
**This issue was created automatically from Mantis Issue 2121. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002121:
**This issue was created automatically from Mantis Issue 2121. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002121 | Frama-C | Kernel | public | 2015-05-26 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dirkx | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | all | **OS** | all | **OS Version** | all |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Magnesium | **Fixed in Version** | Frama-C Magnesium |
### Description :
The tarball has symbolic links from the files to the file itself for all files in bin.
Depending on the unpacking strategy; this may unlink the actual file (as the symlink request to link the now unexisting file to itself fails).
### Additional Information :
hrwxr-xr-x 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/lithium2beryllium.sh link to frama-c-Sodium-20150201/bin/lithium2beryllium.sh
hrwxr-xr-x 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/neon2sodium.sh link to frama-c-Sodium-20150201/bin/neon2sodium.sh
hrwxr-xr-x 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/boron2carbon.sh link to frama-c-Sodium-20150201/bin/boron2carbon.sh
hrwxr-xr-x 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/oxygen2fluorine.sh link to frama-c-Sodium-20150201/bin/oxygen2fluorine.sh
hrwxr-xr-x 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/carbon2nitrogen.sh link to frama-c-Sodium-20150201/bin/carbon2nitrogen.sh
hrwxr-xr-x 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/nitrogen2oxygen.sh link to frama-c-Sodium-20150201/bin/nitrogen2oxygen.sh
hrwxr-xr-x 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/fluorine2neon.sh link to frama-c-Sodium-20150201/bin/fluorine2neon.sh
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/share/Makefile.plugin link to frama-c-Sodium-20150201/share/Makefile.plugin
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/share/Makefile.dynamic link to frama-c-Sodium-20150201/share/Makefile.dynamic
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/share/Makefile.dynamic_config.external link to frama-c-Sodium-20150201/share/Makefile.dynamic_config.external
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/share/Makefile.dynamic_config.internal link to frama-c-Sodium-20150201/share/Makefile.dynamic_config.internal
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/hptmap.ml link to frama-c-Sodium-20150201/external/hptmap.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/hptmap.mli link to frama-c-Sodium-20150201/external/hptmap.mli
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/unmarshal_test.ml link to frama-c-Sodium-20150201/external/unmarshal_test.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/unmarshal_nums.ml link to frama-c-Sodium-20150201/external/unmarshal_nums.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/unmarshal_nums.mli link to frama-c-Sodium-20150201/external/unmarshal_nums.mli
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/unmarshal.ml link to frama-c-Sodium-20150201/external/unmarshal.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/unmarshal.mli link to frama-c-Sodium-20150201/external/unmarshal.mli
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/unmarshal_hashtbl_test.ml link to frama-c-Sodium-20150201/external/unmarshal_hashtbl_test.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/unz.ml link to frama-c-Sodium-20150201/external/unz.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/unz.mli link to frama-c-Sodium-20150201/external/unz.mli
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/sysutil.ml link to frama-c-Sodium-20150201/external/sysutil.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/external/sysutil.mli link to frama-c-Sodium-20150201/external/sysutil.mli
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/sed_get_make_major link to frama-c-Sodium-20150201/bin/sed_get_make_major
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/bin/sed_get_make_minor link to frama-c-Sodium-20150201/bin/sed_get_make_minor
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/opam/files/run_autoconf_if_needed.ml link to frama-c-Sodium-20150201/opam/files/run_autoconf_if_needed.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/src/lib/integer.ml.zarith link to frama-c-Sodium-20150201/src/lib/integer.ml.zarith
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/src/lib/integer.ml.bigint link to frama-c-Sodium-20150201/src/lib/integer.ml.bigint
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/src/memory_state/inout_type.ml link to frama-c-Sodium-20150201/src/memory_state/inout_type.ml
hrw-r--r-- 0 bobot bobot 0 Mar 6 16:28 frama-c-Sodium-20150201/src/memory_state/inout_type.mli link to frama-c-Sodium-20150201/src/memory_state/inout_type.mli
### Steps To Reproduce :
untar using a plain tar.https://git.frama-c.com/pub/frama-c/-/issues/551Incorrect grammar of Predicate Application and Function Application2021-02-22T13:05:40Zmantis-gitlab-migrationIncorrect grammar of Predicate Application and Function ApplicationID0002143:
**This issue was created automatically from Mantis Issue 2143. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002143:
**This issue was created automatically from Mantis Issue 2143. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002143 | Frama-C | Documentation > ACSL | public | 2015-07-06 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Magnesium | **Fixed in Version** | Frama-C Magnesium |
### Description :
Following is the grammar of Function Application in acsl-1.9.pdf in Fig 2.1:
term :: = id (term (, term)*)
and grammar of predicate application is :
pred ::= id (term (, term)*)
But a function application/predicate application can include label-binders like:
For function definition :
logic integer max{L}(integer n1, integer n2 ) = (n1 <=n2)? n2 : n1;
we can call this function as:
ensures max{L}(n1, n2);
Grammar of function application/predicate application should include label-binders.https://git.frama-c.com/pub/frama-c/-/issues/550Crash with \is_infinite2021-02-22T13:05:39Zmantis-gitlab-migrationCrash with \is_infiniteID0002082:
**This issue was created automatically from Mantis Issue 2082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002082:
**This issue was created automatically from Mantis Issue 2082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002082 | Frama-C | Plug-in > wp | public | 2015-02-24 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Using the built-in \is_infinite causes wp to crash.
This is used in the provided libc specifications (math.h), and a call to these functions will cause a crash.
### Steps To Reproduce :
Create program:
#include <math.h>
/*@
ensures \true;
*/
void main() {
double val = acos(1);
}
Run frama-c, where FRAMA_C_LIBC is .../frama-c-Neon-20140301/share/libc:
frama-c -cpp-extra-args="-I${FRAMA_C_LIBC}" -wp is_infinte_test.c
Get output:
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acos, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosh, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acoshf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acoshl, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosl, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asin, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asinf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asinl, generating default assigns from the specification
[wp] warning: No definition for 'memchr' interpreted as reads nothing
[wp] warning: No definition for 'memset' interpreted as reads nothing
[wp] warning: No definition for 'strchr' interpreted as reads nothing
[wp] warning: No definition for 'strcmp' interpreted as reads nothing
[wp] warning: No definition for 'wcscmp' interpreted as reads nothing
[wp] warning: No definition for 'wcslen' interpreted as reads nothing
[wp] warning: No definition for 'wcsncmp' interpreted as reads nothing
[wp] warning: Missing RTE guards
[wp] user error: Builtin \is_infinite(float64) not defined
[wp] failure: Logic '\is_infinite' undefined
[kernel] Current source was: is_infinte_test.c:8
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/wp/LogicCompiler.ml", line 698, characters 20-51
Called from file "src/wp/LogicCompiler.ml", line 758, characters 10-23
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "list.ml", line 57, characters 20-23
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/cfgWP.ml", line 1069, characters 18-63
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 1099, characters 23-207
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/calculus.ml", line 448, characters 14-224
Called from file "src/wp/calculus.ml", line 595, characters 10-57
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 699, characters 40-59
Called from file "set.ml", line 288, characters 38-41
Called from file "map.ml", line 169, characters 20-25
Called from file "map.ml", line 169, characters 10-18
Called from file "map.ml", line 169, characters 10-18
Called from file "src/wp/calculus.ml", line 699, characters 4-64
Called from file "src/wp/calculus.ml", line 745, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 17-42
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 29-31
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
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
Plug-in wp aborted: internal error.
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_guidelineshttps://git.frama-c.com/pub/frama-c/-/issues/548Typos and Grammatical corrections for the ACSL 1.9 manual2021-02-22T13:05:35ZDavid CokTypos and Grammatical corrections for the ACSL 1.9 manualID0002115:
**This issue was created automatically from Mantis Issue 2115. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002115:
**This issue was created automatically from Mantis Issue 2115. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002115 | Frama-C | Documentation > ACSL | public | 2015-05-05 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Magnesium | **Fixed in Version** | Frama-C Magnesium |
### Description :
These are a set of typos and grammatical errors I noted on a recent read of most of the ACSL 1.9 manual. None of these affect technical correctness - just the flow of the English. I put them here simply to be helpful. Do what you like with them.
If you like, I am happy to edit them into a version-controlled copy of the document source myself, if you would like.
Typos & Grammatical corrections
p.13: "used in position of a term or a predicate" -> "used in the position of a term or a predicate"
p. 17: "name x for expression e1 which can be used in" -> "name x for expression e1 ; x can then be used in"
p. 17: "for readibility purposes" -> "for readability purposes"
p. 20, near end: "specified if divisor is" -> "specified if the divisor is"
p. 23: "involve any rounding nor overflow" -> "involve any rounding or overflow"
p. 23: "values which do not naturally" -> "values that do not naturally"
p. 23: "mode in C programs) If the source real number" -> "mode in C programs). If the source real number" (period added)
p. 26: "pointers can only refers" -> "pointers can only refer"
p. 27: "functional update of an union. For an object of an union" -> "functional update of a union. For an object of a union"
p. 27: "Then equality amounts the recursively check equality of fields." -> "Then equality amounts to recursively checking equality of fields."
p. 27: "C aggregates types" -> "C aggregate types"
p. 28: "only for arrays that lies in C" -> "only for arrays that lie in C"
p. 28: Did you intentionally omit the section on string literals? (2.2.8)
p. 29, last line: "Thus, \old construct is useless" -> "Thus, the \old construct is useless" (2 changes)
p. 30: "denotes the effective parameter of isqrt calls which" -> "denotes the effective parameter of isqrt calls, which" (comma expected here)
p. 30: "in the pre-state than in the post-state" -> "in the pre-state as in the post-state"
p. 33: "If such a condition is seeked," -> "If such a condition is desired,"
p. 34: "which are also usefull for \separated predicate" -> "that are also useful for the \separated predicate" (three changes)
p. 38: "that are not member of L." -> "that are not members of L."
p. 38: "is similar as above" -> "is similar to the above"
p. 38, Remarks: "locations that are not member of L" -> "locations that are not members of L"
p.43, last line: "but without decreases clause" -> "but without a decreases clause"
p. 44: "the begining of the annoted statement" -> "the beginning of the annotated statement" (two changes)
p. 47, last line: "These declarations follows the" -> "These declarations follow the"
p. 49, Example 2.39: "The following introduce" -> "The following introduces"
p. 50: "was also bases on definite Horn clauses thus consistent" -> "was also based on definite Horn clauses, and is thus consistent" (2 changes)
p. 51: "there is no syntactic conditions which would" -> "there is no syntactic conditions that would"
p. 52, Example 2.43: "Function that sums the element" -> "Function that sums the elements"
p. 54: "C types and logic types arguments" -> "C type and logic type arguments" or "C types and logic types as arguments"
p. 54: "Such an hybrid predicate" -> "Such a hybrid predicate"
p. 54: "an hybrid function" -> "a hybrid function"
p. 55, Example 2.46: "This second example defines a predicate which indicates" -> "This second example defines a predicate that indicates"
p. 55, Example 2.46: "one of the post condition" -> "one of the post conditions"
p. 55, "Logic declaration can be augmented" -> "Logic declarations can be augmented"
p. 55: "of an hybrid" -> "of a hybrid"
p. 56: "that is the set of memory locations which it depends on. From such an information" -> "that is, the set of memory locations that it depends on. From such information" (3 changes)
p. 57: "Grammar for terms and predicates" -> "The grammar for terms and predicates"
p. 57, at end of page: '(when the allocation succeed)" -> "(when the allocation succeeds)"
p. 58, at top of page: "All of them takes" -> "All of them take" or "Each of them takes"
p. 58, near bottom of page: "if there is no alignment constraints" -> "if there are no alignment constraints"
p. 59: "in the post-state than in the pre-state" -> "in the post-state as in the pre-state"
p. 61: "none of the two allocation clauses" -> "neither of the two allocation clauses"
p. 61: "That is equivalent to give allocates \nothing" -> "That is equivalent to stating allocates \nothing"
p. 63: "A loop-clause without allocation clause implicitly contents loop allocates \nothing" -> "A loop-clause without an allocation clause implicitly states loop allocates \nothing" (2 changes)
p. 64: "since union is made with a" -> "since the arguments of union are a"
p. 64: "accordingly to" -> "according to"
p. 65: "abrupt clause of a statement contracts" -> "abrupt clause of statement contracts"
p. 65: "e.g the value" -> "e.g. the value" (period added)
p. 72, near end: "semantical restrictions" -> "semantic restrictions"
p. 73: "execution This implies several conditions, including e.g:" -> "execution. This implies several conditions, including e.g.:" (two periods added)
p. 73: "Body of a ghost function is ghost code, hence do not modify" -> "The body of a ghost function is ghost code, and hence may not modify"
p. 74: "so as the ghost field of structures" -> "as do the ghost fields of structures"
p. 79: "functions and predicate over" -> "functions and predicates over"
p. 80, near end: "the pointer in argument is" -> "the pointer in the argument is"
p. 83: "in the future, and remain open" -> "in the future and remain open" (no comma)
p. 85: "The set of pure expression is a subset" -> "The set of pure expressions is a subset"https://git.frama-c.com/pub/frama-c/-/issues/547Incorrect result with X modulo 12021-02-22T13:05:33Zmantis-gitlab-migrationIncorrect result with X modulo 1ID0002141:
**This issue was created automatically from Mantis Issue 2141. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002141:
**This issue was created automatically from Mantis Issue 2141. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002141 | Frama-C | Plug-in > wp | public | 2015-07-01 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
WP concludes that “n % 1 == n”, instead of “n % 1 == 0” where n are integers.
This is only a problem with modulo 1, the correct answer is obtained for other integers, or if n is 0 (0 % 1 == 0).
This can be shown with the following lemmas.
/*@
lemma mod_one_error:
\forall integer i; (i % 1) == i;
*/
> frama-c mod.c -wp -wp-prop=@lemma
[kernel] preprocessing with "gcc -C -E -I. mod.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_lemma_mod_one_error : Valid
[wp] Proved goals: 1 / 1
Qed: 1
/*@
lemma mod_one:
\forall integer i; (i % 1) == 0;
*/
> frama-c mod.c -wp -wp-prop=@lemma
[kernel] preprocessing with "gcc -C -E -I. mod.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_mod_one : Unknown
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
I would have expected ‘mod_one_error’ not to validate, and ‘mod_one’ to validate.
The goal generated for mod_one also illustrates the issue.
lemma_mod_one.ergo:
(* ---------------------------------------------------------- *)
(* --- Lemma 'mod_one' --- *)
(* ---------------------------------------------------------- *)
(* --- Global Definitions --- *)
goal lemma_mod_one: forall i : int. 0 = i
This leads to vacuous truths when assuming the correct result. In the example below, wp believes ‘i' is 1, and our assumption leads to the contradictions 1 == 0.
void f1() {
int i = 1 % 1;
//@ assert i == 0;
//@ assert vacuous: \false;
}
> frama-c mod.c -wp
[kernel] preprocessing with "gcc -C -E -I. mod.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_f1_assert_vacuous : Valid
[wp] [Alt-Ergo] Goal typed_f1_assert : Unknown
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
This behavior was observed in both Neon and Sodium.https://git.frama-c.com/pub/frama-c/-/issues/545Incorrect grammar for loop-behavior in document2021-02-22T13:05:29Zmantis-gitlab-migrationIncorrect grammar for loop-behavior in documentID0002021:
**This issue was created automatically from Mantis Issue 2021. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002021:
**This issue was created automatically from Mantis Issue 2021. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002021 | Frama-C | Documentation > ACSL | public | 2014-12-05 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Grammar for loop-behavior in Fig2.9 in acsl.pdf (http://frama-c.com/download/acsl.pdf), page 36, has bug. loop-behavior has following grammar:
loop-behavior := for id (, id)* : loop-clause*
which means that having atleast one loop clause is not necessary. But if I don't add any loop-clause frama-c throws warning: unexpected token ' ' in line XX
### Steps To Reproduce :
Following example is correct as per the grammar of loop-behavior. But frama-c throws warning.
/*@ requires n>=0;
behavior fail :
ensures \result == -1;
*/
int example(double t[], int n, double v ){
int l=0, u= n-1;
/*@ loop invariant 0 <=l && u <= n-1;
for fail:
*/
while(l <= u){
l++;
}
return -1;
}
Note: this is contrived example