frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:28:04Zhttps://git.frama-c.com/pub/frama-c/-/issues/906exception identifier from catch() statement unknown in contracts, but not in ...2021-02-22T13:28:04ZJochen Burghardtexception identifier from catch() statement unknown in contracts, but not in codeID0002071:
**This issue was created automatically from Mantis Issue 2071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002071:
**This issue was created automatically from Mantis Issue 2071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002071 | Frama-Clang | Plug-in > clang | public | 2015-02-02 | 2015-02-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 447.cpp (external front-end)
447.cpp:6:17: unknown identifier 'e'
Now output intermediate result
The message disappears if the "assert" in line 6 is deactivated.
## Attachments
- [447.cpp](/uploads/25b6f25f7846390e808821adc8820019/447.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/903can't compare pointer and reference for equality in contract2021-02-22T13:14:31ZJochen Burghardtcan't compare pointer and reference for equality in contractID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002060 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 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 441.cpp (external front-end)
441.cpp:2:22: invalid implicit conversion
441.cpp:2:22: unknown type comparison for the operator ==
Now output intermediate result
When line 2 is commented out, the comparison in C++ code in line 3 is accepted.
## Attachments
- [441.cpp](/uploads/da2cc8f3623d5563d069827341da0b18/441.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/900type def'd as template typename causes SEGV when used in logic functions2021-02-22T13:14:28ZJochen Burghardttype def'd as template typename causes SEGV when used in logic functionsID0002057:
**This issue was created automatically from Mantis Issue 2057. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002057:
**This issue was created automatically from Mantis Issue 2057. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002057 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In its current version, the program apparently causes a SEGV of the front-end:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Several variations cause different behaviors, such as:
(1) changing "integer" to "int " in line 8:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
438.cpp:8:51: invalid implicit conversion
438.cpp:8:51: expecting a term as body of function
Now output intermediate result
(2) omitting the template parameter, and changing "T" to "int" in line 3:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
Now output intermediate result
[fclang] failure: Cannot understand intermediate AST: line 799: unexpected unknown constructor 39702768 (Unknown constructor for term_node)
[kernel] Current source was: FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i:43
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/frama_Clang_register.ml", line 83, characters 6-75
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
(3) changing "pointer" to "T*" in line 7:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
438.cpp:8:55: predicates do not support binary '+' operation
Now output intermediate result
438.cpp:7:[fclang] failure: predicate definition with a term as body
[kernel] Current source was: 438.cpp:7
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 622, characters 12-76
Called from file "src/frama-clang/convert.ml", line 2393, characters 18-54
Called from file "src/frama-clang/convert.ml", line 2554, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2558, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
## Attachments
- [438.cpp](/uploads/4ab4dc04efdff7cdadbd1e41d15d47e0/438.cpp)
- [438a.cpp](/uploads/957036da370283dcaa88f2713cd9f18a/438a.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/898catching a superclass causes crash2021-02-22T13:14:26ZJochen Burghardtcatching a superclass causes crashID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002051 | Frama-Clang | Plug-in > clang | public | 2015-01-15 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
[fclang] failure: Did not find struct for mangled class name _Z9Underflow
[kernel] Current source was: 432.cpp:6
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_link.ml", line 71, characters 36-53
Called from file "src/lib/FCSet.ml", line 332, characters 37-58
Called from file "src/frama-clang/convert_link.ml", line 86, characters 16-112
Called from file "src/frama-clang/convert_link.ml", line 104, characters 16-62
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert_link.ml", line 102, characters 12-142
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/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
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
The problem remains if some member variable (e.g. "int x;") is added to the body of class "Matherr" in line 2 or/and the body of class "Underflow" in line 3.
The problem disappears if either:
(1) the definition of "Underflow" in line 3 is deleted,
(2) the definition of "foo" in line 5-10 is deleted,
(3) "Matherr" is changed to "Underflow" in the catch statement in line 8, or
(4) "public" is changed to "private" in line 3.
## Attachments
- [432.cpp](/uploads/c3a89685372790a4946ec88f8e54c293/432.cpp)Virgile PrevostoVirgile Prevostohttps://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/907axiom "addr_le_def" given to Alt-Ergo considered too weak2021-08-05T14:15:00ZJochen Burghardtaxiom "addr_le_def" given to Alt-Ergo considered too weakID0002047:
**This issue was created automatically from Mantis Issue 2047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002047:
**This issue was created automatically from Mantis Issue 2047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002047 | Frama-Clang | Plug-in > wp | public | 2015-01-12 | 2015-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Jan2015-Neon-20140301+dev-STANC | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The loop invariant "xx5" of the attached program "fill1.c" can't be proven with Alt-Ergo. The goal reads fine, viz.:
goal fill_loop_inv_xx5_preserved:
forall a_3,a_2,a_1,a : addr.
(a_1 <> a_2) ->
addr_le(a_3, a_2) ->
(region(a.base) <= 0) ->
(region(a_3.base) <= 0) ->
addr_le(a_3, shift_sint16(a_2, 1))
However, the axiom "addr_le_def" appears to be too weak, it currently reads:
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
(addr_le(p, q) -> ((p).offset <= (q).offset))))
While the loop inveriant certainly should be provable, I don't see any way to prove a_3.base=a_2.base with the current version of the file.
Moreover, in order for axioms "addr_le_def" and "addr_le_def1" to be a definition of "addr_le(.,.)" in terms of "=" and "<=" etc., axiom "addr_le_def" should be changed to:
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)].
(addr_le(p, q) -> p.base = q.base and p.offset <= q.offset))
After that change, Alt-Ergo proves the goal without any problems. The attached file "fill_loop_inv_xx5_preserved_Alt-Ergo.mlw" contains the changed version in a comment at line 408.
If my argument is right, the whole axiomatization should be reviewed to remove similar flaws, which give Frama-C a rather poor performance on address arithmetic. (For that reason, I assigned a higher severity.)
### Additional Information :
Originally, I'd submitted this issue to the Alt-Ergo issue tracker, see https://github.com/OCamlPro/alt-ergo/issues/9. I'm indebted to Mohamed Iguernelala for hinting at the weak axiom "addr_le_def", where I had a blind spot.
## Attachments
- [fill1.c](/uploads/e5ff187165a5e10b7858e1f325eea68a/fill1.c)
- [fill_loop_inv_xx5_preserved_Alt-Ergo.mlw](/uploads/6292554fc2953d67792737e6dac31199/fill_loop_inv_xx5_preserved_Alt-Ergo.mlw)
- [fill.c](/uploads/c1dcc11d568e2e09d95aeabf0b9df093/fill.c)
- [fill4.c](/uploads/5ce99f117503a2df12c827af1b439520/fill4.c)
- [fill5.c](/uploads/ece00cbe919a18c0800d32b0adb27fb2/fill5.c)
- [fill4r.c](/uploads/81225ff5f9ecee0d89645919cbe59e44/fill4r.c)
- [find_arr.c](/uploads/fec90cf4fecefaee9a7cea344c14b693/find_arr.c)
- [find_ptr.c](/uploads/8430a7bbd76c8f263bd433d3cfd746d8/find_ptr.c)
- [find_ptr_foo_post_Alt-Ergo_modified.mlw](/uploads/d52e028cdf21562b07c9e340031cef8c/find_ptr_foo_post_Alt-Ergo_modified.mlw)Loïc CorrensonLoïc Corrensonhttps://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/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/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/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/865bitwise negation of uint introduces "-1" in Alt-Ergo obligation2021-02-22T13:41:06ZJochen Burghardtbitwise negation of uint introduces "-1" in Alt-Ergo obligationID0002023:
**This issue was created automatically from Mantis Issue 2023. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002023:
**This issue was created automatically from Mantis Issue 2023. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002023 | Frama-Clang | Documentation > ACSL | public | 2014-12-08 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
For the assertion in line 3 of the attached file "198.c", Frama-c generates the following proof obligation for Alt-Ergo: "goal foo_assert: forall i : int. is_uint32(i) -> ((-1) = i)". However, axiom "is_uint32_def" in line 430 of file "foo_assert_Alt-Ergo.mlw" says: "is_uint32(x) -> (0 <= x)", while "0 <= -1" is false (and unprovable as an own goal by Alt-Ergo).
As a consequence, there exists no (satisfiable) precondition "requires p(i)" that could be added as contract of "foo()" such that the assertion in line 3 becomes satisfiable, since "forall i : int. p(i) -> is_uint32(i) -> ((-1) = i)" implies "forall i : int. p(i) -> is_uint32(-1)". For example, requiring "i == 0xffffffffu" doesn't make line 3 provable, nor does any similar equation.
## Attachments
- [198.c](/uploads/43894779f84ecb85c5bbca9c5d4f60c5/198.c)
- [foo_assert_Alt-Ergo.mlw](/uploads/2d9028c59b5be767e57c7919eccb4d8b/foo_assert_Alt-Ergo.mlw)
- [198a.c](/uploads/387d28aa89210ab23bd7de97f80871b9/198a.c)
- [2compl.txt](/uploads/5886d302a5d8d0deae8deb56309ab3fe/2compl.txt)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/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/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 Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/643insufficient preconditions given to verify constructor call from global varia...2021-02-22T14:02:18ZJochen Burghardtinsufficient preconditions given to verify constructor call from global variable initializationID0002003:
**This issue was created automatically from Mantis Issue 2003. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002003:
**This issue was created automatically from Mantis Issue 2003. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002003 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
The predonditions of the cls() constructor aren't verified for the call originating from the declaration in line 9. The goal in the .mlw file is just "forall i : int. is_sint32(i) -> (0 <> i)", i.e. the fact that i (that is x in the C++ source) has the value 2 isn't given as precondition.
In contrast, when cls() is called explicitly in main(), the actual value of x is given - the .mlw file's goal for line 13 reads: "... -> (0 <> (safe_comp_div(1, 2)))". Note that here the effect of the line-9 cls()-call is ignored in x-value computation; in fact, already the cls()-call in line 12 will crash with zero-divide.
This issues is probably closely related to #2002.
## Attachments
- [178.cpp](/uploads/5a04d189eb4a14ee24fb23392f9ea5b5/178.cpp)
- [476.cpp](/uploads/383651d9a385b7199be6833e66e52491/476.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/868suggest to suppress warning about passing void value via return statement2021-02-22T13:26:54ZJochen Burghardtsuggest to suppress warning about passing void value via return statementID0001998:
**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 PrevostoVirgile Prevosto