frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-03-30T13:47:26Zhttps://git.frama-c.com/pub/frama-c/-/issues/182missing E-ACSL code, control flow graph, function pointer2021-03-30T13:47:26Zmantis-gitlab-migrationmissing E-ACSL code, control flow graph, function pointerID0002416:
**This issue was created automatically from Mantis Issue 2416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002416:
**This issue was created automatically from Mantis Issue 2416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002416 | Frama-C | Plug-in > E-ACSL | public | 2018-12-11 | 2018-12-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.18 Ocaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Is there a workaround for the function pointer limitation
//////////////// cfg.c
void func(void)
{
int i = 0 ;
int *ptr = &i;
/*@ assert \valid(ptr); */
*ptr = 0 ;
}
int main(int argc, char **argv)
{
void (*ptr_func)(void) = &func;
(*ptr_func)();
return 0;
}
////////////////
### Additional Information :
I would like to find a solution that do not involve :
- the use of EVA
OR
- modifying the code
### Steps To Reproduce :
$ frama-c -machdep gcc_x86_64 cfg.c -e-acsl -then-last -print -ocode cfg.e-acsl.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing cfg.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] cfg.c:12: Warning:
function pointers may introduce too limited instrumentation.
[e-acsl] translation done in project "e-acsl".
$ gcc -DE_ACSL_SEGMENT_MMODEL -Wno-attributes -I$(frama-c -print-share-path)/e-acsl/ -o cfg.e-acsl cfg.e-acsl.c $(frama-c -print-share-path)/e-acsl/e_acsl_rtl.c $(frama-c -print-share-path)/../../lib/libeacsl-dlmalloc.a $(frama-c -print-share-path)/../../lib/libeacsl-gmp.a -lm
$ ./cfg.e-acsl
Assertion failed at line 5 in function func.
The failing predicate is:
\valid(ptr).
AbortedJulien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/181Missing cast in code generated by RTE2021-04-20T07:27:57ZJulien SignolesMissing cast in code generated by RTEID0002419:
**This issue was created automatically from Mantis Issue 2419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002419:
**This issue was created automatically from Mantis Issue 2419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002419 | Frama-C | Plug-in > RTE | public | 2018-12-17 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
==========
int main(void) {
int i = 2;
unsigned int j = i < 2;
return 0;
}
$ frama-c -check -rte -warn-unsigned-downcast -print -ocode res.c
[kernel] Parsing a.c (with preprocessing)
[rte] annotating function main
/* Generated by Frama-C */
int main(void)
{
int __retres;
int i = 2;
/*@ assert rte: unsigned_downcast: (i < 2) ≤ 4294967295; */
/*@ assert rte: unsigned_downcast: 0 ≤ (i < 2); */
unsigned int j = (unsigned int)(i < 2);
__retres = 0;
return __retres;
}
$ frama-c res.c
[kernel] Parsing res.c (with preprocessing)
[kernel:annot-error] res.c:6: Warning:
comparison of incompatible types: 𝔹 and ℤ. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
==========
The terms (i < 2) should be casted to int in the generated predicatesJulien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/180E-ACSL crash with RTE generated assertion with booleans2021-04-20T07:09:09Zmantis-gitlab-migrationE-ACSL crash with RTE generated assertion with booleansID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002412 | Frama-C | Plug-in > E-ACSL | public | 2018-12-03 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux x86_64 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
There might be a regression with the RTE or E-ACSL plugin with Argon.
/////////// boolean.c
#include <stdbool.h>
bool return_false(void)
{
return false;
}
int main(void)
{
return 0;
}
///////////////////////////
### Additional Information :
On Chlorine-20180502 (bfd93b819) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
### Steps To Reproduce :
On Argon 18.0 (2f7a0eee0) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Current source was: rte_boolean.c:10
The full backtrace is:
Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023
Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 18.0 (Argon).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [boolean.c](/uploads/1b34c066b4dc860013dcc10c38a49aad/boolean.c)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/179Can't use e-acsl on a dynamic library containing all the instrumentations2023-03-22T03:49:51Zmantis-gitlab-migrationCan't use e-acsl on a dynamic library containing all the instrumentationsID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002422 | Frama-C | Plug-in > E-ACSL | public | 2019-01-22 | 2019-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.19 Ocaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 19-Potassium | **Fixed in Version** | - |
### Description :
Hi !
main.c contains the entry point : the main function and is not instrumented by frama-c
it calls instrumented func.c (e-acsl.func.c containing the __e_acsl_memory_init call) compiled as a dynamic library libe-acsl.func.so
then the e-acsl code segfault at
e_acsl_segment_tracking.h:815
### Additional Information :
Why the hell am I doing this ? :)
Contiki-NG is an IoT OS. It can be build as a firmware for several IoT devices, as a ELF for Linux x86/x86_64, and as a shared library loaded by the Java Cooja network simulator (with some JNI).
Before experimenting with dlopen in C and JNI in Java, which is going to fail because of the __executable_start symbol at ./share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h:47
(this will the subject of another future post)
I would like to be able, as a first step, to use a e-acsl instrumented dynamic library used by a non-instrumented program (containing main or not).
I am open to a solution that eventually needs some change inside the C E-ACSL code.
### Steps To Reproduce :
$ make
rm -vf *.*o ./loader ./main *e-acsl*
frama-c -main func -variadic-no-translation -machdep gcc_x86_64 -c11 -cpp-extra-args="-std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64" -no-frama-c-stdlib func.c -e-acsl-prepare -rte -warn-signed-overflow -warn-unsigned-overflow -warn-signed-downcast -warn-unsigned-downcast -rte-div -rte-float-to-int -rte-mem -rte-pointer-call -rte-shift -rte-no-trivial-annotations -then -e-acsl -e-acsl-full-mmodel -then-last -print -ocode e-acsl.func.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing func.c (with preprocessing)
[rte] annotating function __bswap_16
[rte] annotating function __bswap_32
[rte] annotating function __bswap_64
[rte] annotating function __uint16_identity
[rte] annotating function __uint32_identity
[rte] annotating function __uint64_identity
[rte] annotating function func
[e-acsl] beginning translation.
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap16, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap32, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap64, generating default assigns from the prototype
[kernel:annot:missing-spec] /usr/include/stdio.h:332: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
gcc -shared -fPIC -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_STACK_SIZE=32 -DE_ACSL_HEAP_SIZE=128 -std=c99 -m64 -O0 -g -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jean/local-frama-c/share/frama-c/e-acsl/ -o libe-acsl.func.so e-acsl.func.c /home/jean/local-frama-c/share/frama-c/e-acsl/e_acsl_rtl.c /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-dlmalloc.a /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-gmp.a -lm
gcc -o main main.c -L. -le-acsl.func
LD_LIBRARY_PATH=:./ ./main
Segmentation fault
make: *** [Makefile:11: e-acsl-main-shared] Error 139
## Attachments
- [e-acsl-is-fun.tar](/uploads/c1c5ac773627666455f1b0a93e66da53/e-acsl-is-fun.tar)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/178option -report-csv doesn't work anymore ?2021-02-22T12:55:41ZPatricia Mouyoption -report-csv doesn't work anymore ?ID0002423:
**This issue was created automatically from Mantis Issue 2423. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002423:
**This issue was created automatically from Mantis Issue 2423. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002423 | Frama-C | Plug-in > report | public | 2019-01-22 | 2019-01-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pmo | **Assigned To** | maroneze | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | linux | **OS** | ubuntu | **OS Version** | 4.18 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 19-Potassium | **Fixed in Version** | - |
### Description :
this option seems to be deprecated now ...
I know there is a new option to make report with Eva but only for red alarms and only with eva - I want a complete report as before with -report-csv
There is no indication at all in the changelog or maybe I've missed something ?
Is there a new way to use this option or another option to have the same result ?https://git.frama-c.com/pub/frama-c/-/issues/177Incorrect handling of \initialized when initialized struct is passed to a fun...2022-09-28T11:30:33ZKostyantyn VorobyovIncorrect handling of \initialized when initialized struct is passed to a function by valueID0002310:
**This issue was created automatically from Mantis Issue 2310. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002310:
**This issue was created automatically from Mantis Issue 2310. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002310 | Frama-C | Plug-in > E-ACSL | public | 2017-06-13 | 2019-01-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
This test case is derived from Toyota ITC benchmarks (File uninit_var.c, test case 012). Consider the following code:
struct S1 {
int t;
};
int foo(struct S1 s) {
/*@assert \initialized(&s.t); */
if (s.t > 0) return 0;
return 1;
}
int main(int argc, const char **argv) {
struct S1 s;
s.t = 1;
foo(s);
return 0;
}
Field `t` of struct `S1` is initialized in `main` but when it is passed to `foo` (by value) it's a brand new block where field `t` is not marked as initialized. Consequently assertion in `foo` wrongly fails.
## Attachments
- [itc-uninit-var-12.c](/uploads/4d29c1dc6442465e49a331c23bdd24b3/itc-uninit-var-12.c)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/174Failure to record global variable with initialiser2022-09-28T12:12:55ZKostyantyn VorobyovFailure to record global variable with initialiserID0002194:
**This issue was created automatically from Mantis Issue 2194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002194:
**This issue was created automatically from Mantis Issue 2194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002194 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2019-01-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
/* The following example wrongly fails the assertion */
#include <inttypes.h>
char *B = "foo";
unsigned long ref() {
return (intptr_t)B;
}
int main(int argc, char **argv) {
char *ptr = (char*)ref();
//@ assert \valid_read(ptr);
return 0;
}
### Additional Information :
This seems to be the case where memory analysis incorrectly determines that global variable 'B' should not be modelled and therefore it is omitted from the instrumentation.Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/172Failure to detect overflows into an allocated area within a struct2021-02-22T13:35:04ZKostyantyn VorobyovFailure to detect overflows into an allocated area within a structID0002327:
**This issue was created automatically from Mantis Issue 2327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002327:
**This issue was created automatically from Mantis Issue 2327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002327 | Frama-C | Plug-in > E-ACSL | public | 2017-08-24 | 2019-01-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Presently E-ACSL treats structs as single units of program allocation issuing one call to `store_block` per struct. Such an approach fails to detect overflows within structs. Consider, for instance, the following program:
int main() {
struct node {
char buf1[8];
char buf2[8];
} n;
/*@assert manual_assertion: \valid(&n.buf1[12]); */
n.buf1[12] = '0';
return 0;
}
This program results in an overflow via assignment n.buf1[12] = '0'; that accesses buffer n.buf2 via n.buf1. However, since E-ACSL treats n as a single memory block the issue is not detected.Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/169One \valid seems sufficient to write in a whole array.2021-02-22T12:55:31Zmantis-gitlab-migrationOne \valid seems sufficient to write in a whole array.ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002426 | Frama-C | Plug-in > wp | public | 2019-02-12 | 2019-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | VincentPenelle | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Linux Manjaro | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am on Chlorine version.
When I try to verify the following function with RTE guard enabled, WP succeeds. However, I think it should not, as only the first cell is specified to be valid, the rest is just specified to have valid read.
/*@ requires \valid(a);
@ requires \valid_read(a + (0 .. n-1));
@ requires 0 <= n <= INT_MAX;
*/
void foo(int *a, int n){
/*@ loop invariant 0 <= i <= n;
@ loop invariant \valid(a + (0 .. n-1));
*/
for (int i = 0; i<n;i++) a[i] = i;
}
Note: that works as well without any loop.
It doesn't work if you declare to pointers with different names, and declare one to be \valid and the other to be \valid_read (like in swap function for example).
It looks like the loop invariant \valid is simplified to true by Qed.
If that's normal, please explain me why.
Thanks,
--
Vincent Penelle.
### Steps To Reproduce :
Specify an array as being \valid_read, and one of its cells to be \valid.
Then, try to write in any cell.
Generate the RTE guards. WP should succeed to prove that the cells you're writing in are \valid.https://git.frama-c.com/pub/frama-c/-/issues/168Division by zero doesn't increase the number of VC in console output2021-02-22T12:55:28Zmantis-gitlab-migrationDivision by zero doesn't increase the number of VC in console outputID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002428 | Frama-C | Plug-in > wp | public | 2019-02-17 | 2019-02-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Obvious division by zero doesn't increase the total number of proof obligations:
Test2:
<pre>
/*@ assigns \nothing;
*/
int test2(int a)
{
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test2.c (with preprocessing)
[rte] annotating function test2
[rte] test2.c:5:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
Proved goals line is the same as in the case without division:
Test1:
<pre>
/*@ assigns \nothing;
*/
int test1(int a)
{
return a;
}
</pre>
Frama-C output:
<pre>
[kernel] Parsing test1.c (with preprocessing)
[rte] annotating function test1
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
From my point of view this is an incorrect behavior and the proved goals like should be 'Proved goals: 1 / 2' as in this case:
Test3:
<pre>
/*@ assigns \nothing;
*/
int test3(int a)
{
//@ assert 0 != 0;
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test3.c (with preprocessing)
[rte] annotating function test3
[rte] test3.c:6:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_test3_assert : Unknown (109ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
</pre>
## Attachments
- [test2.c](/uploads/6a8a966174608d26a4e3aaca44d430f1/test2.c)https://git.frama-c.com/pub/frama-c/-/issues/166kernel generates UnspecifiedSequence when 2 following ternary operators2021-02-22T13:34:58Zmantis-gitlab-migrationkernel generates UnspecifiedSequence when 2 following ternary operatorsID0002435:
**This issue was created automatically from Mantis Issue 2435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002435:
**This issue was created automatically from Mantis Issue 2435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002435 | Frama-C | Kernel | public | 2019-05-07 | 2019-05-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 Linux 4.19 | **OS** | OCaml 4.07.1 Opam 2.0.3 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider ternary_operator.c :
/////////////////
int main() {
return (2>1) ? 1 : (1>0) ? 1 : 0;
}
/////////////////
then frama-c generates :
/////////////////
int main(void)
{
int tmp_0;
if (2 > 1) tmp_0 = 1;
else {
int tmp;
if (1 > 0) tmp = 1; else tmp = 0;
tmp_0 = tmp;
}
return tmp_0;
}
//////////////
and considers :
if (1 > 0) tmp = 1; else tmp = 0;
tmp_0 = tmp;
as an UnspecifiedSequence statement
if (1 > 0) tmp = 1; else tmp = 0;
as a "If" statement
and
tmp_0 = tmp;
as a "Instr" statement
Is the construction of the AST with a intermediate UnspecifiedSequence the normal behaviour ?
## Attachments
- [ternary_operators.c](/uploads/90d149e439b96c230c8a26e90e2192da/ternary_operators.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/164frama-c installation needs dune > 1.5 package installed2022-07-28T11:34:57Zmantis-gitlab-migrationframa-c installation needs dune > 1.5 package installedID0002448:
**This issue was created automatically from Mantis Issue 2448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002448:
**This issue was created automatically from Mantis Issue 2448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002448 | Frama-C | Documentation > website | public | 2019-06-04 | 2019-06-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | varosi | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | macOS | **OS Version** | Mojave |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Installation instructions here - https://frama-c.com/install-18.0-Argon.html#installing-frama-c-on-macos
Doesn't tell that dune package in spam should be > 1.5. This brakes build with strange message telling the reverse:
# Error: Version 1.5 of dune is not supported.
# Supported versions:
# - 0.0
# - 1.0 to 1.1
If you do install later package with:
opam install dune.1.9.3
Everything works just fine. So it would make life of newcomers like me easier if this is said in install instructions here:
https://frama-c.com/install-18.0-Argon.html#installing-frama-c-on-macosFrançois BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/163invalid links to "ACSL by Example"2021-03-30T11:18:12ZJens Gerlachinvalid links to "ACSL by Example"ID0002449:
**This issue was created automatically from Mantis Issue 2449. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002449:
**This issue was created automatically from Mantis Issue 2449. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002449 | Frama-C | Documentation > website | public | 2019-06-08 | 2019-06-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The WP webpage (https://frama-c.com/wp.html) uses old (abandoned) links to "ACSL by Example".
I suggest to replace the link
http://www.fokus.fraunhofer.de/download/acsl_by_example
with
https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf
and the link
https://gitlab.fokus.fraunhofer.de/verification/open-acslbyexample.git
with
https://github.com/fraunhoferfokus/acsl-by-example
### Additional Information :
The suggested links have been stable for a couple of years now.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/160Does not build with OCaml 4.08.02022-09-28T11:03:06Zmantis-gitlab-migrationDoes not build with OCaml 4.08.0ID0002456:
**This issue was created automatically from Mantis Issue 2456. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002456:
**This issue was created automatically from Mantis Issue 2456. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002456 | Frama-C | Kernel > Makefile | public | 2019-06-18 | 2019-06-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | -current |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
The build fails with OCaml 4.08.0:
Packing /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.cmo
File "_none_", line 1:
Error: The implementation (obtained by packing)
does not match the interface /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.mli:
...
In module Cint:
Values do not match:
val is_cint_simplifier : Conditions/1.simplifier
is not included in
val is_cint_simplifier : Conditions/2.simplifier
File "src/plugins/wp/Cint.mli", line 80, characters 0-45:
Expected declaration
File "src/plugins/wp/Cint.mli", line 80, characters 0-45:
Actual declaration
File "_none_", line 1:
Definition of module Conditions/1
File "_none_", line 1:
Definition of module Conditions/2
gmake: *** [src/plugins/wp/.Makefile.plugin.generated:580: /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.cmo] Error 2
I suspect the problem lies in there being multiple identical Wp.mli files, each declaring the same Conditions module, which OCaml 4.08.0 now does not view as identical.François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/159Ambiguous path error using why32021-02-22T12:55:18Zmantis-gitlab-migrationAmbiguous path error using why3ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002454 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
### Steps To Reproduce :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
## Attachments
- [example.c](/uploads/ba254a88318716a5e0665ff9fe46d1f4/example.c)https://git.frama-c.com/pub/frama-c/-/issues/158build failure due to mangled variable assignment in Makefile2022-09-28T11:02:51Zmantis-gitlab-migrationbuild failure due to mangled variable assignment in MakefileID0002458:
**This issue was created automatically from Mantis Issue 2458. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002458:
**This issue was created automatically from Mantis Issue 2458. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002458 | Frama-C | Kernel > configure | public | 2019-06-20 | 2019-06-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | 6.5-current |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
here's the patch:
Index: Makefile.generating
--- Makefile.generating.orig
+++ Makefile.generating
@@ -153,8 +153,8 @@ endif
ifeq ($(HAS_OCAML408),yes)
DYNLINK_INIT=fun () -> ()
FORMAT_STAG=stag
- FORMAT_STRING_OF_STAG=match s with\n\
- | Format.String_tag str -> str\n\
+ FORMAT_STRING_OF_STAG=match s with \
+ | Format.String_tag str -> str \
| _ -> raise (Invalid_argument "unsupported tag extension")
FORMAT_STAG_OF_STRING=Format.String_tag s
else
The \n quoting does not work on GNU make 4.2.1. I get
FORMAT_STRING_OF_STAG='match s withn | Format …`
The GNU make manual recommends to use the 'define' keyword to assign multi-line values to make variables, but why bother? We don't need the linebreaks, do we?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/157configure does not detect gtksourceview due to wrong path2022-09-28T11:03:51Zmantis-gitlab-migrationconfigure does not detect gtksourceview due to wrong pathID0002457:
**This issue was created automatically from Mantis Issue 2457. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002457:
**This issue was created automatically from Mantis Issue 2457. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002457 | Frama-C | Kernel > configure | public | 2019-06-20 | 2019-06-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | 6.5 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is on 19.0-beta2.
due to looking in the wrong directory, gtksourceview is not found.
Diff can be found in `Additional Information`
### Additional Information :
Index: configure.in
--- configure.in.orig
+++ configure.in
@@ -975,8 +975,8 @@ else
fi
configure_library([GTKSOURCEVIEW],
- [$SOURCEVIEW_PATH/lablgtksourceview2.$LIB_SUFFIX,
- $SOURCEVIEW_PATH/lablgtk3_sourceview3.$LIB_SUFFIX],
+ [$LABLGTKPATH_FOR_CONFIGURE/lablgtksourceview2.$LIB_SUFFIX,
+ $LABLGTKPATH_FOR_CONFIGURE/lablgtk3_sourceview3.$LIB_SUFFIX],
[lablgtksourceview not found],
no)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/155External provers broken with 19.0-beta12021-02-22T12:55:13Zmantis-gitlab-migrationExternal provers broken with 19.0-beta1ID0002437:
**This issue was created automatically from Mantis Issue 2437. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002437:
**This issue was created automatically from Mantis Issue 2437. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002437 | Frama-C | Kernel | public | 2019-05-20 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bpc | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 GNU/Linux | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
External provers, with why3, look broken with 19.0-beta1 :
$ frama-c -wp -wp-prover why3:z3 swap.c
[kernel] Parsing swap.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [z3] Goal typed_swap_ensures_A : Unknown (Qed:3ms) (51ms)
[wp] Proved goals: 3 / 4
Qed: 3 (0.38ms-0.63ms-0.77ms)
Z3: 0 (unknown: 1)
Same problem using why3:cvc4-15 and why3:alt-ergo.
With the "native" alt-ergo, no problem :
$ frama-c -wp -wp-prover alt-ergo swap.c
[kernel] Parsing swap.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] Proved goals: 4 / 4
Qed: 3 (0.60ms-1ms-3ms)
Alt-Ergo: 1 (11ms) (40)
### Additional Information :
$ opam list
# Packages matching: installed
# Name # Installed # Synopsis
alt-ergo 2.3.0 The Alt-Ergo SMT prover
alt-ergo-lib 2.3.0 The Alt-Ergo SMT prover library
alt-ergo-parsers 2.3.0 The Alt-Ergo SMT prover parser library
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
biniou 1.2.0 Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve
camlp5 7.06.10-g84ce6cc4 Preprocessor-pretty-printer of OCaml
camlzip 1.07 Provides easy access to compressed files in ZIP, GZIP and JAR format
conf-autoconf 0.1 Virtual package relying on autoconf installation
conf-gmp 1 Virtual package relying on a GMP lib system installation
conf-gnomecanvas 2 Virtual package relying on a Gnomecanvas system installation
conf-graphviz 0.1 Virtual package relying on graphviz installation
conf-gtksourceview 2 Virtual package relying on a GtkSourceView system installation
conf-m4 1 Virtual package relying on m4
conf-perl 1 Virtual package relying on perl
conf-pkg-config 1.1 Virtual package relying on pkg-config installation
conf-python-2-7 1.0 Virtual package relying on Python-2.7 installation
conf-which 1 Virtual package relying on which
coq 8.9.0 Formal proof management system
cppo 1.6.5 Equivalent of the C preprocessor for OCaml programs
dune 1.9.3 Fast, portable and opinionated build system
easy-format 1.3.1 High-level and functional interface to the Format module of the OCaml standard library
frama-c 19.0.beta1 pinned to version 19.0.beta1 at git+https://github.com/Frama-C/Frama-C-snapshot.git#latest
jbuilder transition This is a transition package, jbuilder is now named dune. Use the dune
lablgtk 2.18.8 OCaml interface to GTK+
menhir 20181113 An LR(1) parser generator
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-config 1 OCaml Switch Configuration
ocaml-system 4.05.0 The OCaml compiler (system version, from outside of opam)
ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
ocamlfind 1.8.0 A library manager for OCaml
ocamlgraph 1.8.8 A generic graph library for OCaml
ocplib-simplex 0.4 A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities and optimizing linear objective functions
psmt2-frontend 0.2 A library to parse and type-check a conservative extension of the SMT-LIB 2 standard with prenex polymorphism
seq 0.1 Compatibility package for OCaml's standard iterator type starting from 4.07.
why3 1.2.0 Why3 environment for deductive program verification
yojson 1.7.0 Yojson is an optimized parsing and printing library for the JSON format
z3 4.8.4 Z3 solver
zarith 1.7 Implements arithmetic and logical operations over arbitrary-precision integers
## Attachments
- [swap.c](/uploads/cdbec3e4e4a47f15ad17c1c3703832b9/swap.c)
- [tst.c](/uploads/d3498f1224a689c944bb6c4ef8857c30/tst.c)https://git.frama-c.com/pub/frama-c/-/issues/154handling of escape sequences2021-02-22T13:40:11Zmantis-gitlab-migrationhandling of escape sequencesID0002382:
**This issue was created automatically from Mantis Issue 2382. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002382:
**This issue was created automatically from Mantis Issue 2382. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002382 | Frama-C | Kernel | public | 2018-07-03 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
Code:
<pre>
/*@
predicate isspace(integer c) = c == ' ' || c == '\f' || c == '\n' ||
c == '\r' || c == '\t' || c == '\v';
*/
</pre>
Error:
<pre>
[kernel] Parsing test.h (with preprocessing)
test.h:2:[kernel] failure: Unknown error (File "src/kernel_internals/parsing/logic_lexer.mll", line 390, characters 20-26: Assertion failed)
</pre>
Need to support '\v'.
## Attachments
- [escape_sequences.c](/uploads/24f837eb87b6ff67601f79146e0f08eb/escape_sequences.c)https://git.frama-c.com/pub/frama-c/-/issues/151number of generated files in Frama-C 18 vs 19. beta(2)2021-02-22T12:54:59ZJens Gerlachnumber of generated files in Frama-C 18 vs 19. beta(2)ID0002453:
**This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002453:
**This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002453 | Frama-C | Plug-in > wp | public | 2019-06-14 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
This entry references issue
https://github.com/Frama-C/Frama-C-snapshot/issues/21
in order to be able to easily add files.
### Steps To Reproduce :
Run the command
frama-c -pp-annot -no-unicode -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast -wp-model Typed+ref -wp-out rc.wp rc.c
on the attached files.
As mentioned in the github issue, both 18.0 and 19.beta(2) report 17 VC of which 5 are discharged by Qed and the remaining 12 are verified by Alt-Ergo.
However, Frama-C 18.0 generates 12 .mlw and .out files, respectively.
Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files, respectively.
The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged by Alt-Ergo.
## Attachments
- [rc.c](/uploads/12c6518483a56dad661d3ee7feabf59b/rc.c)