frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:27:11Zhttps://git.frama-c.com/pub/frama-c/-/issues/897recursive logic integer function definition causes error2021-02-22T13:27:11ZJochen Burghardtrecursive logic integer function definition causes errorID0002050:
**This issue was created automatically from Mantis Issue 2050. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002050:
**This issue was created automatically from Mantis Issue 2050. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002050 | Frama-Clang | Plug-in > clang | public | 2015-01-15 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
431.cpp:2:56: unknown identifier 'fac'
Now output intermediate result
The problem disappears when the file is renamed to "431.c".
## Attachments
- [431.cpp](/uploads/50a3448bd9c7ec87a3c7205370803f6e/431.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/896ACSL comment rejected in function template2021-02-22T13:27:13ZJochen BurghardtACSL comment rejected in function templateID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002048 | Frama-Clang | Plug-in > clang | public | 2015-01-12 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **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 430.cpp (external front-end)
inadequate comment at 430.cpp:5:2
If line 2 is commented-in and line 3 is commented-out, the error message disappears.
## Attachments
- [430.cpp](/uploads/fb7c1b9a2c7e740eb0e5c7200661ce99/430.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/895unprovable obligation generated for "ensures" in presence of exceptions2021-02-22T13:14:24ZJochen Burghardtunprovable obligation generated for "ensures" in presence of exceptionsID0002046:
**This issue was created automatically from Mantis Issue 2046. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002046:
**This issue was created automatically from Mantis Issue 2046. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002046 | Frama-Clang | Plug-in > clang | public | 2015-01-08 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
Running "frama-c -wp 429.cpp" on the attached program, the goal "typed__Z3bari_post_part1" cannot be proven by Alt-Ergo, i.e. it can't be proven that the postcondition of "foo" implies that of "bar" if the former doesn't throw an exception.
The goal in the file "_Z3bari_post_part1_Alt-Ergo.mlw" reads:
585 goal _Z3bari_post_part1:
586 forall i : int.
587 forall f : S___fc_exn_struct.
588 let x = (f.F___fc_exn_struct_exn_uncaught) : int in
589 (1 <> x) ->
590 is_sint32(i) ->
591 is_sint32(f.F___fc_exn_struct_exn_kind) ->
592 is_sint32(x) ->
593 ((0 = x) -> (42 <= i)) ->
594 (24 <= i)
If line 589 is changed to "(0 = x) ->", Alt-Ergo can prove it without problems; likewise if line 593 is changed to "((1 <> x) -> (42 <= i)) ->".
## Attachments
- [429.cpp](/uploads/8924b97702a6b0ba13c4daf1f56285ca/429.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/894throw without argument causes crash2021-02-22T13:41:11ZJochen Burghardtthrow without argument causes crashID0002045:
**This issue was created automatically from Mantis Issue 2045. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002045:
**This issue was created automatically from Mantis Issue 2045. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002045 | Frama-Clang | Plug-in > clang | public | 2015-01-08 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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:
Now output intermediate result
[kernel] Current source was: 428.cpp:2
The full backtrace is:
Raised at file "stack.ml", line 36, characters 20-25
Called from file "src/kernel/exn_flow.ml", line 98, characters 23-44
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2046, characters 15-31
Called from file "cil/src/cil.ml", line 3095, characters 5-86
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 3255, characters 16-40
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3484, characters 14-39
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3446, characters 5-91
Called from file "cil/src/cil.ml", line 3538, characters 16-38
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 2130, characters 24-57
Called from file "cil/src/cil.ml", line 3532, characters 5-53
Called from file "cil/src/cil.ml", line 6151, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5741, characters 3-30
Called from file "cil/src/cil.ml", line 6152, characters 2-420
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 6185, characters 7-84
Called from file "src/kernel/visitor.ml", line 827, characters 2-45
Called from file "src/kernel/file.ml", line 1803, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1880, characters 2-36
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
Unexpected error (Stack.Empty).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
## Attachments
- [428.cpp](/uploads/ec15e3525df0c4c9340947fc89b631c9/428.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/885constructor overloading resolution with templates causes dubious "contract me...2021-02-22T13:27:09ZJochen Burghardtconstructor overloading resolution with templates causes dubious "contract merge" warningID0002043:
**This issue was created automatically from Mantis Issue 2043. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002043:
**This issue was created automatically from Mantis Issue 2043. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002043 | Frama-Clang | Plug-in > clang | public | 2015-01-05 | 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 :
Running "frama-c -wp 426.cpp" produces the output:
Now output intermediate result
426.cpp:5:[kernel] warning: found two contracts. Merging them
[wp] Running WP plugin...
The warning remains if
(1) the contract in line 7 is activated, or
(2) the contract in line 11 is deactivated.
The warning disappears if
(3) lines 4-5 are deleted,
(4) line 8 is deleted, or
(5) "char" is changed to "int" in line 13.
Even if the warning is printed, the proof obligation for the constructor call in line 13 seems to be correct, viz.:
(* ---------------------------------------------------------- *)
(* --- Instance of 'Pre-condition (file 426.cpp, line 4) in '_ZN7complexIcEEC1vci'' in 'main' at call '_ZN7complexIcEEC1vci' (file 426.cpp, line 13)
--- *)
(* ---------------------------------------------------------- *)
goal main_call__ZN7complexIcEEC1vci_pre:
forall i : int.
forall t : int farray.
(i <= 6) ->
linked(t) ->
is_sint32(i) ->
(1 = i)
So it is not clear which contracts are merged. Possibly this is a revival of issue #1611. However, it could also indicate that the contract in line 4 is merged with the (empty) contract of the constructor in line 8 (since the warning disappears when line 8 is removed) - which would be wrong in general.
## Attachments
- [426.cpp](/uploads/83b16ec11a724e4803101543fe3e06de/426.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/884contract of template function specialization taken to refer to next plain fun...2021-02-22T13:14:10ZJochen Burghardtcontract of template function specialization taken to refer to next plain function belowID0002042:
**This issue was created automatically from Mantis Issue 2042. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002042:
**This issue was created automatically from Mantis Issue 2042. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002042 | Frama-Clang | Plug-in > clang | public | 2015-01-05 | 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 :
Using "frama-c -wp 424.cpp" the attached program can be verified, although e.g. foo<int>(0) yields 2 whereas its contract says it should yield 4.
Apparently, Frama-C thinks the contract belongs to the plain function bar(). That would also be an explanation for issue #2034.
Moving the contract from line 4 down to line 6, or to line 8, keeps that behavior.
After moving it up to line 1 (i.e. before the generic template), no obligation at all is generated (which is ok since foo<>() isn't called anywhere).
## Attachments
- [424.cpp](/uploads/27785eb453be4b53b4f7843126234b75/424.cpp)
- [424a.cpp](/uploads/8bcfdd48f28c3257a7b0dbdfd882ce36/424a.cpp)https://git.frama-c.com/pub/frama-c/-/issues/882compile-time template recursion causes "multiply-defined" errors2021-02-22T13:43:19ZJochen Burghardtcompile-time template recursion causes "multiply-defined" errorsID0002038:
**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/881method contract in template specialization class unimplemented2021-02-22T13:14:05ZJochen Burghardtmethod contract in template specialization class unimplementedID0002037:
**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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/883"ensures" clause of function template not supplied to Alt-Ergo2021-02-22T13:27:02ZJochen Burghardt"ensures" clause of function template not supplied to Alt-ErgoID0002034:
**This issue was created automatically from Mantis Issue 2034. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002034:
**This issue was created automatically from Mantis Issue 2034. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002034 | Frama-Clang | Plug-in > clang | public | 2014-12-15 | 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 :
Running "frama-c -wp 411.cpp" generates, from the "assert" in line 12, an unprovable obligation (for Alt-Ergo), viz: "goal main_assert: forall i : int. is_sint32(i) -> (1 = i)", see line 570 of file "main_assert_Alt-Ergo.mlw".
If the function "nop" is made a non-template function (by uncommenting the typedef in line 4, and commenting-out the "template<class T>" prefix in line 7), the obligation reads "goal main_assert: forall i : int. (2 = (2 * i)) -> is_sint32(i) -> (1 = i)", and is proven without problems by Alt-Ergo.
## Attachments
- [411.cpp](/uploads/f4d3734df967c73ae7c415efd8c5d1de/411.cpp)
- [main_assert_Alt-Ergo.mlw](/uploads/13ed07ef6485c5aa5d0eafa5599fabbf/main_assert_Alt-Ergo.mlw)
- [411a.cpp](/uploads/0ffcaa8993e4cb1ec8e78eb5d2774ac2/411a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/879protected variable not visible in contract in subclass2021-02-22T14:02:19ZJochen Burghardtprotected variable not visible in contract in subclassID0002032:
**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/833error message "unknown identifier 'xxx'" causes Frama-C to forget previous mo...2021-02-22T14:01:54ZJochen Burghardterror message "unknown identifier 'xxx'" causes Frama-C to forget previous more severe errorsID0002033:
**This issue was created automatically from Mantis Issue 2033. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002033:
**This issue was created automatically from Mantis Issue 2033. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002033 | Frama-Clang | Plug-in > clang | public | 2014-12-15 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
In its current form (cf. issue #2032), the complete output of "frama-c -wp 405.cpp" looks like:
Now output intermediate result
405.cpp:6:[kernel] user error: Cannot find field salary
[kernel] user error: skipping file "405.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
However, if a non-declared variable (e.g. "xxx") is added to the "assigns" clause in line 5, the subsequent call to the wp plugin is no longer suppressed; the complete output then looks:
405.cpp:5:26: unknown identifier 'xxx'
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
If there is some Frama-C-internal variable holding the severity of
errors detected so far, the "Cannot find field salary" error seems to
set it to a high level (thus suppressing the wp call), which is ok;
however the "unknown identifier 'xxx'" seems to lower that level again
(thus re-enabling the wp call), which is probably not ok.
## Attachments
- [405.cpp](/uploads/fe7b7b538990b1a71e7de87d63e0922a/405.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/939use of later-defined nested class type in method signature causes error2021-02-22T13:15:29ZJochen Burghardtuse of later-defined nested class type in method signature causes errorID0002027:
**This issue was created automatically from Mantis Issue 2027. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002027:
**This issue was created automatically from Mantis Issue 2027. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002027 | Frama-Clang | Plug-in > clang | public | 2014-12-11 | 2014-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **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** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
403.cpp:8:[kernel] user error: redefinition of '_ZN6StringE4Srep' in the same scope. Previous declaration was at 403.cpp:4
[kernel] user error: skipping file "403.cpp" that has errors.
The error remains if the definition of "Srep" is moved into "String".
The error disappears if the declarations of "foo" is deleted in line 4.
## Attachments
- [403.cpp](/uploads/4ea891dfc1b5ccbb91e068ab31096c71/403.cpp)https://git.frama-c.com/pub/frama-c/-/issues/877"&p->a" causes abort when "->" is user-defined2021-02-22T13:13:58ZJochen Burghardt"&p->a" causes abort when "->" is user-definedID0002025:
**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/876suggest to document Frama-C's handling of return value optimization2021-02-22T13:13:56ZJochen Burghardtsuggest to document Frama-C's handling of return value optimizationID0002022:
**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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/810insufficient preconditions given to Alt-Ergo to prove "requires" clause about...2021-02-22T14:02:09ZJochen Burghardtinsufficient preconditions given to Alt-Ergo to prove "requires" clause about class member variableID0002014:
**This issue was created automatically from Mantis Issue 2014. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002014:
**This issue was created automatically from Mantis Issue 2014. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002014 | Frama-Clang | Plug-in > clang | public | 2014-12-04 | 2015-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
In the attached program "188.cpp", the constructor "X()" initialized the class member variable "x" to 13 (contract and code in line 4 and 5, respectively; contract deliberately phrased to prevent Qed from using it). This constructor is called from the declaration in line 12.
The "assert" in line 13 can be proved without problems; however, the (literally identical) precondition of the "foo" call in line 14 cannot. The file "main_assert_Alt-Ergo.mlw" for the "assert" has the goal:
823 goal main_assert:
824 let a = shiftfield_F__Z1X_x(shift__Z1X(global(L_i_105), 0)) : addr in
825 forall t : int farray.
826 forall t_1 : (addr,int) farray.
827 linked(t) ->
828 (130 = (10 * t_1[a])) ->
829 is_sint32(t_1[a]) ->
830 (t_1[a] <= 42)
that is, t_1[a]==13 is known and t_1[a]<=42 is to be proved.
In contrast, the file "main_call__Z3foo1X_pre_Alt-Ergo.mlw" for the "requires" has the goal:
824 goal main_call__Z3foo1X_pre:
825 let a = shiftfield_F__Z1X_x(shift__Z1X(global(L_i_105), 0)) : addr in
826 let a_1 = shift__Z1X(global(L___fc_tmp_0_106), 0) : addr in
827 forall t : int farray.
828 forall t_2,t_1 : (addr,int) farray.
829 linked(t) ->
830 (t_1[a] <= 42) ->
831 (130 = (10 * t_1[a])) ->
832 IsS__Z1X(Load_S__Z1X(a_1, t_2)) ->
833 is_sint32(t_1[a]) ->
834 ((Load_S__Z1X(a_1, t_2).F__Z1X_x) <= 42)
that is, t_1[a]==13 is known and (Load_S__Z1X(a_1, t_2).F__Z1X_x)<=42 is to be proven, where no relation between t_1 and t_2 is known (both are locally quantified variables).
I guess both proof goals should be similar, or at least a relation between t_1 and t_2 should be given to Alt-Ergo in the goal stemming from "requires".
If "assigns x;" is added to the contract of "X()" in line 4, the situation doesn't improve. The goals then look as follows. In file "main_assert_Alt-Ergo.mlw":
759 goal main_assert:
760 forall i : int.
761 forall t : int farray.
762 (130 = (10 * i)) ->
763 linked(t) ->
764 is_sint32(i) ->
765 (i <= 42)
that is, i==13 is known and i<=42 is to be proved.
In file "main_call__Z3foo1X_pre_Alt-Ergo.mlw":
824 goal main_call__Z3foo1X_pre:
825 let a = shift__Z1X(global(L___fc_tmp_0_106), 0) : addr in
826 forall i : int.
827 forall t : int farray.
828 forall t_1 : (addr,int) farray.
829 (i <= 42) ->
830 (130 = (10 * i)) ->
831 linked(t) ->
832 is_sint32(i) ->
833 IsS__Z1X(Load_S__Z1X(a, t_1)) ->
834 ((Load_S__Z1X(a, t_1).F__Z1X_x) <= 42)
that is, i==13 is known and (Load_S__Z1X(a, t_1).F__Z1X_x)<=42 is to be proven, where no relation between i and t_1 is known (again, both are locally quantified variables).
## Attachments
- [188.cpp](/uploads/099b24b3b63f23a0b2d36961399b08f8/188.cpp)
- [main_assert_Alt-Ergo.mlw_without_assigns](/uploads/a178b5c1643ad780e1b69564d3ddd595/main_assert_Alt-Ergo.mlw_without_assigns)
- [main_call__Z3foo1X_pre_Alt-Ergo.mlw_without_assigns](/uploads/9353ccdc4d04963494c985a23d4a60a5/main_call__Z3foo1X_pre_Alt-Ergo.mlw_without_assigns)
- [main_assert_Alt-Ergo.mlw_with_assigns](/uploads/1763b58af26b99be4ae48ee3bbc91da3/main_assert_Alt-Ergo.mlw_with_assigns)
- [main_call__Z3foo1X_pre_Alt-Ergo.mlw_with_assigns](/uploads/926b2e468083e8df93a34ec6b80db691/main_call__Z3foo1X_pre_Alt-Ergo.mlw_with_assigns)Virgile PrevostoVirgile Prevostohttps://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/874clause labels not accepted by cxx plugin2021-02-22T13:13:53ZJochen Burghardtclause labels not accepted by cxx pluginID0002010:
**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/872different error messages for "0<x" and "0<x<9" when x is of class type2021-02-22T13:13:50ZJochen Burghardtdifferent error messages for "0<x" and "0<x<9" when x is of class typeID0002007:
**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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/869side effect of constructor call from global variable initialization ignored2021-02-22T14:02:18ZJochen Burghardtside effect of constructor call from global variable initialization ignoredID0002002:
**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/674method call in initializer of global constant causes segmentation fault2021-02-22T13:08:42ZJochen Burghardtmethod call in initializer of global constant causes segmentation faultID0002005:
**This issue was created automatically from Mantis Issue 2005. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002005:
**This issue was created automatically from Mantis Issue 2005. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002005 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-03-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **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
If the "const" is removed from line 8, the output changes to:
Now output intermediate result
182.cpp:8:[kernel] warning: Call to _ZN3clsE1a in constant. Ignoring this call and returning 0.
If line 8 is embedded in the body of main(), the problem disappears (with and without "const").
## Attachments
- [182.cpp](/uploads/488e6187dc8b8a423989ecada7a407e0/182.cpp)Franck VedrineFranck Vedrine