frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:55:18Zhttps://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/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)https://git.frama-c.com/pub/frama-c/-/issues/126Prove of \false2021-04-15T06:50:23ZJens GerlachProve of \falseID0002427:
**This issue was created automatically from Mantis Issue 2427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002427:
**This issue was created automatically from Mantis Issue 2427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002427 | Frama-C | Plug-in > wp | public | 2019-02-16 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the attached program foo.c is analysed with the command line
frama-c -pp-annot -no-unicode -wp -wp-prover alt-ergo -wp-prover eprover foo.c
then the assertion "\false" is verified with "eprover" (2.2).
To me the axiomatics and the lemma look fine which would mean that it is a problem of "eprover".
However, I would like that an WP expert has a look at it before I contact the developer of "eprover".
Thanks in advance.
### Steps To Reproduce :
I am using Frama-C 18.0, Why3 0.88.3, alt-ergo 2.2.0, eprover 2.2.
## Attachments
- [foo.c](/uploads/96dbe2588b177df6328014404f4b189f/foo.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/125Shape of VC depends on selection of properties2021-09-21T13:53:03ZJens GerlachShape of VC depends on selection of propertiesID0002404:
**This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002404:
**This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002404 | Frama-C | Plug-in > wp | public | 2018-10-08 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP allows to select properties by using the option -wp-prop. I have noticed the following:
When selecting a property 'foo' by -wp-prop=foo, sometimes all VCs that belong to that property are verified.
However, when I wish to verify all properties, some VC's of the property 'foo' are not verified.
This might be caused by the fact that the the actual "shape" of a VC appears to depend on -wp-prop.
(I attach an example of the slight differences between a VC that belongs to a certain property "foo" depending on whether -wp-prop=foo is used or not.)
This of course defeats somehow the purpose of using -wp-prop and it would be a welcome feature
if the generation of a VC of a property 'foo' is not affected by "-wp-prop=foo".
### Additional Information :
Is this maybe a problem of Qed?
Also, if there are several ways to generate/simplify a VC, it would be nice if one chooses one that has a higher likelihood to be verified.
## Attachments
- [diff.txt](/uploads/14ff154d537bcec5e27f7f5946ba2bfd/diff.txt)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/124incomplete loading of saved state when using WP?2021-02-22T14:00:16ZJens Gerlachincomplete loading of saved state when using WP?ID0002290:
**This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002290:
**This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002290 | Frama-C | Plug-in > wp | public | 2017-03-09 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux/macOS | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I run the line
frama-c -save swap.sav -wp -wp-rte swap.c
on the attached line and then load the saved sate with
frama-c-gui -load swap.sav
I observe the following:
1.) a message in the Frama-C-GUI:"1 state in saved file ingnored. It is invalid in this Frama-C configuration."
2.) the GUI shows which proof obligations have been verified but the tab "WP Goals" does not show any information about which prover was successful
### Additional Information :
I am not sure whether this a problem of the kernel or of the WP plug-in.
## Attachments
- [swap.c](/uploads/68eb8d47535f4c84d136f65f15dec59a/swap.c)https://git.frama-c.com/pub/frama-c/-/issues/122malloc breaks reasoning about assigns2021-02-22T13:34:49Zmantis-gitlab-migrationmalloc breaks reasoning about assignsID0002455:
**This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002455:
**This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002455 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
If a function contains a call to malloc, WP fails to verify its assigns clause.
This could be because malloc does assign to variables in order to track allocation state, but if so there should be a way of specifying that the function assigns to only the listed variables, as well as whatever malloc assigns to. Even duplicating the annotation on malloc will not verify, which includes assigns clauses for the malloc state variables.
### Steps To Reproduce :
# Verify a function with a call to malloc and assigns \nothing
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c -wp-fct f
# Verify a function with the same contract as malloc, which only calls malloc
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c wp-fct malloc_wrapper
## Attachments
- [example.c](/uploads/419009a078988ed9875d2ded26c9f430/example.c)https://git.frama-c.com/pub/frama-c/-/issues/121floating-point support is somwhat incomplete2021-02-22T12:56:27Zmantis-gitlab-migrationfloating-point support is somwhat incompleteID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002459 | Frama-C | Plug-in > wp | public | 2019-07-02 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | florian | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | any | **OS** | any | **OS Version** | any |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi!
Maybe I am doing something fundamentally wrong, but I've tried some simple programs and I don't get anywhere. For example:
/*@ requires x >= 0.0f && x <= 100.0f;
*/
void float_fun(float x)
{
float y = x + 1.0f;
//@ assert y >= 1.0f;
}
I've had a look in share/frama-c/wp/why3/Cfloat.why and I'm not surprised nothing works, the axiomatisation is very incomplete, compared to the current stuff in why3. Could you please port to https://gitlab.inria.fr/why3/why3/blob/master/stdlib/ieee_float.mlw and then use a SMT solver by default that supports it natively (i.e. CVC4 or Z3)?
I know this is a bit of a drastic change, but as it stands WP is not overly useful for anyone trying to do anything with floats (e.g. control systems)...https://git.frama-c.com/pub/frama-c/-/issues/118Mk_addr not defined in Memory.v (coqwp via why3ide)2021-02-22T12:54:05Zmantis-gitlab-migrationMk_addr not defined in Memory.v (coqwp via why3ide)ID0002414:
**This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002414:
**This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002414 | Frama-C | Plug-in > wp | public | 2018-12-07 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | visq | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Memory.Mk_addr is needed for Coq proofs but not in Memory.v (it *is* present in Memory.why).
As a consequence, Coq fails to compile the generated proof scripts for a null pointer check:
> Error: The reference Memory.Mk_addr was not found in the current environment.
### Additional Information :
Frama-c Argon 18.0
Coq 8.6
why3 0.88.3
### Steps To Reproduce :
cat <<EOF >id.c
/*@ requires \valid(p);
ensures *p == \old(*p);
*/
void id(int* p)
{
int tmp;
if (p == (int*)0) return;
tmp = *p;
*p = ~~tmp;
}
EOF
frama-c -wp -wp-rte -wp-split -wp-prover why3ide id.c
# Select Postcondition Line 2
# Coq
# Edit
# Replay
# => Error: The reference Memory.Mk_addr was not found in the current environment.https://git.frama-c.com/pub/frama-c/-/issues/117contracts about memory mapped I/O through volatile memory locations2021-02-22T12:54:04Zmantis-gitlab-migrationcontracts about memory mapped I/O through volatile memory locationsID0002407:
**This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002407:
**This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002407 | Frama-C | Plug-in > wp | public | 2018-10-31 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
We've attached a small example in which a state machine communicates a peripheral through a volatile variable , on line 6 of constants.h:
volatile uint32_t rxBuffer;
The state of the machine is held by a struct mac, declared on line 21 of mac.h:
struct mac {
mac_packet_t mac_packet;
MessageType latestMessage;
mac_bridge_t MAC_BRIDGE_A;
}
the mac_bridge_t represents the machine's memory mapped I/O interface, as declared on line 15 of mac_bridge.h:
struct mac_bridge
{
volatile uint32_t *cmd_rx_buffer;
}
on line 13 of main.c,
mac_t mac = the_mac();
mac becomes a pointer to singleton_mac instance of struct mac declared on line 8 of mac.c and returned by the function the_mac() defined on line 17 of mac.c. On line 14 of main.c,
mac->MAC_BRIDGE_A = theMacBridge();
mac's IO interface MAC_BRIDGE_A becomes the singletonMacBridgeA instance of struct mac_bridge returned by the function theMacBridge() defined on line 11 of mac.c
mac_bridge_t theMacBridge() {
singletonMacBridgeA.cmd_rx_buffer = &rxBuffer;
return &singletonMacBridgeA;
}
thus, mac has as MAC_BRIDGE_A singletonMacBridgeA whose cmd_rx_buffer is a reference to the volatile rxBuffer. The volatile rxBuffer reads and writes from ghost state as given on line 7 of constants.h:
//@ ghost uint32_t injectorAPBBuffer[4294967296];
//@ ghost uint32_t injectorAPBBufferCount=0;
/*@ ghost //@ requires buffer == &(rxBuffer);
@ uint32_t readsBuffer(volatile uint32_t *buffer) {
@ static uint32_t injectorAPBBufferCount = 0;
@ for (int i=0; i<4294967296; i++) {
@ injectorAPBBuffer[i%4294967296]=i%42949967296;
@ }
@ if (buffer == &(rxBuffer)) {
@ return injectorAPBBuffer[injectorAPBBufferCount++];
@ }
@ else
@ return 0;
@ }
@ */
//@ ghost uint32_t bufferAPBCollector[4294967296];
//@ ghost uint32_t bufferAPBCollectorCount = 0;
/*@ ghost //@ requires buffer == &(rxBuffer);
@ uint32_t writesBuffer(volatile uint32_t *buffer, uint32_t v) {
@ if (buffer == &(rxBuffer)){
@ return bufferAPBCollector[(bufferAPBCollectorCount++)%64] = v;
@ }
@ else {
@ return 0;
@ }
@ }
@*/
//@ volatile (rxBuffer) reads readsBuffer writes writesBuffer;
mac implements a transition system driven by an alphabet of labels obtained through calls to macbridge_get_packet, defined on line 3 of mac_bridge.c
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge)
{
mac_packet_t received_packet={0};
received_packet.object_high=(uint8_t)(*(mac_bridge->cmd_rx_buffer));
return(received_packet);
}
when the given macbridge_t is the reference to the singletonMacBridgeA, we want this function to have as postcondition that the packet this function returns has the value found in the appropriate ghost state
/*@
behavior A:
assumes mac_bridge == &singletonMacBridgeA;
ensures \result.object_high == (uint8_t)injectorAPBBuffer[(injectorAPBBufferCount-1)%4294967296];
*/
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge);
The resulting Alt-ergo doesn't seem to capture the post-condition.
(* ---------------------------------------------------------- *)
(* --- Post-condition (file mac_bridge.h, line 24) in 'macbridge_get_packet' --- *)
(* ---------------------------------------------------------- *)
goal macbridge_get_packet_post:
forall t : int farray.
forall t_1 : (addr,int) farray.
forall t_2 : (addr,addr) farray.
forall a : addr.
let a_1 = shiftfield_F7_mac_bridge_cmd_rx_buffer(a) : addr in
let a_2 = t_2[a_1] : addr in
let x = t_1[a_2] : int in
(region(a.base) <= 0) ->
framed(t_2) ->
linked(t) ->
valid_rd(t, a_1, 1) ->
is_uint32(x) ->
valid_rd(t, a_2, 1) ->
(x = to_uint8(x))
## Attachments
- [framaExample.tar.gz](/uploads/ab7c400254275ad87e4710a1a81cafe6/framaExample.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/116crash2021-02-22T12:54:02Zmantis-gitlab-migrationcrashID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002409 | Frama-C | Plug-in > wp | public | 2018-11-13 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.gimbert | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | macosx | **OS** | mojave | **OS Version** | 10.14.1 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp somme.c
with somme.c containing
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
leads to crash
Trace below
### Additional Information :
[kernel] Parsing somme.c (with preprocessing)
[wp] Failure: Unbound logic variable 'f'
[kernel] Current source was: somme.c:4
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 531, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 998, characters 12-50
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 524, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 527, characters 9-16
Called from file "src/plugins/wp/LogicSemantics.ml", line 205, characters 18-38
Called from file "src/plugins/wp/LogicSemantics.ml", line 238, characters 16-32
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "list.ml", line 88, characters 20-23
Called from file "list.ml", line 88, characters 32-39
Called from file "list.ml", line 88, characters 32-39
Called from file "src/plugins/wp/LogicSemantics.ml", line 594, characters 23-52
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "src/plugins/wp/LogicSemantics.ml", line 361, characters 16-35
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 434, characters 28-51
Called from file "src/plugins/wp/LogicSemantics.ml", line 735, characters 39-62
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml", line 399, characters 21-32
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/LogicCompiler.ml", line 485, characters 6-60
Called from file "src/plugins/wp/LogicCompiler.ml", line 741, characters 6-104
Called from file "src/plugins/wp/LogicCompiler.ml", line 758, characters 24-46
Called from file "src/plugins/wp/cfgWP.ml", line 1351, characters 31-42
Called from file "map.ml", line 295, characters 20-25
Called from file "src/plugins/wp/cfgWP.ml", line 1435, characters 19-59
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml" (inlined), line 73, characters 21-47
Called from file "src/plugins/wp/Model.ml" (inlined), line 127, characters 21-45
Called from file "src/plugins/wp/Model.ml" (inlined), line 129, characters 18-36
Called from file "src/plugins/wp/cfgWP.ml", line 1433, characters 14-202
Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 19-28
Called from file "src/plugins/wp/Model.ml" (inlined), line 126, characters 19-36
Called from file "src/plugins/wp/cfgWP.ml", line 1431, characters 10-1023
Called from file "src/plugins/wp/register.ml", line 689, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 301, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 301, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
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 791, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Chlorine-20180502.
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
hugo-9:TP3 gimbert$ cat somme.c
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
## Attachments
- [somme.c](/uploads/5ef73e24f859da4da063d6d4e135ea99/somme.c)https://git.frama-c.com/pub/frama-c/-/issues/115dubious discharge of postcondition2021-02-22T14:00:51ZJens Gerlachdubious discharge of postconditionID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002390 | Frama-C | Plug-in > wp | public | 2018-07-24 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following function
/*@
assigns \nothing;
ensures a == 0;
*/
void foo(int a)
{
a = 0;
}
The postcondition can of course not be verified because the assignment happens to a copy "a" and furthermore nothing is known about the value of "a" in the pre-state.
If I add, however, the admittedly weird looking precondition "requires \valid(&a);" as shown here
/*@
requires \valid(&a);
assigns \nothing;
ensures a == 0;
*/
void bar(int a)
{
a = 0;
}
then Qed discharges the postcondition.
I am not sure this a bug or rather caused by taking the address of a formal argument in the precondition
but in any case it would be nice if someone could have a look at it.
### Steps To Reproduce :
Call
frama-c -wp -wp-rte foo.c
on the attached file.
## Attachments
- [foo.c](/uploads/59eb64f1e1b8ca2563cbfa0bcbb63a83/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/114Newer releases of FramaC produce apparent WP plug-in bug2021-02-22T14:01:18Zmantis-gitlab-migrationNewer releases of FramaC produce apparent WP plug-in bugID0002401:
**This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002401:
**This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002401 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The code in the attached example models a reactive program which interacts with peripherals via memory mapped I/O through an address defined by a constant. While an older version of frama-C (Phosphorus) successfully produced Altergo axiomatizations of boolean logic functions like the "logic boolean isAMessage(mac_t mac)" defined in mac.h,
"
logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_packet.object_low == 0x0A) && (mac->\
mac_packet.payload_length == 0x00));
"
the newer versions produce as AltErgo axiomatization (see out/typed/Axiomatic11.ergo in the attached)
"
function L_isAMessage
() :
bool =
andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))
"
Note that the argument to the boolean logic function is absent and the mac_t fields referenced in the ACSL definition of the logic function have. become "#{w_i}" - this malformed AltErgo (# is illegal in AltErgo) seems to originates from WP's QED module's pretty printer, whose find_var_env function returns these malformed names when it fails to find a given name in its environment.
### Steps To Reproduce :
tar -xvf framaBug.tar.gz
make wp
## Attachments
- [framaBug.tar.gz](/uploads/f07e549fb7296718c7ae0d86fb99b96e/framaBug.tar.gz)
- [frmaBug.tar.gz](/uploads/a43835306fcfcff1aef5bd28e09e0b4d/frmaBug.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/113Auto-generated assigns clause for a void* argument crashes wp2021-02-22T13:34:40Zmantis-gitlab-migrationAuto-generated assigns clause for a void* argument crashes wpID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002385 | Frama-C | Plug-in > wp | public | 2018-07-05 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | schollet | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using an unspecified function with an void* argument from an external file, the default generated assigns clause for that argument crashes frama-c and WP miss-attributes the error to the user.
Specifically, for an unspecified function foo(void* p), the auto generated assigns clause states that the function assigns *((char *)p+(0 .. )), which is then picked up by WP as an invalid user input.
Version : Frama-C 17 Chlorine
### Additional Information :
The command run :
frama-c -wp test2.c
Error log :
[kernel] Parsing test2.c (with preprocessing)
[kernel:annot:missing-spec] test2.c:7: Warning:
Neither code nor specification for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] test2.c:11: User Error: Invalid infinite range i_0+(0..)
[kernel] Plug-in wp aborted: invalid user input.
The auto-generated assigns clause (found with frama-c-gui):
/*@ assigns *((char *)thing + (0 ..));
assigns *((char *)thing + (0 ..)) \from *((char *)thing + (0 ..));
*/
Removing the assigns clause for create stops WP from crashing
### Steps To Reproduce :
run `frama-c -wp test2.c` with those 3 provided files
OR:
Write a function and its specification with at least an assigns clause.
Write in it a call to another function.
Write in another file that 2nd function which takes as an argument an void*.
Write the header and include it in the first file.
For the header and the 2nd file, do not write any specification for the function.
run frama-c -wp on the first file
## Attachments
- [assigns.tar.gz](/uploads/7d8c7280dce8dde42f8cce1f86cbef35/assigns.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/112alt-ergo goals generated directly / via why3 differ in provability2021-02-22T12:53:52ZJochen Burghardtalt-ergo goals generated directly / via why3 differ in provabilityID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002353 | Frama-C | Plug-in > wp | public | 2018-02-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
I generated an Alt-Ergo proof obligation for the ensures clause "xxx" (line 1140) of the attached program "search_n_standalone.c" (which was obtained from "search_n" in "Acsl by example" by "gcc -E -C"). When I did this directly (see attached script "fd"), it was proven without problems. However, when I did this via Why3 (see script "fw"), Alt-Ergo responded "Don't know" after 0.1 seconds.
In order to compare both mlw files given to Alt-Ergo, I moved the goal of the via-Why3 file into the direct file; it became provable there. Removing as many axioms and definitions as possible while keeping the (non-)provability, I obtained the files "xxx_direct.mlw" and "xxx_via_why3.mlw". It seems that the former defines and uses "shift_sint32", while the latter does not (it uses "shift" instead). Probably, this is the reason for the different outcomes of Alt-Ergo.
Although the observed issue may not be bug (both mlw files may be semanically equivalent), it might be desirable to unify the proof obligations given to Alt-Ergo on different pathways.
## Attachments
- [search_n_standalone.c](/uploads/79defa5986c7ebb10060cb2d8013dd27/search_n_standalone.c)
- [fd](/uploads/2325b1feb2a0e2c6bc2768f1552ecbf9/fd)
- [fw](/uploads/ade985efb5f8ea0601fa91f90ec1f340/fw)
- [xxx_direct.mlw](/uploads/49efc095c1124c4e87c110c2b7a10bb7/xxx_direct.mlw)
- [xxx_via_why3.mlw](/uploads/28204d54407af26ed64d8841005b5cef/xxx_via_why3.mlw)https://git.frama-c.com/pub/frama-c/-/issues/111Coq translation of predicate name changes when additional files are processed...2021-02-22T14:00:22ZJochen BurghardtCoq translation of predicate name changes when additional files are processed by Frama-CID0002340:
**This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002340:
**This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002340 | Frama-C | Plug-in > wp | public | 2018-01-04 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | Ubuntu | **OS Version** | Ubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prover coq -wp-prop LowerBoundShift equal_range2_cpp.c" succeeds in proving the lemma in line 16 of "equal_range2_cpp.c", using the Coq proof in file "wp0.script".
However, when "lower_bound_cpp.c" is appended as another command line argument to the same call, the lemma is no longer proven.
Using "wp-out" arguments and running a "diff -r" on the resulting directories reveals that the ACSL predicate name "LowerBound" is translated as "P_LowerBound_1_" for the first (succeeding) run, but as "P_LowerBound_2_" for the second (failing) run.
Note that the definitions of the "LowerBound" predicates literally agree in both C files.
The problem disappears when the overloaded 3-argument version of predicate "LowerBound" is omitted in both C files, or when the contract (i.e. the only use of "LowerBound" in that file) is omitted in file "lower_bound_cpp.c".
## Attachments
- [equal_range2_cpp.c](/uploads/a7f339a24fa1ad2c67458331246b61a8/equal_range2_cpp.c)
- [lower_bound_cpp.c](/uploads/1b5c79b560a67c3ba096b9ce8462c3fc/lower_bound_cpp.c)
- [wp0.script](/uploads/a549eb877d73af8f17c7be0a3cad6d0c/wp0.script)https://git.frama-c.com/pub/frama-c/-/issues/109Crash on loop with global assigns and per-behavior assigns2021-02-22T13:47:26ZBoris YakobowskiCrash on loop with global assigns and per-behavior assignsID0002180:
**This issue was created automatically from Mantis Issue 2180. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002180:
**This issue was created automatically from Mantis Issue 2180. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002180 | Frama-C | Plug-in > wp | public | 2015-10-19 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp crashes on the following program
/*@ behavior foo:
*/
void main(void)
{
int i;
int t[10];
i = 0;
/*@ loop assigns t[0 .. i];
for foo: loop assigns t[0 .. i]; */
while (i < 10) {
t[i] = 0;
i ++;
}
return;
}https://git.frama-c.com/pub/frama-c/-/issues/108suggest to supply previous "ensures" as hypotheses in proof obligation of nex...2021-02-22T12:53:43ZJochen Burghardtsuggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"ID0002336:
**This issue was created automatically from Mantis Issue 2336. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002336:
**This issue was created automatically from Mantis Issue 2336. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002336 | Frama-C | Plug-in > wp | public | 2017-12-08 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte foo.c -wp-out wp-out" on the attached file fails to prove clauses "E1" (as expected) and "E2". The latter is provable from "E1" by axiom "a2". A look at file "main_post_E2_Alt-Ergo.mlw" reveals that "E1" isn't given as hypothesis, and hence axiom "a2" can't be applied.
I cannot judge whether there is good reason for this behavior of Frama-C/Wp. If there isn't, I suggest that "E1" should be given as hypothesis to the proof obligation for "E2", similar to Frama-C/Wp's behavior on consecutive "assigns" clauses. The same applies to statement contracts.
## Attachments
- [foo.c](/uploads/5ad3994f41ed8b1f3aec521fbbf78ded/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/107Information on C type of array is not present (in Coq)2021-02-22T13:48:11ZJens GerlachInformation on C type of array is not present (in Coq)ID0002332:
**This issue was created automatically from Mantis Issue 2332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002332:
**This issue was created automatically from Mantis Issue 2332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002332 | Frama-C | Plug-in > wp | public | 2017-11-22 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux, macOS | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file 'array.c' there are two simple predicates 'AllEqual' and 'Constant' that involve int arrays.
There are also two lemmas that relate both predicate.
While it can automatically verified that "Constant" implies "AllEqual" the proof of the "converse" statement fails. When looking at the Coq presentation of "AllEqual" it becomes apparent that Coq only sees an "integer array"; the specific C type (represented by the predicate 'is_sint32') is NOT present at all.
### Additional Information :
The error also occurs in the beta release of Frama-C 16 (Sulfur).
### Steps To Reproduce :
Run the command:
frama-c-gui -no-unicode -wp -wp-prover alt-ergo -wp-prover coq -wp-script 'wp0.script' array.c
## Attachments
- [array.c](/uploads/9ffd5dc713b956ec02a3457ddc3b71c6/array.c)
- [wp0.script](/uploads/eb44100130d8efee641d5565ee82857b/wp0.script)https://git.frama-c.com/pub/frama-c/-/issues/106suggest unique term normalization for lemmas and goals2021-02-22T12:53:39ZJochen Burghardtsuggest unique term normalization for lemmas and goalsID0002329:
**This issue was created automatically from Mantis Issue 2329. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002329:
**This issue was created automatically from Mantis Issue 2329. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002329 | Frama-C | Plug-in > wp | public | 2017-10-09 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501 | **OS** | - | **OS Version** | xubuntu 17.04 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prop g aaa.c" on the attached file fails to prove the assertion "g", although it obviously follows from "f" by applying lemma "lem". One reason for that is of course the inherent incompleteness of SMT provers like Alt-Ergo and Cvc4. However, another reason is that Frama-C's term normalization(1) swaps some arguments of "+", and
(2) performs swaps in the lemma that differ from those performed in the goal.
As a result, in the attached mlw file,
"(L_Foo(a,b+c)=true) -> (L_Bar(a,c+d)=true)"
appears in the lemma, while "(L_Foo(a,i_1+i_2)=true) -> (L_Bar(a,i+i_1)=true)" appears in the goal. The latter is equivalent to
"(L_Foo(a,c+b)=true) -> (L_Bar(a,d+c)=true)"
when expressed in a notation closer to the source-code. Variable "c" is common to L_Foo and L_Bar; note its different positions in the lemma vs. in the goal.
If the goal is changed to "(L_Foo(a,i_2+i_1)=true) -> (L_Bar(a,i_1+i)=true)", it syntactically matches the lemma, and Alt-Ergo proves it in a few milliseconds.
Unless there are good reasons to swap the arguments of "+", they should be kept in their source-code order; this way, the user has a chance to control what is given to the provers.
However, if there *are* good reasons to include argument swapping in term normalization, it should be performed in the same way both in lemmas and in goals.
A possible explanation for the above behavior of Frama-C is that, for some
reason, source-code variable names are transformed to unrelated internal names
in goals, but not in lemmas, and that term normalization just orders arguments
of commutative functions lexicographically (cf. issue #2100).
## Attachments
- [aaa.c](/uploads/86f4cf4ef5586dff6d49e1d6d35ff66e/aaa.c)
- [main_assert_g_Alt-Ergo.mlw](/uploads/4875bf8644ee1246e06bb880e675a7ad/main_assert_g_Alt-Ergo.mlw)https://git.frama-c.com/pub/frama-c/-/issues/105suggest boolean expressions for "-wp-prop" arguments2021-02-22T12:53:37ZJochen Burghardtsuggest boolean expressions for "-wp-prop" argumentsID0002285:
**This issue was created automatically from Mantis Issue 2285. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002285:
**This issue was created automatically from Mantis Issue 2285. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002285 | Frama-C | Plug-in > wp | public | 2017-02-27 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | low | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the semantics of "-wp-prop" arguments is unexplained and difficult to understand, when negation and more than one label is used.
For example, using the attached file, "-wp=prop=A,B,-C" selects l4,l5,l6, whereas "-wp-prop=-C,B,A" selects all but l3, and so does "-wp-prop=A,B,c" (although the set of "C"-labelled lemmas is the complement of that of the "c"-labelled lemmas).
I think, parsing arbitrary boolean expressions (built from "!", "&&", "||") isn't more difficult that the current mechanism, but is easier to describe in the manual and to understand.
Alternatively, "-" could be kept as negation, "," could be used for cunjunction only, and the results of multiple args "-wp-prop=X -wp-prop=Y" could be or-ed together; this would at least allow to express arbitrary sets in disjunctive normal form.
### Additional Information :
Complex set expressions arise when labels are used during proof development to attach prover names (and even options) to properties. Using calls like "frama-c -wp -wp-prop=PROVE_WITH_CVC4 -wp-prover=cvc4 ..." can save a lot of proving time that is normally wasted by unsuccessful attempts by unsuitable provers. Other labels that can save time are "TODO", "NEEDS_LONG_TIMEOUT", etc. This way, boolean expressions arise in a natural way; and the user needs to be sure about their semantics, in order not to overlook proof obligations due to splitting by prover.
## Attachments
- [proptest.c](/uploads/969a6dcaeb4f45e418845f21976d9cb7/proptest.c)
- [bbb.c](/uploads/5672cfb09ff165d83ff4c8efc35aacbd/bbb.c)