frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-04-15T09:10:25Zhttps://git.frama-c.com/pub/frama-c/-/issues/620unable to use lemma separated_region2021-04-15T09:10:25ZJens Gerlachunable to use lemma separated_regionID0002041:
**This issue was created automatically from Mantis Issue 2041. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002041:
**This issue was created automatically from Mantis Issue 2041. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002041 | Frama-C | Plug-in > wp | public | 2014-12-28 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am using two Frama-C installation:
1.) Neon-20140301 installed through opam under OS X
2.) Neon-20140301+dev-stance manually installed under Linix
In both installations the lemma separated_region in file FRAMAC_SHARE/wp/coqwp/Memory.v
is unaccessible because it is put in comments.
I suspect that this is the reason why I cannot prove that a local struct variable is separated from one
that a function receives as an argument.
What is the reason that this lemma is not available?Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/369Frama-C sleeps too much when discharging trivial goals2021-04-15T09:08:16Zmantis-gitlab-migrationFrama-C sleeps too much when discharging trivial goalsID0002280:
**This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002280:
**This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002280 | Frama-C | Plug-in > wp | public | 2017-02-13 | 2017-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pkhuong | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Linux/x86_64 | **OS** | Linux | **OS Version** | 4.9.0-1-amd64 #1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have a largish C functions that generates ~70K goals (that I'm refactoring away). Verification with WP and RTE assertions succeeds, but takes ~14 minutes of real time. strace shows the majority of that time is spent executing *no syscall* (i.e., not calling external solvers) except printing the progress on stderr, getrusage, and nanosleeping for half a second. I LD_PRELOADed a shared object to turn usleep into a no-op, and that improved the runtime from 14 minutes to 3 minutes.
Could Frama-C sleep less when Qed does all the work?
### Steps To Reproduce :
frama-c slow_qed.c -cpp-gnu-like -no-asm-contracts -constfold -machdep x86_64 -implicit-function-declaration error -wp -wp-rte -wp-extensional -wp-split -wp-init-const -wp-prop="-trustme,-freeable,-@assigns,-@lemma,-@variant" -wp-prover=alt-ergo,Z3:4.5.0
## Attachments
- [slow_qed.c](/uploads/df95dd235b294d5f24c6ca57181db9d4/slow_qed.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/385WP inserts unwanted new lines into Coq proofs2021-04-15T09:00:28ZJens GerlachWP inserts unwanted new lines into Coq proofsID0002266:
**This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002266:
**This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002266 | Frama-C | Plug-in > wp | public | 2017-01-02 | 2017-01-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have noticed (since Aluminium) that whenever I work on a Coq proof, then WP adds a newline to all the other Coq proofs in wp0.script (right before "Qed.").
In the long run, it is a bit annoying to have all these empty lines in the coq proofs...Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/387Why3 warning2021-04-15T09:00:01ZJens GerlachWhy3 warningID0002263:
**This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002263:
**This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002263 | Frama-C | Plug-in > wp | public | 2016-12-16 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running WP I observe the following warning
[Config] reading extra configuration file /Users/jens/.opam/4.04.0/share/frama-c/wp/why3/why3.conf
File "/Users/jens/.opam/4.04.0/share/why3/drivers/smt-libv2.drv", line 34, characters 7-14:
Library file not found: int
The problem occurs both under Linux and macOS.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/388more prover processes run than expected2021-04-15T08:59:30ZJens Gerlachmore prover processes run than expectedID0002262:
**This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002262:
**This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002262 | Frama-C | Plug-in > wp | public | 2016-12-15 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I start WP with '-wp-par 4' (for example) I often observe that more than 4 prover processes are actually running.
### Additional Information :
I am not sure this is related but:
It happens from time to time that a proof obligations that is verified with '-wp-par 1' and given timeout T
is not verified when using a greater number of processes and the same timeout T.
### Steps To Reproduce :
run WP on example with a sufficiently large number of proof obligations that require more than one theorem prover
## Attachments
- ![screen-shot](/uploads/64bc6ecf07003613b00fa43be854d6b3/screen-shot.png)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/405error in Coq file generation2021-04-15T08:59:05ZAlain Giorgettierror in Coq file generationID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002260 | Frama-C | Plug-in > wp | public | 2016-12-03 | 2016-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | giorgetti | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When an ACSL axiomatic in a C file main.c contains a type declaration, say
type t;
the command
frama-c .. -wp main.c -wp-prover coqide ..
generates a wrong line
Parameter fct : Type.
in the file typed_fct/A_coq_.v.
### Additional Information :
Noticed during a meeting with L. CorrensonLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/409Nested scopes may cause issues with the validity of created pointers2021-04-15T08:57:59Zmantis-gitlab-migrationNested scopes may cause issues with the validity of created pointersID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002245 | Frama-C | Plug-in > wp | public | 2016-08-17 | 2016-08-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Upon entering a nested scope (caused by conditional blocks, or even just wrapping parts of code in {}), pointers once known as valid may become unknown in validity. This only seems to occur when more than 1 pointer is being reasoned about in the scope.
### Additional Information :
This bug occurs on both Sodium in Cygwin and Aluminum on Linux.
### Steps To Reproduce :
== Program bug.c:
/*@
ensures \valid(\result);
*/
int* foo();
void main() {
int* x = foo();
{
int y;
//@ assert \valid(x);
//@ assert \valid(&y);
}
}
== Command to run:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:6:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Unknown (51ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
== Expected output:
Both assertions to pass, since x is ensures to be valid, and the & operator always returns a valid pointer.
== Real output:
The pointer we ensure to be valid could not be proven to be valid.
Moving the definition of y to the outer scope fixes this issue, as well as moving the definition of x inside.
## Attachments
- [bug.c](/uploads/cfc99feea8974ba3cb5097bed4bfb3d3/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/508Validation fails when predicate is used with implicit type conversion.2021-04-15T08:54:27Zmantis-gitlab-migrationValidation fails when predicate is used with implicit type conversion.ID0002229:
**This issue was created automatically from Mantis Issue 2229. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002229:
**This issue was created automatically from Mantis Issue 2229. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002229 | Frama-C | Plug-in > wp | public | 2016-05-31 | 2016-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When there is an implicit type conversion on a parameter, and the value is checked by a predicate, validation fails when it should succeed.
In the example below, the functions foo and foo_pred have the same precondition, except foo_pred has the statement in a predicate. foo validates while foo_pred does not.
run2 validates the assertion, showing the precondition should be true, but foo_pred still fails.
run3 is similar to run2 except a ghost variable is used. This causes foo_pred to validate.
### Steps To Reproduce :
File foo.c (attached):
/*@
predicate bar_req(int i) = ((unsigned char) i) == i;
*/
//@ requires ((unsigned char) i) == i;
void foo(int i) {
}
//@ requires bar_req(i);
void foo_pred(int i) {
}
void run(char c) {
unsigned char uc = c;
foo(uc); // Valid
foo_pred(uc); // Fails
}
void run2(char c) {
unsigned char uc = c;
//@ assert ((unsigned char) ((int) uc)) == uc;
foo_pred(uc); // Fails
}
void run3(char c) {
unsigned char uc = c;
//@ ghost int ic = uc;
//@ assert ((unsigned char) ic) == uc;
foo_pred(uc); // Valid
}
Run command:
frama-c foo.c -wp -wp-prover why3:alt-ergo -wp-model=typed+Cast
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing foo.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [alt-ergo] Goal typed_cast_run2_call_foo_pred_pre : Unknown (158ms)
[wp] [alt-ergo] Goal typed_cast_run_call_foo_pred_pre : Unknown (Qed:0.54ms) (157ms)
[wp] Proved goals: 4 / 6
Qed: 3
alt-ergo: 1 (10ms) (unknown: 2)
## Attachments
- [foo.c](/uploads/792c293c47386d643589dcebe3f4d174/foo.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/509Oddities in the modeling of floats and doubles2021-04-15T08:53:31Zmantis-gitlab-migrationOddities in the modeling of floats and doublesID0002228:
**This issue was created automatically from Mantis Issue 2228. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002228:
**This issue was created automatically from Mantis Issue 2228. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002228 | Frama-C | Plug-in > wp | public | 2016-05-16 | 2016-05-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I a unsure of the modeling of floats and doubles provided in magnesium. There are three unexpected results I encountered.
1.
The following program proves the contradiction with the command:
frama-c -wp -wp-timeout 60 -wp-prover why3:z3-4.4.0 getNaN.c -no-tty
/*@ assigns \result;
ensures \is_NaN(\result);
*/
extern float getNaN();
void main() {
getNaN();
//@ assert Contradiction: \false;
}
2.
The following assertions are not proven (although I would expect them to be trivial) using the command:
frama-c -wp -wp-timeout 60 -wp-prover alt-ergo -no-tty fin.c
void foo() {
float a = 1.0;
//@ assert \is_finite(a);
}
void bar() {
double a = 1.0;
//@ assert \is_finite(a);
}
3.
The values for + or - INF are not modeled for floats or doubles. The following lemmas validate:
/*@
lemma inf_float:
\forall float x; \is_finite(x) || \is_NaN(x);
*/
/*@
lemma inf_double:
\forall double x; \is_finite(x) || \is_NaN(x);
*/Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/514Crash with large array initialisation2021-04-15T08:48:55Zmantis-gitlab-migrationCrash with large array initialisationID0002219:
**This issue was created automatically from Mantis Issue 2219. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002219:
**This issue was created automatically from Mantis Issue 2219. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002219 | Frama-C | Plug-in > wp | public | 2016-03-18 | 2016-03-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | szt | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86-64 | **OS** | GNU/Linux | **OS Version** | Ubuntu 14.04.4 |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
wp plugin crashes when I try to check code
### Additional Information :
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing ../../prog/array_testcase.c (with preprocessing)
[kernel] Current source was: ../../prog/array_testcase.c:1
The full backtrace is:
Raised at file "src/plugins/wp/register.ml", line 607, characters 30-32
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 778, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 227, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Magnesium-20151002.
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
### Steps To Reproduce :
just run
frama-c -wp -wp-proof alt-ergo array_testcase.c
## Attachments
- [array_testcase.c](/uploads/38b172c0d08b3e77a7af8dddf97dc43f/array_testcase.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/518WP detect a non-natural loop on a do-while(0) loop2021-04-15T08:47:58Zmantis-gitlab-migrationWP detect a non-natural loop on a do-while(0) loopID0001911:
**This issue was created automatically from Mantis Issue 1911. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001911:
**This issue was created automatically from Mantis Issue 1911. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001911 | Frama-C | Plug-in > wp | public | 2014-08-19 | 2016-03-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached example, the do-while(0) "false" loop makes the WP fail with the message:
wp2.c:8:[wp] warning: calculus failed on strategy
for 'main', behavior 'default!', all properties, both assigns or not because
unsupported non-natural loop without invariant property. (abort)
Maybe it can be detected that this is not a loop in fact ?
### Additional Information :
It is ok with -wp-invariants option.
### Steps To Reproduce :
$ frama-c -wp-fct main wp2.c
## Attachments
- [wp2.c](/uploads/b42a155d1a7118131a8c4260a6a121b4/wp2.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/526zombie processes (again)2021-04-15T08:46:59ZJens Gerlachzombie processes (again)ID0002205:
**This issue was created automatically from Mantis Issue 2205. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002205:
**This issue was created automatically from Mantis Issue 2205. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002205 | Frama-C | Plug-in > wp | public | 2016-02-01 | 2016-02-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is related #2154 and #2132.
I have updated my Frama-C installation under OS X with a patch provided by Loïc Correnson.
The situation has improved in the sense that my system is not so sluggish anymore but there still a substantial number of zombie processes: 86 (before the patch I counted 111 for the same example).
## Attachments
- [command.ml](/uploads/53d60edd523f389028615aaf8ed6c2a3/command.ml)
- [command.mli](/uploads/bf305b67d611a41cda9b7c025b58739d/command.mli)
- [task.ml](/uploads/122a5d6e2d50c4bfcf7d91c4148a15ea/task.ml)
- [task.mli](/uploads/2c222544f2dd773830d8266c242cc2d4/task.mli)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/584Unable to prove things that are provable, gets confused2021-04-15T08:45:52Zmantis-gitlab-migrationUnable to prove things that are provable, gets confusedID0002179:
**This issue was created automatically from Mantis Issue 2179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002179:
**This issue was created automatically from Mantis Issue 2179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002179 | Frama-C | Plug-in > wp | public | 2015-10-18 | 2015-10-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
In the attached file as is using wp -wp-model Typed,cast test-final.c, the last assert can't be proven, resulting in the ensures and assigns to be valid under hypotheses. This is a minimal version that still shows the problem.
However, there are several ways to make it be able to prove it and as far as I can see should have no effect on it. The different ways are:
- Removing any of the following 3 lines:
p[n] = 0x80; /* there is always room for one */
HASH_BLOCK_DATA_ORDER(c, p, 1);
c->num = 0;
- Removing the first assert
- Removing the requires \valid_read(c->data+(0 .. c->num-1));
I assume it gets confused because the \valid_read() overlaps with the \valid(c). It's not really needed. (In the full version the \valid_read() should more be something like \initialized.)
## Attachments
- [test-final.c](/uploads/d2b5913be633bcbecc3fbfb5a5fd886c/test-final.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/592incomplete Alt-Ergo obligation files generated in presence of lemma "forall i...2021-04-15T08:44:57ZJochen Burghardtincomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."ID0002169:
**This issue was created automatically from Mantis Issue 2169. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002169:
**This issue was created automatically from Mantis Issue 2169. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002169 | Frama-C | Plug-in > wp | public | 2015-09-21 | 2015-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 483.c -wp-out wp-out" on the attached file generates an Alt-Ergo obligation file "foo_assert_Alt-Ergo.mlw" which contains neither the lemma "xxx" nor the proof goal for the assertion in line 5. Apparently, Frama-C/Wp tacitly crashes during translating the lemma.
The problem disappears ifin line 2 "int" is changed to "integer", or "\false" is changed to some formula containing "x".
## Attachments
- [483.c](/uploads/b7743ec7ca8f15e3df9b2238386f8533/483.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/593suggest command-line option to avoid sophisticated expression transformations...2021-04-15T08:43:45ZJochen Burghardtsuggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligationsID0002168:
**This issue was created automatically from Mantis Issue 2168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002168:
**This issue was created automatically from Mantis Issue 2168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002168 | Frama-C | Plug-in > wp | public | 2015-09-21 | 2015-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 482b.c" on the attached file, the assertion "zzz" can't be proven by Alt-Ergo, although it should be an immediate consequence of assertion "yyy" and axiom "xxx". Looking at the file "bar_assert_zzz_Alt-Ergo.mlw" shows that some sophisticated expression transformations have been applied to the goal, but not to the axiom:
763 axiom Q_xxx:
764 forall lg_0,pos_0 : int.
765 (forall i : int. (pos_0 <= i) -> (i < (lg_0 + pos_0)) -> P_Tst(i)) ->
766 P_Prp(1 - lg_0)
772 goal bar_assert_zzz:
787 (forall i_1 : int. (i_1 < i) -> (x <= i_1) -> P_Tst(i_1)) ->
788 P_Prp(1 + x - i)
It is not a problem of Frama-C/Wp, but a problem of Alt-Ergo: it just should apply the lemma "xxx" with instantiation { pos_0:=x, lg_0 := i-x } to obtain line 788 from line 787.
However, when trying to prove the "zzz" assertion manually using Coq, Wp's transformation causes additional confusion. It would be desirable if the was a command-line switch to generate proof obligations as close to the source code as possible, i.e. to avoid the transformation.
As a side note, if the "assert" in line 20 is replaced by the statement-contract "ensures" in line 18, the transformation disappears, the goal is fairly good readable, and Alt-Ergo find the proof.
## Attachments
- [482b.c](/uploads/2c17baa4edc565f1b208267d133e0f42/482b.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/595assertion failure using memset on a char2021-04-15T08:43:01Zmantis-gitlab-migrationassertion failure using memset on a charID0002160:
**This issue was created automatically from Mantis Issue 2160. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002160:
**This issue was created automatically from Mantis Issue 2160. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002160 | Frama-C | Plug-in > wp | public | 2015-09-14 | 2015-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to analyse the this:
#include <string.h>
int main()
{
char a;
memset(&a, 0, 1);
}
Using wp I get:
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: No definition for 'memchr' interpreted as reads nothing
[wp] warning: No definition for 'strlen' interpreted as reads nothing
[wp] warning: No definition for 'memset' interpreted as reads nothing
[wp] warning: No definition for 'strchr' interpreted as reads nothing
[wp] warning: No definition for 'strcmp' interpreted as reads nothing
[wp] warning: No definition for 'strncmp' interpreted as reads nothing
[wp] warning: No definition for 'wcscmp' interpreted as reads nothing
[wp] warning: No definition for 'wcslen' interpreted as reads nothing
[wp] warning: No definition for 'wcsncmp' interpreted as reads nothing
[wp] warning: Missing RTE guards
[kernel] Current source was: test.c:6
The full backtrace is:
Raised at file "src/wp/MemVar.ml", line 474, characters 54-66
Called from file "src/wp/MemVar.ml", line 519, characters 16-38
Called from file "src/wp/MemVar.ml", line 543, characters 9-38
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/Lang.ml", line 735, characters 25-40
Called from file "src/wp/Warning.ml", line 139, characters 6-10
Called from file "src/wp/LogicSemantics.ml", line 813, characters 12-42
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/cfgWP.ml", line 1087, characters 18-60
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 1118, characters 23-207
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/calculus.ml", line 448, characters 14-224
Called from file "src/wp/calculus.ml", line 595, characters 10-57
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 724, characters 40-59
Called from file "set.ml", line 304, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/wp/calculus.ml", line 724, characters 4-64
Called from file "src/wp/calculus.ml", line 770, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1402, characters 39-62
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/wp/cfgWP.ml", line 1391, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 15-40
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 27-29
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (File "src/wp/MemVar.ml", line 474, characters 54-60: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
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_guidelinesLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/598Slow in proof obligation generation2021-04-15T08:41:46Zmantis-gitlab-migrationSlow in proof obligation generationID0002156:
**This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002156:
**This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002156 | Frama-C | Plug-in > wp | public | 2015-09-03 | 2015-09-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | juki21c | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Both Ubuntu and OS X | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I experienced that Frama-C/WP was very slow in generating the proof obligations only (skipping invoking any provers). For the attached files, code6.c takes about 1 min. code10.c takes about 15 min. code12.c abnormally terminates Frama-C with a stack overflow error.
### Steps To Reproduce :
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code6.c
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code10.c
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code12.c
## Attachments
- [code.zip](/uploads/f899faa93ff0631830e910686ea4ef7d/code.zip)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/803Able to assert a false statement2021-04-15T08:31:46Zmantis-gitlab-migrationAble to assert a false statementID0002087:
**This issue was created automatically from Mantis Issue 2087. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002087:
**This issue was created automatically from Mantis Issue 2087. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002087 | Frama-C | Plug-in > wp | public | 2015-03-03 | 2015-03-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached program, 'absurd' validates when it should not. The is only observed when all of the following conditions are met.
'num' must be part of a struct, which can be global (as in the program below) or returned from split.
Changing the assigns to only r.num cause the correct behavior. However, if the struct is returned from split, absurd still validates.
'split' must be called, if the body is inlined, the bad behavior is not observed.
Alt-ergo 0.99.1 must be used, can not replicate using 0.95.2
The expression must be '5/2', I have not found any other numbers that causes this behavior.
### Steps To Reproduce :
Create struc_div.c (attached):
struct result {
int num;
};
struct result r;
/*@
assigns r;
ensures r.num == 5/2;
*/
void split() {
r.num = 5/2;
}
void test_split() {
split();
//@ assert absurd: r.num == -99 && r.num == 99;
}
Run:
frama-c struct_div.c -wp -wp-rte
Results:
[kernel] preprocessing with "gcc -C -E -I. struct_div.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function split
[rte] annotating function test_split
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_split_post : Valid
[wp] [Qed] Goal typed_split_assign : Valid
[wp] [Alt-Ergo] Goal typed_test_split_assert_absurd : Valid (26ms) (18)
[wp] Proved goals: 3 / 3
Qed: 2
Alt-Ergo: 1 (26ms-26ms) (18)
Expected that 'absurd' assertion should not validate.
## Attachments
- [struct_div.c](/uploads/bcd65e49d23e7f76196a0a8f49474af9/struct_div.c)
- [foo.mlw](/uploads/7def6a9caa1198c52f69c52f37493bc9/foo.mlw)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1001assigns crash on incorrect locations2021-04-15T08:29:05Zmantis-gitlab-migrationassigns crash on incorrect locationsID0001844:
**This issue was created automatically from Mantis Issue 1844. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001844:
**This issue was created automatically from Mantis Issue 1844. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001844 | Frama-C | Plug-in > wp | public | 2014-07-17 | 2014-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boulme | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux Ubuntu 14.04 LTS | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the file "crash_assigns.c",
an invalid assign clause makes wp crash with the message:
Current source was: crash_assigns.c:5
The full backtrace is:
Raised at file "hashtbl.ml", line 353, characters 18-27
Called from file "hashtbl.ml", line 361, characters 22-38
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
### Additional Information :
Replacing the invalid assigns clause with a valid one like
assigns t[0..9];
makes the pb disappear...
### Steps To Reproduce :
run frama-c-gui crash_assigns.c
and try to prove assigns clause using wp.
## Attachments
- [crash_assigns.c](/uploads/b195abe901a4302f8d3fab7fb4ce8458/crash_assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1240Frama-C GUI discards candidate coq proof2021-04-15T08:23:28ZJens GerlachFrama-C GUI discards candidate coq proofID0001687:
**This issue was created automatically from Mantis Issue 1687. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001687:
**This issue was created automatically from Mantis Issue 1687. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001687 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2014-03-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The problem is as follows:
In a Coq proof we add the line
repeat (rewrite shift_zero in *).
When quitting the Coq IDE, coq complains (correctly) about the token "*)" and restores the original proof,
thus completely discarding the proof attempt.
The proof attempt should at least be saved, somehow.
### Additional Information :
Running release candidate of Frama-C Neon.Loïc CorrensonLoïc Correnson