frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:06:42Zhttps://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/576No syntax to apply lambda expressions2021-02-22T13:06:12ZDavid CokNo syntax to apply lambda expressionsID0002196:
**This issue was created automatically from Mantis Issue 2196. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002196:
**This issue was created automatically from Mantis Issue 2196. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002196 | Frama-C | Kernel > ACSL implementation | public | 2015-12-05 | 2015-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL 1.9 allows writing lambda expressions. They can be used in extended quantifiers. But there is no syntax to use them anywhere else, such as to apply a lambda expression to a sequence of arguments.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/575ambiguity with consecutive comparison and ternary expressions2021-02-22T13:06:12ZDavid Cokambiguity with consecutive comparison and ternary expressionsID0002195:
**This issue was created automatically from Mantis Issue 2195. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002195:
**This issue was created automatically from Mantis Issue 2195. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002195 | Frama-C | Kernel > ACSL implementation | public | 2015-12-05 | 2015-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The ACSL grammar allows two forms of ternary expressions for predicates:
term ? pred : pred
pred ? pred : pred
But the interpretation of consecutive comparisons depends on whether the expression is in term or predicate position. Thus the predicate
(i == j < k) ? (\true==>\\true) ? (\true==>\false)
is fundamentally ambiguous in the grammar. If the condition is a predicate, it is equivalent to
((i == j) && (j < k)) ? ...
As a term it is equivalent to
((i == j) < k) ?
Depending on the types of i, j, and k,
it may not typecheck correctly as either a term or predicate - but does, for example, if all three are ints. However, it would be really bad design if the grammar parser depended on the types of expressions.
Is this construct deemed illegal, or is it resolved in favor of one form or the other?Virgile PrevostoVirgile Prevostohttps://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 examplehttps://git.frama-c.com/pub/frama-c/-/issues/544assumes clause and labels2021-02-22T13:05:28ZJens Gerlachassumes clause and labelsID0002040:
**This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002040:
**This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002040 | Frama-C | Plug-in > wp | public | 2014-12-27 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
My understanding of assumes clauses is that they refer to the pre-state of a function.
The attached example, however, works differently.
The function push_back has two disjoint behaviors that rely on the predicate "full".
The function push_back_twice is only verified if I add the label "Pre"
to the predicate "full" in the assumes clauses of function push_back.
I think this is a bug.
It should not be necessary to add this explicit label.
### Additional Information :
Concerns versions
Neon-20140301
Neon-20140301+dev-stance
I remember that Kim Völlinger had observed the same(?) problem in Oxygen and
that it was fixed in Fluorine.
## Attachments
- [assumes_label.c](/uploads/c4f41bff0222c51c966f982647981368/assumes_label.c)https://git.frama-c.com/pub/frama-c/-/issues/540predicate definitions should be of type prop2021-02-22T13:05:22ZClaude Marchépredicate definitions should be of type propID0000444:
**This issue was created automatically from Mantis Issue 444. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000444:
**This issue was created automatically from Mantis Issue 444. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000444 | Frama-C | Kernel > ACSL implementation | public | 2010-04-08 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cmarche | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In a predicate definition like below
//@ predicate f(integer x) = x+1;
it should be checked that the body of the definition denotes a prop and not a termhttps://git.frama-c.com/pub/frama-c/-/issues/534memory leak (endless recursion?) caused by erroneous c program2021-02-22T13:05:10ZJochen Burghardtmemory leak (endless recursion?) caused by erroneous c programID0002184:
**This issue was created automatically from Mantis Issue 2184. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002184:
**This issue was created automatically from Mantis Issue 2184. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002184 | Frama-C | Plug-in > wp | public | 2015-11-02 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | 14.04.1-Ubuntu |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Running "frama-c 10.c" on the attached program causes frama-c to allocate a rapidly increasing amount of memory, until it crashes with the unbuntu-message "Fatal error: out of memory." Apparently, it performs an endless recursion.
The program "10.c" is erroneous and nonsensical, and originates from a "creduce" experiment with a poor test script. However, it may be worth to eliminate the endless recusion, anyway?
## Attachments
- [10.c](/uploads/6b5ba89a77511be850092e7d6514913b/10.c)https://git.frama-c.com/pub/frama-c/-/issues/532"If" statement with only one successor2021-02-22T13:05:08ZHugo Illous"If" statement with only one successorID0002119:
**This issue was created automatically from Mantis Issue 2119. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002119:
**This issue was created automatically from Mantis Issue 2119. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002119 | Frama-C | Kernel | public | 2015-05-20 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.illous | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
When a "If" statements contains in its true block the sequence "do {} while (0);", in the CFG, this statement will have only one successor.
### Steps To Reproduce :
You can simply try with this C program and compute List.length stmt.succs
void f(int n) {
if (n == 0) do {} while (0);
}https://git.frama-c.com/pub/frama-c/-/issues/529overloading of predicate fails2021-02-22T13:05:00ZJens Gerlachoverloading of predicate failsID0002098:
**This issue was created automatically from Mantis Issue 2098. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002098:
**This issue was created automatically from Mantis Issue 2098. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002098 | Frama-C | Kernel > ACSL implementation | public | 2015-03-31 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Magnesium | **Fixed in Version** | Frama-C Magnesium |
### Description :
Overloading of ACSL predicates does not work anymore.
### Additional Information :
the problem does NOT occur under Neon.
### Steps To Reproduce :
the attached program reports the following error when called with 'frama-c overloading.c'
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing overloading.c (with preprocessing)
overloading.c:10:[kernel] user error: invalid implicit conversion from 'int' to 'short' in annotation.
[kernel] user error: stopping on file "overloading.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [overloading.c](/uploads/9a26b0d025434222fddb2f37e1e99e80/overloading.c)
- [overloading2.c](/uploads/09b42bc4285c4460e2dc291ef3a83c3b/overloading2.c)https://git.frama-c.com/pub/frama-c/-/issues/522provide option "-wp-lemma"2021-02-22T13:04:45ZJens Gerlachprovide option "-wp-lemma"ID0002202:
**This issue was created automatically from Mantis Issue 2202. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002202:
**This issue was created automatically from Mantis Issue 2202. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002202 | Frama-C | Plug-in > wp | public | 2016-01-23 | 2016-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP has several options to consider only individual functions, properties, or behaviors during verification.
It would be nice if there were an option "-wp-lemma 'name' " which would allow to consider only the names lemma.https://git.frama-c.com/pub/frama-c/-/issues/504Reals are bad encoded for coq2021-02-22T13:04:23Zmantis-gitlab-migrationReals are bad encoded for coqID0002214:
**This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002214:
**This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002214 | Frama-C | Plug-in > wp | public | 2016-03-03 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davyg | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | All | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The definition of real_base(Qedlib) in the coq exporter of wp is incorrect :
There is :
Definition real_base e a n :=
match n with
| 0 => 1%R
| Zpos n => (a * pow e (Pos.to_nat n))%R
| Zneg n => (a / pow e (Pos.to_nat n))%R
end.
in stead of
Definition real_base e a n :=
match n with
| 0 => a
| Zpos n => (a * pow e (Pos.to_nat n))%R
| Zneg n => (a / pow e (Pos.to_nat n))%R
end.
### Steps To Reproduce :
I think that any coq proof you try to prove with wp containing real constant should have the errorhttps://git.frama-c.com/pub/frama-c/-/issues/502Values inferred for 32-bit variable do not fit in 32-bit type2021-02-22T13:04:21ZPascal CuoqValues inferred for 32-bit variable do not fit in 32-bit typeID0001968:
**This issue was created automatically from Mantis Issue 1968. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001968:
**This issue was created automatically from Mantis Issue 1968. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001968 | Frama-C | Plug-in > Eva | public | 2014-11-13 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The values inferred for the variable i below are 64-bit values that wouldn't even fit the 32-bit unsigned int that variable i is.
Program:
int main() {
Frama_C_show_each(sizeof(unsigned int));
unsigned int i = 0;
while (u())
{
i+=2;
}
}
$ frama-c -val t.c
…
[value] Called Frama_C_show_each({4})
…
[value] Values at end of function main:
i ∈ [0..9223372036854775806],0%2https://git.frama-c.com/pub/frama-c/-/issues/501coq fails to compile Cint because Zbits is not found2021-02-22T13:04:18Zmantis-gitlab-migrationcoq fails to compile Cint because Zbits is not foundID0002155:
**This issue was created automatically from Mantis Issue 2155. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002155:
**This issue was created automatically from Mantis Issue 2155. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002155 | Frama-C | Plug-in > wp | public | 2015-09-02 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
As described in https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2014-March/004380.html, I get the same error message that Cint can't be compiled because Zbits isn't compiled yet.
I'm getting this on a Debian system.
I attached a patch based on the mail that seems to fix the issue for me.
## Attachments
- [wp.driver.patch](/uploads/a497ab58ae4dc3b1ac4220b14fafbd1d/wp.driver.patch)https://git.frama-c.com/pub/frama-c/-/issues/496Frama-c accepts assigning formal parameters when a range is used2021-02-22T13:04:05Zmantis-gitlab-migrationFrama-c accepts assigning formal parameters when a range is usedID0002217:
**This issue was created automatically from Mantis Issue 2217. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002217:
**This issue was created automatically from Mantis Issue 2217. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002217 | Frama-C | Kernel | public | 2016-03-17 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
When assigning a range, no error is produced when referencing a formal parameter.
### Steps To Reproduce :
test.c:
typedef struct obj {
char buf[5];
} obj;
/*@
assigns x.buf[0..0];
*/
void foo(obj x);
void bar() {
obj tmp;
foo(tmp);
//@ assert \true;
}
Running as given above produces no error (it should).
> frama-c test.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
Running the above program with wp causes an error.
> frama-c test.c -wp
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
[wp] warning: Missing RTE guards
test.c:6:[wp] user error: Address of logic value (tmp_0)
[kernel] Plug-in wp aborted: invalid user input.
Changing the specification of foo to “assigns x.buf[0]” results in the expected error.
> frama-c test.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
test.c:6:[kernel] user error: can not assign part of a formal parameter: x.buf[0]
[kernel] user error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.