frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:43:19Z
https://git.frama-c.com/pub/frama-c/-/issues/882
compile-time template recursion causes "multiply-defined" errors
2021-02-22T13:43:19Z
Jochen Burghardt
compile-time template recursion causes "multiply-defined" errors
ID0002038:
**This issue was created automatically from Mantis Issue 2038. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002038:
**This issue was created automatically from Mantis Issue 2038. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002038 | Frama-Clang | Plug-in > clang | public | 2014-12-18 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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:
Now output intermediate result
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:12:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
[kernel] user error: skipping file "421.cpp" that has errors.
The problem remains if line 8 is simplified to "enum { val = 2 };".
## Attachments
- [421.cpp](/uploads/9cf0a89e99ce408e9dc6f580aa78d893/421.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/881
method contract in template specialization class unimplemented
2021-02-22T13:14:05Z
Jochen Burghardt
method contract in template specialization class unimplemented
ID0002037:
**This issue was created automatically from Mantis Issue 2037. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002037:
**This issue was created automatically from Mantis Issue 2037. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002037 | Frama-Clang | Plug-in > clang | public | 2014-12-18 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
unimplemented next attachment
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The error remains if "<T*>" is removed from line 4, turning the template specialization into an ordinary template definition.
The error disappears if line 5 is deleted.
## Attachments
- [418.cpp](/uploads/41c07d4334cfd74c52b3a0c1d86a481c/418.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/880
public variables of superclass not visible in subclass invariant
2021-02-22T14:02:19Z
Jochen Burghardt
public variables of superclass not visible in subclass invariant
ID0001959:
**This issue was created automatically from Mantis Issue 1959. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001959:
**This issue was created automatically from Mantis Issue 1959. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001959 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
120.cpp:9:[kernel] user error: Cannot find field a
If "a ==" is deleted from line 9, the error message disappears.
Note that "a" is visible in the code in line 11.
## Attachments
- [120.cpp](/uploads/64602eaf38dd440ae1fe439ce89706fd/120.cpp)
- [127.cpp](/uploads/cd8fe9eacdedaad20a6a8966f6923c25/127.cpp)
- [120a.cpp](/uploads/00f63c1e84fb84a81269bc2d3301d26d/120a.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/879
protected variable not visible in contract in subclass
2021-02-22T14:02:19Z
Jochen Burghardt
protected variable not visible in contract in subclass
ID0002032:
**This issue was created automatically from Mantis Issue 2032. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002032:
**This issue was created automatically from Mantis Issue 2032. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002032 | Frama-Clang | Plug-in > clang | public | 2014-12-15 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **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:
Now output intermediate result
405.cpp:6:[kernel] user error: Cannot find field salary
The error message remains even if "salary" is made "public" in line 2.
It disappears if the assigns clause in line 5 is deleted.
If "salary" is changed to "Employee::salary" in line 5 (contract), Frama-C aborts with the output:
framaCIRGen: SemaLookup.cpp:1622: bool clang::Sema::LookupQualifiedName(clang::LookupResult &, clang::DeclContext *, bool): Assertion `(!isa<TagDecl>(LookupCtx) || LookupCtx->isDependentContext() || cast<TagDecl>(LookupCtx)->isCompleteDefinition() || cast<TagDecl>(LookupCtx)->isBeingDefined()) && "Declaration context must already be complete!"' failed.
Aborted (core dumped)
## Attachments
- [405.cpp](/uploads/2604415c974ca132ad21fa0bfb2e0f9a/405.cpp)
- [406.cpp](/uploads/8f70ac40f88399771a698c999ed6a392/406.cpp)
- [408a.c](/uploads/0b0359c6a4713e4d26344413bba10744/408a.c)
- [408b.c](/uploads/2f8a39a246fa56a8f647e4698a807cf2/408b.c)
https://git.frama-c.com/pub/frama-c/-/issues/877
"&p->a" causes abort when "->" is user-defined
2021-02-22T13:13:58Z
Jochen Burghardt
"&p->a" causes abort when "->" is user-defined
ID0002025:
**This issue was created automatically from Mantis Issue 2025. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002025:
**This issue was created automatically from Mantis Issue 2025. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002025 | Frama-Clang | Plug-in > clang | public | 2014-12-11 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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/ACSLTermOrPredicate.h:276: void Acsl::TermOrPredicate::Operator::setLocation(location): Assertion `!_startLocation' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if the assertion is replaced by the statement "if (&p->a == 0);".
## Attachments
- [199.cpp](/uploads/3e0bcc51008398612e7ce3d387855f6a/199.cpp)
- [400.cpp](/uploads/f61316995b878a4df7118757094715ba/400.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/876
suggest to document Frama-C's handling of return value optimization
2021-02-22T13:13:56Z
Jochen Burghardt
suggest to document Frama-C's handling of return value optimization
ID0002022:
**This issue was created automatically from Mantis Issue 2022. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002022:
**This issue was created automatically from Mantis Issue 2022. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002022 | Frama-Clang | Plug-in > clang | public | 2014-12-08 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte 192.cpp" on the attached program verifies all obligations, thus showing that Frama-C assumes that no return value optimization (RVO) is done (the copy constructor "X()" from line 13 is called once for the "return" in line 21, and a second time for the initialization in line 25; as a result, the digit "2" is appended to variable "s" twice).
I suggest that Frama-C prints a warning that it assumes that no RVO is done. The g++ compiler doesn't do this; however, Frama-C/Wp users are expected to be far more interested in semantic details than g++ users are. As an alternative, Frama-C's handling of RVO issues should eventually be explained in the manual.
## Attachments
- [192.cpp](/uploads/315524f9cdd77995005dd6b3cf7d4c6e/192.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/875
variable in then-part of "?:" in ACSL clause causes syntax error
2021-02-22T13:13:55Z
Jochen Burghardt
variable in then-part of "?:" in ACSL clause causes syntax error
ID0001993:
**This issue was created automatically from Mantis Issue 1993. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001993:
**This issue was created automatically from Mantis Issue 1993. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001993 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-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:
157.cpp:2:27: unexpected end of expression
The message disappears if "i" is replaced by "2" in the contract in line 2.
## Attachments
- [157.cpp](/uploads/f1b07e5429c0ae36142e24e8e7cf2eeb/157.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/874
clause labels not accepted by cxx plugin
2021-02-22T13:13:53Z
Jochen Burghardt
clause labels not accepted by cxx plugin
ID0002010:
**This issue was created automatically from Mantis Issue 2010. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002010:
**This issue was created automatically from Mantis Issue 2010. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002010 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-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:
187.cpp:2:27: expecting a term or predicate
187.cpp:2:27: expecting a predicate
Now output intermediate result
When the file is renamed to "187.c", Frama-C processes it without complaints, so I guess my syntax is correct. I failed to find this detail in the manual "acsl-implementation-Neon-20140301.pdf", cf. #2009.
## Attachments
- [187.cpp](/uploads/38bdf3aaabc360f9919bbc99cddd8bb1/187.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/872
different error messages for "0<x" and "0<x<9" when x is of class type
2021-02-22T13:13:50Z
Jochen Burghardt
different error messages for "0<x" and "0<x<9" when x is of class type
ID0002007:
**This issue was created automatically from Mantis Issue 2007. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002007:
**This issue was created automatically from Mantis Issue 2007. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002007 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Output of "frama-c -wp 185.cpp" in its current version:
185.cpp:4:24: comparison of incompatible types
Now output intermediate result
185.cpp:4:[kernel] user error: comparison of incompatible types: struct _Z1X and ℤ in annotation.
[kernel] user error: skipping file "185.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
Output of the same command after deleting "< 9" (or, alternatively, deleting "0 <") in line 4:
185.cpp:4:20: comparison of incompatible types
185.cpp:4:20: expecting a term or predicate
185.cpp:4:20: expecting a predicate
Now output intermediate result
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
While both behaviors of Frama-C are ok, their difference (in particular not running / running the Wp plugin) could indicate a bug.
## Attachments
- [185.cpp](/uploads/b1c887234898b1febb2313938115a12a/185.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/870
insufficient preconditions given to Alt-Ergo to prove obligation originating ...
2021-02-22T14:02:18Z
Jochen Burghardt
insufficient preconditions given to Alt-Ergo to prove obligation originating from virtual methods
ID0001974:
**This issue was created automatically from Mantis Issue 1974. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001974:
**This issue was created automatically from Mantis Issue 1974. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001974 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte 138.cpp" on the attached 9-line program generates 98 proof obligations of which 71 turn out to be unprovable (by Qed and Alt-Ergo) after a total user-time of 3 minutes (see session protocol in file "138".txt"). These figures by their own may indicate a problem in scaling-up the current approach to C++ inheritance and virtual functions.
A closer look at e.g. the file "_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw" shows that Alt-Ergo is given insufficient preconditions to prove the goal
"forall i_2,i_1,i : int. forall t_2,t_1 : (addr,int) farray. ... -> is_sint32(i_2) -> is_sint32(t_2[...]) -> -2147483648 <= i_2 + t_2[...]".
Neither "i_2" nor "t_2" appear in the goal formula, except in the shown slice.
Knowing that both i_2 and t_2[...] are signed 32-bit ints is insufficient to prove that their sum won't underflow.
## Attachments
- [138.cpp](/uploads/9bb17093b31c46f1c71a4b8455b1c907/138.cpp)
- [138.txt](/uploads/0d56b0f35ac408035605037a1316ad19/138.txt)
- [_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw](/uploads/8e72ed9402b727d86b81bb8cca28f534/_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw)
https://git.frama-c.com/pub/frama-c/-/issues/869
side effect of constructor call from global variable initialization ignored
2021-02-22T14:02:18Z
Jochen Burghardt
side effect of constructor call from global variable initialization ignored
ID0002002:
**This issue was created automatically from Mantis Issue 2002. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002002:
**This issue was created automatically from Mantis Issue 2002. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002002 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **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 :
The attached program can be verified by "frama-c -wp 177.cpp", although printing x's value after line 11 reveals that the proven assertion there is false.
The reason is that x was set to 42 by the constructor call cls() from the declaration in line 8, but Frama-C doesn't consider the body code of line 5 when determining the value of x in line 11.
On the other hand, it seems that Frama-C is well aware about the declaration in line 8 calling the constructor in line 5: annotating the latter with "requires \false" produces an unproven obligation that vanishes again if line 8 is deleted.
## Attachments
- [177.cpp](/uploads/723d9cb3d39ae9300cad25f31ece596a/177.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/868
suggest to suppress warning about passing void value via return statement
2021-02-22T13:26:54Z
Jochen Burghardt
suggest to suppress warning about passing void value via return statement
ID0001998:
**This issue was created automatically from Mantis Issue 1998. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001998:
**This issue was created automatically from Mantis Issue 1998. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001998 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output for file "165.cpp":
Now output intermediate result
165.cpp:4:[kernel] warning: Return statement with a value in function returning void
According to Stroustrup, sect.7.3 "Value Return", the code is ok, and can make sense in templates with type parameters, cf. file "165a.cpp".
Running "g++ -Wall -pedantic 165.cpp" doesn't give a warning either.
## Attachments
- [165.cpp](/uploads/de64441631b47caf183ef875ea08a786/165.cpp)
- [165a.cpp](/uploads/e805233d81f78ff5dc0a6e47430d449d/165a.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/867
identifier declared in condition is unknown in assert clause
2021-02-22T14:01:53Z
Jochen Burghardt
identifier declared in condition is unknown in assert clause
ID0001996:
**This issue was created automatically from Mantis Issue 1996. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001996:
**This issue was created automatically from Mantis Issue 1996. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001996 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
159.cpp:4:17: unknown identifier 'i'
Now output intermediate result
If the assertion in line 4 is changed to a statement, like "i = 2;", the message disappears.
## Attachments
- [159.cpp](/uploads/70c4933a06e4a73d20c28472895a233a/159.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/866
"do"-loop with body interspersed with "case" labels of surrounding "switch" n...
2021-02-22T13:26:56Z
Jochen Burghardt
"do"-loop with body interspersed with "case" labels of surrounding "switch" not parsed
ID0001994:
**This issue was created automatically from Mantis Issue 1994. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001994:
**This issue was created automatically from Mantis Issue 1994. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001994 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Unsupported Statement:
DefaultStmt 0x2caf430 <158.cpp:6:2, col:15>
`-UnaryOperator 0x2c64b68 <col:12, col:15> 'int' postfix '++'
`-DeclRefExpr 0x2c64b40 <col:12> 'int' lvalue Var 0x2c649a0 'sum' 'int'
Aborting
The program has been boiled down from that an exercise in Stroustrup's C++ book, see attached file "stroustrup_06_06_15.cpp" for full example.
## Attachments
- [158.cpp](/uploads/7f019adb35c3e1fa16d757db41c9f50c/158.cpp)
- [stroustrup_06_06_15.cpp](/uploads/420758addbd603cbf270e95b7f67b154/stroustrup_06_06_15.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/864
non-predicate on right-hand size of "|" causes segmentation fault
2021-03-29T16:34:53Z
Jochen Burghardt
non-predicate on right-hand size of "|" causes segmentation fault
ID0001991:
**This issue was created automatically from Mantis Issue 1991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001991:
**This issue was created automatically from Mantis Issue 1991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001991 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Same for "&".
In contrast, "i | (i==i)" is accepted, which might not be ok either, since "i" is not a predicate, and "i | ..." isn't either.
## Attachments
- [155.cpp](/uploads/97f44d774ea3375ac8795a16896f3136/155.cpp)
- [155a.cpp](/uploads/6028e94aafd01c070d1470bd32b6a00c/155a.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/863
how to specify equality of references, rather than of values, in contract?
2021-02-22T13:13:38Z
Jochen Burghardt
how to specify equality of references, rather than of values, in contract?
ID0001990:
**This issue was created automatically from Mantis Issue 1990. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001990:
**This issue was created automatically from Mantis Issue 1990. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001990 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The contract of the function "fst" in line 4 of the attached program intends to specify that "fst(ppp)" returns a reference to "ppp.xxx".
However, it is interpreted by Frama-C as specifying that "fst(ppp)" and "ppp.xxx" have the same value. As a consequence, the assertion in line 10 cannot be proven; the generated obligation essentially amounts to "t_2[a_1] = t_2[a] -> 222 = t_2[a_1 <- 222][a]"; cf. the attached .mlw file. If the precondition would state reference equality (i.e. "a_1 = a") instead of value equality (i.e. "t_2[a_1] = t_2[a]"), the goal would follow trivially.
Frama-C's interpretation is not a bug, but is perfectly valid.
However, the question arises how the intended meaning (i.e. reference equality) could be formalized in the contract. Maybe another equality operator ( named e.g. "===") should be introduced into ACSL++ for this purpose.
## Attachments
- [152.cpp](/uploads/ae9fb734c8266aae29f014361aee8f4f/152.cpp)
- [_Z3bar_assert_Alt-Ergo.mlw](/uploads/f53057cf4583330c0dba0cd5ac99de4f/_Z3bar_assert_Alt-Ergo.mlw)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/862
namespace prefix in annotation causes segmentation fault
2021-03-29T16:41:05Z
Jochen Burghardt
namespace prefix in annotation causes segmentation fault
ID0001985:
**This issue was created automatically from Mantis Issue 1985. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001985:
**This issue was created automatically from Mantis Issue 1985. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001985 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
## Attachments
- [147.cpp](/uploads/ee910fafdfbabeb2abdb356f31ad4a03/147.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/861
scope resolution operator not recognized in assertion
2021-02-22T13:26:43Z
Jochen Burghardt
scope resolution operator not recognized in assertion
ID0001984:
**This issue was created automatically from Mantis Issue 1984. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001984:
**This issue was created automatically from Mantis Issue 1984. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001984 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
146.cpp:9:14: unexpected token 'operator -> ::' when starting to parse a term
Now output intermediate result
(Lines 5-8 aren't really needed to produce the error message.)
## Attachments
- [146.cpp](/uploads/73158ee47b3e3b872d5c8187cf72008b/146.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/860
identifier unknown after leaving inner scope that declared same name
2022-04-02T21:12:27Z
Jochen Burghardt
identifier unknown after leaving inner scope that declared same name
ID0001983:
**This issue was created automatically from Mantis Issue 1983. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001983:
**This issue was created automatically from Mantis Issue 1983. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001983 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
145.cpp:7:16: unknown identifier 'x'
Now output intermediate result
...
[wp] Proved goals: 0 / 0
The error message disappears and a proof obligation is generated (and proven by Qed) if "x" is changed to "y" in the inner scope (line 5).
## Attachments
- [145.cpp](/uploads/73be9f397b0fdbf37c7e518259c9bf24/145.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/859
enum types in contract cause syntax error
2021-02-22T13:26:57Z
Jochen Burghardt
enum types in contract cause syntax error
ID0001982:
**This issue was created automatically from Mantis Issue 1982. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001982:
**This issue was created automatically from Mantis Issue 1982. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001982 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
144.cpp:4:22: keyword 'keyword -> enum' encountered when parsing a type
Now output intermediate result
The message disappears if the file is renamed to "144.c".
## Attachments
- [144.cpp](/uploads/cfc01750842b55273e7a3094dc5cba83/144.cpp)
Virgile Prevosto
Virgile Prevosto