frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:07:23Zhttps://git.frama-c.com/pub/frama-c/-/issues/617deficient axioms2021-02-22T13:07:23ZDavid Cokdeficient axiomsID0002138:
**This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002138:
**This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002138 | Frama-C | Plug-in > wp | public | 2015-06-29 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The proof of the following with -WP and alt-ergo fails:
/*@
requires (int)(x+y) == x+y;
ensures \result == x+y;
*/
int f(int x, int y) {
return x+y;
}
On inspecting the intermediate artifacts, we identified the problem as inadequate axioms. Two solutions requiring changes in axioms worked for us.
However, I don't know if either change would have wider ramifications.
1)
axiom is_to_sint32 :
(forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))
The effect of the triggers in this axiom is simply to allow is_sint32(to_sint32(x)) to be reduced to true. In fact the more common need is to know that to_sint32(x) satisfies is_sint32. The proof above goes through if the trigger is changed to
axiom is_to_sint32 :
(forall x:int [to_sint32(x)]. is_sint32(to_sint32(x)))
2)
axiom id_sint32 :
(forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and
(x < 2147483648)) -> (to_sint32(x) = x)))
This axiom is much more useful if it is written as an equivalence instead of an implication. Doing so also enables the proof of the program above to go through.https://git.frama-c.com/pub/frama-c/-/issues/618Sessions and WP do not interact properly2021-02-22T13:07:24Zmantis-gitlab-migrationSessions and WP do not interact properlyID0002044:
**This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002044:
**This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002044 | Frama-C | Plug-in > wp | public | 2015-01-06 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Bonjour, quelques problèmes avec le -save et le -load des sessions conjugés avec WP/Why3 et l'option no-let !!!!
1. Si on utilise pas -wp-out les fichiers temporaires de wp sont supprimés et lors du prochain appel de frama-c avec le -load, il se plaint de l'absence des fichiers
2. Si on specifie -wp-out, avec le -load, Frama-C retrouve les fichiers générés mais il ne semble pas retrouver tout ce dont il a besoin.
3. Enfin lors de l'utilisation de coq comme prover lors d'un run (avec -load et -save), au prochain appel avec toujours -load et -save, frama-c appelle systématiquement coq, y compris si on specifie -wp-prover altergo par exemple.
### Steps To Reproduce :
Pour les points 1 et 2:
Par exemple, pour le fichier C suivant:
$ cat essai.c
struct greycounter_mem {_Bool _first; };
/*@ requires \valid(self);
@ ensures ((*self)._first ==1);
@ assigns *self;*/
void greycounter_reset (struct greycounter_mem *self) {
self->_first = 1;;
return;
}
Le script suivant active les différents problemes:
#!bin/bash
src=essai.c
# Error 1: temporary wp folder with no-let option and why3 solver (eg. altergo or CVC4)
frama-c -save session -wp-prop "@ensures" -wp-prover why3:altergo -wp-no-let $src
frama-c -load session -save session -wp-prop "@assigns" $src
# Error 2: no-let with why3:cvc4
frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-no-let -wp-out wp
frama-c -load session -save session -wp-prop "@assigns" $src
# Here it works
frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-out wp
frama-c -load session -save session -wp-prop "@assigns" $srchttps://git.frama-c.com/pub/frama-c/-/issues/627Range of remainder of two positive integers, wrong and missing assertions.2021-02-22T13:07:39Zmantis-gitlab-migrationRange of remainder of two positive integers, wrong and missing assertions.ID0002129:
**This issue was created automatically from Mantis Issue 2129. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002129:
**This issue was created automatically from Mantis Issue 2129. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002129 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Nitrogen-20111001
alt-ergo 0.94
False negative and false positive int the following code.
/*@ requires 0 <= n; */
void modulo_testcase_0(unsigned n) {
/*@ ghost unsigned q = n / 2; */
/*@ ghost unsigned r = n % 2; */
/*@ assert 0 <= n; */ /* OK */
/*@ assert n == 2*q + r; */ /* OK */
/*@ assert 0 <= q; */ /* OK */
/*@ assert 0 <= r < 1; */ /* NOK, cannot be proven */
}
/*@ requires 0 <= n && 0 < d; */
void modulo_testcase_1(int n, int d) {
/*@ assert n <= d * (n / d); */ /* NOK, cannot be proven */
/*@ ghost int q = n / d; */ /* OK */
/*@ ghost int r = n % d; */ /* OK */
/*@ assert 0 <= r < 1; */ /* NOK, r < d is true */
/*@ assert n <= d * (n / d); */ /* OK */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [modulo_testcase.c](/uploads/b725efd4758f124867c970e99d059011/modulo_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/628*off == off_cpy cannot be proven just after the assignment *off = off_cpy2021-02-22T13:07:41Zmantis-gitlab-migration*off == off_cpy cannot be proven just after the assignment *off = off_cpyID0002130:
**This issue was created automatically from Mantis Issue 2130. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002130:
**This issue was created automatically from Mantis Issue 2130. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002130 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Nitrogen-20111001
alt-ergo 0.94
#include <stddef.h>
/*
* Can memory zones be declared disjoint? For instance:
* \disjoint(off, buf + *off)
*
* wp does not accept and thus gracefully skips the following try:
* @ requires \forall size_t i;
* 0 <= i < sizeof(*off) ==> (char *) off != buf + (*off + i);
*/
/*@
@ requires \valid(off) && \valid(buf + *off);
@ assigns *off, buf[*off];
@ ensures *off == \old(*off) + 1;
@ ensures buf[\old(*off)] == '\0';
@*/
void alias_testcase_0(char *const buf, size_t *const off) {
size_t off_cpy = *off; /* restricted pointers cannot be required */
buf[off_cpy++] = '\0';
/*@ assert off_cpy - 1 == \at(*off, Pre); */ /* OK */
/*@ assert buf[off_cpy - 1] == '\0'; */ /* OK */
*off = off_cpy;
/*@ assert *off == off_cpy; */ /* NOK, cannot be proven */
/*@ assert buf[\at(*off, Pre)] == '\0'; */ /* NOK, cannot be proven */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [alias_testcase.c](/uploads/65a0be19399d07141588a8edf1eeb1c0/alias_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/631*i == *j cannot be proven from i == j2021-02-22T13:07:43Zmantis-gitlab-migration*i == *j cannot be proven from i == jID0002128:
**This issue was created automatically from Mantis Issue 2128. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002128:
**This issue was created automatically from Mantis Issue 2128. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002128 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | virgile | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Nitrogen-20111001
alt-ergo 0.94
The following assertion cannot be proven.
void pointer_testcase(int *i, int *j) {
/*@ assert i == j ==> *i == *j; */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [pointer_testcase.c](/uploads/ec0d97eb74499b149912f74f57f48a94/pointer_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/682CVC4 results are not displayed in the GUI2021-02-22T13:08:57ZJens GerlachCVC4 results are not displayed in the GUIID0001688:
**This issue was created automatically from Mantis Issue 1688. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001688:
**This issue was created automatically from Mantis Issue 1688. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001688 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When using the CVC4 prover the verification results are not automatically displayed in the GUI.
### Additional Information :
The problem was observed with Frama-C Neon.
## Attachments
- ![frama-c-gui](/uploads/947420837a3939ef2f99b9141387b822/frama-c-gui.gif)
- [gui01.c](/uploads/fbec4c1ec851421b393af44be48d6dc6/gui01.c)https://git.frama-c.com/pub/frama-c/-/issues/701WP-Plugin crashes due to an internal error2021-02-22T13:09:24Zmantis-gitlab-migrationWP-Plugin crashes due to an internal errorID0001922:
**This issue was created automatically from Mantis Issue 1922. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001922:
**This issue was created automatically from Mantis Issue 1922. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001922 | Frama-C | Plug-in > wp | public | 2014-09-12 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | 14.04 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When the attached file is called with the command line, that reads as follows:
frama-c.byte -pp-annot -no-unicode -wp -wp-no-bits -wp-rte -wp-script 'wp0.script' -wp-model Typed+ref -wp-out foo.wp foo.c
Frama-C produces the following output:
[kernel] preprocessing with "gcc -C -E -I. -dD foo.c"
Adhesion_Factor.c:1:0: warning: "__STDC__" redefined [enabled by default]
/* =============================================================================
^
foo.c:1:0: note: this is the location of the previous definition
# 1 "Adhesion_Factor.c"
^
Adhesion_Factor.c:1:0: warning: "__STDC_HOSTED__" redefined [enabled by default]
/* =============================================================================
^
foo.c:1:0: note: this is the location of the previous definition
# 1 "Adhesion_Factor.c"
^
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function TrackToTrain_Packet_071
[rte] annotating function TrackToTrain_Packet_071_Encoder
[wp] Collecting variable usage
[wp] Computing [100 goals...]
[wp] failure: Non-assignable term (P_Telegram+(0 .. I_Cur_Dim-1))
[kernel] Current source was: Adhesion_Factor.c:59
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 "list.ml", line 55, characters 20-23
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/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
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 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
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
### Additional Information :
The attached foo.c is the preprocessed version of a file out of the openETCS project. All used predicates are already included in the file.
## Attachments
- [foo.c](/uploads/4ca8b0f3f57e9d34ae71f1281023f171/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/776WP ignores some goals when 'initialized' is used in hypotheses2021-02-22T13:11:28Zmantis-gitlab-migrationWP ignores some goals when 'initialized' is used in hypothesesID0001670:
**This issue was created automatically from Mantis Issue 1670. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001670:
**This issue was created automatically from Mantis Issue 1670. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001670 | Frama-C | Plug-in > wp | public | 2014-03-04 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The message:
[wp] warning: Allocable, Freeable, Valid_read, Fresh and Initialized not yet implemented
is perfectly clear, but I would have expected that annotations using these predicates would have been ignored. Instead of that, proof obligations of other annotations simply disappear.
### Steps To Reproduce :
Example:
/*@ requires r1: \initialized(Y+(0 .. 99));
assigns X[0..99];
ensures X[0] == Y[0];
*/
void cp( int *X, int *Y );
void f (int *A, int *B) {
cp(B, A);
/*@ assert a1: A[0] == B[0]; */
}
Without the 'requires' property, the assertion is proved:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_assert_a1 : Valid
[wp] Proved goals: 1 / 1
Qed: 1
With the 'requires' property, the assertion is not even scheduled as a goal:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0https://git.frama-c.com/pub/frama-c/-/issues/777compatibility between \null in ACSL and NULL in C in wp2021-02-22T13:11:29Zmantis-gitlab-migrationcompatibility between \null in ACSL and NULL in C in wpID0001647:
**This issue was created automatically from Mantis Issue 1647. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001647:
**This issue was created automatically from Mantis Issue 1647. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001647 | Frama-C | Plug-in > wp | public | 2014-02-17 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
I have tried to prove properties involving NULL pointers, and I had problem to write the ACSL part. Here is and example:
/*@
ensures e1: \result == \null;
ensures e2: \result == 0;
ensures e3: \result == (int *) \null;
ensures e4: \result == (int *) 0;
ensures e5: \result == (int *)((void *)0);
*/
int * f (void) {
return NULL;
}
None of the properties are proved with the default memory model.
I finally manage to prove them with: -wp-model Typed+cast
Since NULL is used very often in programs, even with a clean typing, maybe something could be done for this special case ? Just a suggestion... ;-)https://git.frama-c.com/pub/frama-c/-/issues/779Make identifiers in Coq proofs more similar to those from C code2021-02-22T13:11:35ZJens GerlachMake identifiers in Coq proofs more similar to those from C codeID0001630:
**This issue was created automatically from Mantis Issue 1630. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001630:
**This issue was created automatically from Mantis Issue 1630. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001630 | Frama-C | Plug-in > wp | public | 2014-01-23 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When I want to proof an obligation for function
foo(int* a, int n)
then the Coq representation of the obligation uses the identifiers "a_0" and "n_0".
In my opinion, the proofs would be easier to read if WP would generate the names "a"
and "n".
(I often use "remember a_0 as a" to achieve this, but it would be nicer if I did not have to do it manually.)https://git.frama-c.com/pub/frama-c/-/issues/792Crash when using wpo api get_result2021-02-22T13:11:58Zmantis-gitlab-migrationCrash when using wpo api get_resultID0001779:
**This issue was created automatically from Mantis Issue 1779. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001779:
**This issue was created automatically from Mantis Issue 1779. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001779 | Frama-C | Plug-in > wp | public | 2014-05-19 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jpinheiro | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301 | **OS** | mac-osx | **OS Version** | maveriks |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When using wp and wpo api, if i invoke wpo api get_result it crashes and tells me to report it.
Example code:
let () = Dynamic.load_module "Wp"
module Wpo = Type.Abstract(struct let name = "Wpo.po" end)
let get_result = Dynamic.get ~plugin:"Wp" "Wpo.get_result" (Datatype.func Wpo.ty (Datatype.func Wpo.ty Wpo.ty))
### Additional Information :
[kernel] failure: unexpected exception "Type.Make_tbl(Key)(Info).Incompatible_type(\"Wp.Wpo.get_result has type Wpo.po -> Wpo.prover -> Wpo.result but is used with type Wpo.po -> Wpo.po -> Wpo.po.\")"
[kernel] Current source was: :0
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 "list.ml", line 73, characters 12-15
Called from file "src/kernel/dynamic.ml", line 322, characters 4-154
Called from file "src/kernel/dynamic.ml", line 355, characters 6-57
Called from file "src/kernel/dynamic.ml", line 391, characters 6-22
Called from file "src/lib/FCSet.ml", line 327, characters 38-41
Called from file "queue.ml", line 134, characters 6-20
Called from file "list.ml", line 73, characters 12-15
Called from file "src/kernel/cmdline.ml", line 292, characters 10-56
Called from file "src/kernel/cmdline.ml", line 319, characters 8-51
Called from file "src/kernel/cmdline.ml", line 328, characters 49-69
Called from file "src/kernel/cmdline.ml", line 566, characters 6-137
Called from file "src/kernel/cmdline.ml", line 749, characters 4-33
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
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 :
frama-c -load-script wp_script.ml condi.chttps://git.frama-c.com/pub/frama-c/-/issues/826frama-clang and WP: unverified precondition of member function2021-02-22T13:12:49ZJens Gerlachframa-clang and WP: unverified precondition of member functionID0001785:
**This issue was created automatically from Mantis Issue 1785. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001785:
**This issue was created automatically from Mantis Issue 1785. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001785 | Frama-Clang | Plug-in > wp | public | 2014-05-25 | 2015-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached example, there is one unverified precondition.
[wp] Proved goals: 38 / 39
Qed: 60 (0ms-1ms)
Alt-Ergo: 18 (15ms-81ms) (58) (unknown: 1)
Coq: 0 (unknown: 6)
cvc4: 9 (30ms-50ms) (interruped: 1)
If I understand it correctly, then drama-clang/wp cannot establish that the object on which
the method "get" is called is properly constructed.
In my opinion everything is fine.
### Steps To Reproduce :
Go to acslplusplus/C++Examples/OperatorOverloading and call
"make basic_assignment1.wpgui"
## Attachments
- [a.cpp](/uploads/2c4b691a23a507efa093fea9afa8060b/a.cpp)https://git.frama-c.com/pub/frama-c/-/issues/1020syntax error for alt-ergo with memset spec2021-02-22T13:17:31Zmantis-gitlab-migrationsyntax error for alt-ergo with memset specID0001587:
**This issue was created automatically from Mantis Issue 1587. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001587:
**This issue was created automatically from Mantis Issue 1587. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001587 | Frama-C | Plug-in > wp | public | 2013-12-16 | 2014-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
When trying to prove the first loop invariant of this example, there is a message:
/tmp/wpd57f12.dir/typed/A_MemSet.ergo:10:[wp] user error:
Prover Alt-Ergo returns Failed
characters 6-106:typing error: syntax error
and neither the establishment nor the preservation can be proved.
### Additional Information :
Command line is :
frama-c -cpp-extra-args=-I`frama-c -print-share-path`/libc pb_wp.c -wp
## Attachments
- [pb_wp.c](/uploads/97bd3bebc043ed6808b7047aec5dd9d0/pb_wp.c)https://git.frama-c.com/pub/frama-c/-/issues/1032WP - strcpy not proved2021-02-22T13:17:51Zmantis-gitlab-migrationWP - strcpy not provedID0001652:
**This issue was created automatically from Mantis Issue 1652. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001652:
**This issue was created automatically from Mantis Issue 1652. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001652 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | - | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I took the attached program from one of the WP tutorials but added the main function which calls strcpy. I wonder why the requires are not valid. I do not know what is wrong with my two strings in main.
### Steps To Reproduce :
[formal_verification]$ frama-c -pp-annot -wp -wp-rte -wp-proof why3:Z3,alt-ergo -wp-split -wp-model Typed+ref string_lib.c [kernel] preprocessing with "gcc -C -E -I. -dD string_lib.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] Collecting variable usage
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_ref_main_call_strcpy_pre_2_part1 : Valid [wp] [Qed] Goal typed_ref_main_call_strcpy_pre_2_part1 : Valid [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre : Unknown [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre_2_part2 : Unknown (Qed:4ms) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre_2_part2 : Unknown (Qed:4ms) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre : Unknown [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre_3 : Valid (24ms) (22) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre_3 : Valid (10ms)
## Attachments
- [string_lib.c](/uploads/83ca58d14714f50a83c5dbefcf99dec0/string_lib.c)https://git.frama-c.com/pub/frama-c/-/issues/624do ... while{ } loop and -wp-invariants option2021-02-22T13:23:13ZLionel Blatterdo ... while{ } loop and -wp-invariants optionID0002118:
**This issue was created automatically from Mantis Issue 2118. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002118:
**This issue was created automatically from Mantis Issue 2118. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002118 | Frama-C | Plug-in > wp | public | 2015-05-19 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | blatterl | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Fedora | **OS Version** | Version 17 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I use the WP plug-in on the do ... while{ } loop below with the -wp-invariants option, WP proves all goals.
But the ensures properties ("ensures n == 0 ==> \result == 0") of the function, including the do ... while{ } loop seems not valid to me.
I get the same result if I replace the post condition "\result == 0" by anything.
What is the exact semantics of the -wp-invariants option ?
/*@ ensures n == 0 ==> \result == 0; */
int fonction(int n, int a){
int i = 0;
int b = 0;
/*@ loop invariant b == i*a; */
do {
b = b+a;
i = i+1;
} while (i < n);
/*@ assert n== 0 ==> b==a; */
return b;
}
### Steps To Reproduce :
frama-c -wp -wp-invariants file.c
with file.c containing the above snippet.https://git.frama-c.com/pub/frama-c/-/issues/1231Errors in coq files generated by WP2021-02-22T13:24:10Zmantis-gitlab-migrationErrors in coq files generated by WPID0001603:
**This issue was created automatically from Mantis Issue 1603. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001603:
**This issue was created automatically from Mantis Issue 1603. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001603 | Frama-C | Plug-in > wp | public | 2014-01-16 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I noticed some errors in the coq files generated by WP:
- real_of_int not defined,
- is_float32 : R -> Prop but used as bool (is_float32 f_0%R))%R=true)
- let x_0 := ((Zeq_bool 1 t_0))%Z in ... x_0 used both as bool and as Prop
### Additional Information :
The example is the foo.c file posted on [Frama-c-discuss] by David Mentre yesterday evening (15/01/2014 - 18:30)https://git.frama-c.com/pub/frama-c/-/issues/1319Warning for Axiom: From wp: Overloaded operator User defined axiom2021-02-22T13:27:13ZPatrick BaudinWarning for Axiom: From wp: Overloaded operator User defined axiomID0000896:
**This issue was created automatically from Mantis Issue 896. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000896:
**This issue was created automatically from Mantis Issue 896. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000896 | Frama-C | Plug-in > wp | public | 2011-07-28 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Since there is no overloading is the source, the warning message has no sense!
### Additional Information :
> cat file.c
extern int tab[], x;
//@ axiomatic A { axiom ax: 10 < \block_length(tab); }
//@ assigns x;
extern void h(void);
//@ requires r2: x==0; assigns x;
void g() { h(); }
//@ requires r1: x==0;
void f(void) { g(); }
> frama-c -wp
...
file.c:8:[wp] warning: Warning for Axiom ax:
From wp: Overloaded operator User defined axiom ax{L} and User defined axiom ax
{L} not yet implemented
Effect: Ignored user-defined axiom 'ax'https://git.frama-c.com/pub/frama-c/-/issues/931assertion not proved anymore by WP2021-02-22T13:27:50Zmantis-gitlab-migrationassertion not proved anymore by WPID0001941:
**This issue was created automatically from Mantis Issue 1941. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001941:
**This issue was created automatically from Mantis Issue 1941. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001941 | Frama-C | Plug-in > wp | public | 2014-10-23 | 2014-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In a program similar to the enclosed example, the e1_wp property was proved by a previous version of WP, but is not proved anymore with Neon.
Adding the commented loop invariant doesn't help.
I tried to simplify as much as I can, but I don't understand what is going wrong in the proof obligation.
### Steps To Reproduce :
$ frama-c -wp-prop a1_val bts1940.c
## Attachments
- [bts1940.c](/uploads/d52e85090cbbe7ead916f090a0ad520d/bts1940.c)https://git.frama-c.com/pub/frama-c/-/issues/599invalid statement contract ("assigns") verified with CVC4 under strange circu...2021-02-22T13:29:19ZJochen Burghardtinvalid statement contract ("assigns") verified with CVC4 under strange circumstancesID0002110:
**This issue was created automatically from Mantis Issue 2110. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002110:
**This issue was created automatically from Mantis Issue 2110. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002110 | Frama-Clang | Plug-in > wp | public | 2015-04-30 | 2015-09-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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-prover cvc4 -wp 473.c" on the attached file (referred to as version "(0)" in the modification discussion below) results in verifying all proof obligations, including the statement contract in line 27, which is obviously false, since "myRead" also assigns "fd->pos" (line 13) and definitely changes it (line 15). I can't see a contradiction from which line 27 could be proven.
CVC4 still proves all obligations if one of the following changes is made:
(+1) myRead's "assigns" clauses in line 13 and 14 are joined into a single one, viz. "assigns fd->pos,*a;"
(+2) all "requires" clauses in line 10-12 and 20-22 are commented-in simultaneously
CVC4 fails to prove the statement contract in line 27 if one of the following changes is made:
(-1) myRead's "assigns" clauses in line 13 and 14 are swapped,
(-2) myRead's "assigns" clauses in line 13 and 14 are joined into a single "assigns *a,fd->pos;"
(-3) the "ensures" clauses in line 15 is deleted
(-4) the "ensures" clauses in line 23 (i.e. the whole contract) is deleted
(-5) the type of "a" is changed from "struct A*" to "int*" in line 17 and 25
From (+1) vs. (-2), as well as from (0) vs. (-1), it seems that the order of the memory location specifiers in myRead's "assigns" clause does matter.
In (0) vs. (-4), the "ensures" clause of "myMain" apparently influences its body code.
## Attachments
- [473.c](/uploads/11dc1d524233fc5202f6d678f181dca2/473.c)
- [wp-out.tar.gz](/uploads/ab1dd06676ca947a179dfe9d25490319/wp-out.tar.gz)
- [myMain_0b.why](/uploads/7dbe248cc0d0ba6fe57db28b2ffe6d19/myMain_0b.why)
- [myMain_0b1.smt2](/uploads/d3a0414d7a30295360902d885a8b6107/myMain_0b1.smt2)
- [myMain_0b2.smt2](/uploads/0835c74f12ab3e7a82f4a7d6ad984ac0/myMain_0b2.smt2)
- [myMain_0.smt2](/uploads/22b46ceffb1f126b776507e741a9134c/myMain_0.smt2)
- [myMain_-4.smt2](/uploads/7c12b3f5df33a42109d0215a16cc65c9/myMain_-4.smt2)
- [myMain_0.why](/uploads/e153c4b48d2e88354dae40eea92a4613/myMain_0.why)
- [myMain_-4.why](/uploads/45ab78b845a9d3f96afb1065a32e9184/myMain_-4.why)https://git.frama-c.com/pub/frama-c/-/issues/1181invalid loop invariant marked as valid (without pending hypothesis)2021-02-22T13:30:09ZVirgile Prevostoinvalid loop invariant marked as valid (without pending hypothesis)ID0001462:
**This issue was created automatically from Mantis Issue 1462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001462:
**This issue was created automatically from Mantis Issue 1462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001462 | Frama-C | Plug-in > wp | public | 2013-07-29 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **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 Neon-20140301 |
### Description :
Given the program below, wp discharges all proof obligations, including the first loop invariant whose preservation is false. This allows then to prove the invalid assertion after the loop. It seems that all three loop invariants (with their \at() term) are necessary to reproduce the issue.
### Additional Information :
-- file.c
void f(int c) {
int x = 0;
int y = 0;
/*@ assert for_value: c<= 0 || c == 1 || c>=2; */
if (c==2) { x=1; y=1; }
L:
/*@
loop invariant \at(x==0,L) ==> i!=0 ==> y == 0;
loop invariant \at(x==1,L) ==> i!=0 ==> x == 1;
loop invariant \at(c==0,Pre) ==> i==0 ==> x == 0;
loop assigns i,x,y;
*/
for (int i = 0; i<10; i++) {
if (c == 0) { x = 0; }
if (c == 1) { y = 1; }
if (c == 2) { x = 1; }
}
if (c==1) { /*@ assert consequence_of_false_invariant: y==0; */ }
}
### Steps To Reproduce :
frama-c -wp file.c
One can see the inconsistent status (green/black bullet) of the assert with
frama-c-gui -wp file.c -then -val -main f -slevel 100