frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-11-27T15:03:11Zhttps://git.frama-c.com/pub/frama-c/-/issues/2680[WP] Using Z3 when predicate with access to struct defined leads to inconsist...2023-11-27T15:03:11ZReMarxist[WP] Using Z3 when predicate with access to struct defined leads to inconsistency### Steps to reproduce the issue
Launch the following example with this command (note big timeout):
```bash
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
```
Example:
```c
struct S
{
int n;
};
/*@ axiomatic Block {
pr...### Steps to reproduce the issue
Launch the following example with this command (note big timeout):
```bash
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
```
Example:
```c
struct S
{
int n;
};
/*@ axiomatic Block {
predicate isZero(int left) =
left == 0;
// Unused, but necessary for verification
logic int getN(struct S *s) = s->n;
}*/
/*@ requires \valid(s);
requires isZero(s->n);
assigns \nothing;
ensures \false; // Verified by Z3
*/
void g(struct S *s)
{
}
/*@ assigns \nothing;
ensures \false; // Verified by Z3
*/
void f()
{
struct S s;
s.n = 0;
g(&s);
}
```
As you can see, specifications establish that f() and g() ensure obviously false statement. The problem is in verification of g(), I've defined f() to show that preconditions of g() can be satisfied.
### Expected behaviour
Attempt to prove `\false` in postcondition of `g()` should fail.
### Actual behaviour
Z3 proves `\false` in postcondition of `g()`:
```
[kernel] Parsing tmp/acsl/acsl.c (with preprocessing)
[rte:annot] annotating function f
[rte:annot] annotating function g
[wp] Running WP plugin...
[wp] 9 goals scheduled
[wp] Proved goals: 9 / 9
Qed: 7
Z3 4.12.2: 2
```
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.1 (Cobalt)
- Z3 version 4.12.2 - 64 bit
- Why3 platform version: 1.6.0
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
### Additional information
The problem may be in Z3 itself, because Alt-Ergo and CVC4 cannot prove these goals. I've also reproduced the problem using docker image from Docker Hub.
I've posted this report as a question on StackOverflow previously (https://stackoverflow.com/questions/77460683/why-wp-with-z3-proves-false-when-access-to-struct-field-is-defined) as I wasn't able to post an issue here.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2668[EVA] unsoundness when initializing in switch statement before first case2023-09-20T08:51:15ZJulien Lepiller[EVA] unsoundness when initializing in switch statement before first case<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
The following code is validated by EVA:
```c
#include <stdio.h>
int main(int argc, char *argv[]) {
switch(argc) {
int i = 5;
case 0:
i = 17;
// fall-through
default:
//@ assert i == 17;
printf("%d\n", i);
}
return 0;
}
```
The file is run through frama-c:
```bash
frama-c -eva test.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Eva should not validate the assert, since "i" is possibly uninitialized. This is because in C, code between the switch statement and the first case is not executed. Note that frama-c-gui correctly shows that code as dead code.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Eva validates the assert. No warnings are generated.
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *27.1 (Cobalt)*
- Plug-in used: *Eva*
- OS name: *Ubuntu*
- OS version: *22.04*
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
When using `-slevel 2` or above, Eva does not validate the assert, but still validates the generated `\initialized` assert for `printf`.
If `int i` is not initialized before the first case, Eva does not validate the assert. If a `break` is inserted, it does not validate the assert either.David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2666Alias plugin's `Abstract_state` API requires using private `Alias__Abstract_s...2023-11-06T08:47:52ZBasile ClémentAlias plugin's `Abstract_state` API requires using private `Alias__Abstract_state` moduleThe Alias plugin exposes [the `Abstract_state` module](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/abstract_state.mli) through [`API.mli`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.ml...The Alias plugin exposes [the `Abstract_state` module](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/abstract_state.mli) through [`API.mli`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.mli).
However, OCaml doesn't know that the modules `G` and `LSet` used in the `Abstract_state` module are the same as those exposed in the `API` module, even though [they are](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.ml#L26-28), because the `.mli` do not expose this information. To use `API.Abstract_state` in a meaningful way, the `G` and `LSet` modules must be accessed through the private `Alias__Abstract_state` module generated by `dune`.Jan RochelJan Rochelhttps://git.frama-c.com/pub/frama-c/-/issues/2637libgnomecanvas disabled in brew2023-06-21T08:15:31ZLaura Titololibgnomecanvas disabled in brewTrying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/for...Trying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/formula/libgnomecanvas. https://gitlab.gnome.org/Archive/libgnomecanvas).https://git.frama-c.com/pub/frama-c/-/issues/2601[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed ...2022-05-30T12:20:54ZCostava[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed index when array is function parameter<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
With Alt-Ergo 2.4.1 installed:
`frama-c -wp -wp-rte poc.c` / `frama-c-gui -wp -wp-rte poc.c`
using [poc.c](/uploads/62e84944634b546da975b2397c7c4e4d/poc.c) :
```c
/*@
requires \valid_read(arr + (0 .. 3));
assigns \nothing;
*/
int foo(const int arr[const static 4]) {
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
return 0;
}
/*@
assigns \nothing;
*/
int main(void) {
const int arr[4] = {0, 1, 2, 3};
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
foo(arr);
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals proved.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte poc.c
[kernel] Parsing poc.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 34 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_foo_assert_rte_mem_access_3 : Timeout (Qed:9ms) (10s)
[wp] Proved goals: 33 / 34
Qed: 23 (2ms-5ms-14ms)
Alt-Ergo 2.4.1: 10 (7ms-17ms-30ms) (556) (interrupted: 1)
```
33/34 goals proved.
The verification of `/*@ assert rte: mem_access: \valid_read(arr + j); */` for code `const int jvalue = arr[j];` in function `foo` is not successful.
From a naive perspective, the `arr[j]` accesses in main and foo are equivalent, so the assert in foo should be verifiable if the assert in main is.
(I am aware that a different assert is generated in main: `/*@ assert rte: index_bound: j < 4; */`)
Also, the `//@ assert 0 <= j < 4;` immediately before the access can be verified, both in main and foo, so it seems the rte assert should be able to be verified also.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP, RTE
- OS name: Manjaro Linux
- OS version: Qonos 21.2.4
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
The poc.c is a simplified proof of concept, but I did hit this situation when working on a real program.
To be explicit about the provers involved:
```sh
$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/user/.why3.conf
```
I was uncertain whether to submit this here or at the [alt-ergo issues](https://github.com/OCamlPro/alt-ergo/issues).
Apologies if this is the wrong place. Let me know if I should post there instead.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2593Build failure if only the eva plugin is selected: -rectypes is required2022-07-11T15:44:07Zfx-cartonBuild failure if only the eva plugin is selected: -rectypes is required### Steps to reproduce the issue
- untar the frama-c-24.0 sources
- configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
- make
### Expected behaviour
Compilation succeeds
#...### Steps to reproduce the issue
- untar the frama-c-24.0 sources
- configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
- make
### Expected behaviour
Compilation succeeds
### Actual behaviour
Compilation fails with the following message:
```
Ocamlc src/plugins/value/domains/multidim_domain.cmo
File "src/plugins/value/domains/multidim_domain.ml", line 1:
Error: Invalid import of Abstract_memory, which uses recursive types.
The compilation flag -rectypes is required
make: *** [share/Makefile.generic:78: src/plugins/value/domains/multidim_domain.cmo] Error 2
```
### Contextual information
- Frama-C installation mode: from source
- Frama-C version: 24.0
- Plug-in used: Eva (and dependencies)
- OS name: Linux
- OS version: Gentoo linux
### Additional information (optional)
- With no configure options, it builds fine.
- I've tried to debug the issue, and I think this is caused by having "-rectypes" added to BFLAGS for the rule compiling src/kernel_services/abstract_interp/abstract_memory.mli; which seems to be added as a side effect of the following line in the Makefile:
```
src/kernel_services/abstract_interp/abstract_memory.cmo: BFLAGS += -rectypes
```
For some reason, the dependency tree happens to change between the two configurations (default ./configure and ./configure with the aforementioned options), and in the latter case, the .cmi is a dependency of the .cmo, and thus inherits the local variables including BFLAGS.
- If I run `make src/kernel_services/abstract_interp/abstract_memory.cmi` and then `make`, it builds fine, because in the first make invocation the .cmo is not in the dependency tree, so -rectypes won't be added.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2580Non ghost lvalue when assigning array (frama-c 22)2022-10-05T06:41:34ZRaul MontiNon ghost lvalue when assigning array (frama-c 22)The following code aborts when using the e-acsl plug-in of frama-c 22.0, while it passes when using frama-c 20.0. I paste the failing case output bellow. The warning mentions lines `//@ ghost int acopy[len];` and `//@ ghost acopy[i] = a[...The following code aborts when using the e-acsl plug-in of frama-c 22.0, while it passes when using frama-c 20.0. I paste the failing case output bellow. The warning mentions lines `//@ ghost int acopy[len];` and `//@ ghost acopy[i] = a[i];`. I am wondering if this is actually not allowed or if it is just a bug?
Regards,
Raúl Monti.
```
#include <stdio.h>
/*@ requires len >= 0;
@ requires \valid(a+(0..len-1));
@*/
void add1(int* a, int len) {
//@ ghost int acopy[len];
int i;
for(i = 0; i < len; i++) {
//@ ghost acopy[i] = a[i];
}
for(i = 0; i < len; i++) {
a[i] = a[i] + 1;
}
//@ assert \forall integer i; 0 <= i < len ==> a[i] == acopy[i] + 1;
}
int main() {
int a[3];
a[0] = 0;
a[1] = 1;
a[2] = 2;
add1(a, 3);
return 0;
}
```
The output I get when running e-acsl-gcc.sh add.c -c -O add in frama-c-22:
```
e-acsl-gcc.sh add.c -c -O add
+ frama-c -remove-unused-specified-functions -machdep gcc_x86_64 -cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 -no-frama-c-stdlib add.c -e-acsl -e-acsl-share=.../.opam/default/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.c
[kernel] Parsing add.c (with preprocessing)
[kernel:ghost:bad-use] add.c:7: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] add.c:10: Warning:
'*(acopy + i)' is a non-ghost lvalue, it cannot be assigned in ghost code
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2548Error: Unbound value Why3.Whyconf.load_default_config_if_needed2021-04-13T17:49:41ZQixError: Unbound value Why3.Whyconf.load_default_config_if_needed
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [ ] the issue has not yet been reported on our old
[BTS](htt...
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [ ] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*); **(Can't tell; getting a database connection error)**
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md). **(Not exactly; I'm building from source within a Dockerfile)**
# Contextual information
- Frama-C installation mode: from source
- Frama-C version: c4d10fb975d443e3c40289843fae89c424b54e63
- Plug-in used: WP
- OS name: Debian Buster
- OS version: 20210326 (10.8)
# Steps to reproduce the issue
Dockerfile:
```Dockerfile
FROM debian:buster-20210326 AS base
RUN apt update -y
RUN apt install -y gnupg2 wget apt-transport-https ca-certificates
RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add -
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN cat /etc/apt/sources.list
RUN apt update -y
RUN apt install -y clang-12 lld-12 grub-common ninja-build git libssl-dev libgmp-dev pkg-config make m4 unzip tar bzip2 gcc g++ autoconf zlib1g-dev time
RUN cc --version
RUN c++ --version
WORKDIR /opam
RUN wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
RUN echo "/opam" | sh install.sh --no-backup
ENV PATH="/opam:/opam/bin:${PATH}"
RUN opam --version
RUN time opam init -y --disable-sandboxing --jobs=1
RUN time opam install -y depext ocamlfind ocamlgraph zarith yojson why3.1.4.0 alt-ergo.2.4.0
ENV PATH="/root/.opam/default/bin:${PATH}"
RUN why3 --version
RUN why3 config detect
ARG FRAMAC_REF=c4d10fb975d443e3c40289843fae89c424b54e63
WORKDIR /framac
RUN git init .
RUN git remote add origin https://git.frama-c.com/pub/frama-c.git
RUN git fetch origin ${FRAMAC_REF}
RUN git checkout ${FRAMAC_REF}
RUN autoconf
RUN ./configure
RUN make -j4
RUN make install
RUN frama-c --version; echo
```
# Expected behaviour
Should build to completion.
# Actual behaviour
```
File "src/plugins/wp/Why3Provers.ml", line 31, characters 19-61:
31 | let config = Why3.Whyconf.load_default_config_if_needed config in
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Whyconf.load_default_config_if_needed
make: *** [share/Makefile.generic:78: src/plugins/wp/Why3Provers.cmo] Error 2
make: *** Waiting for unfinished jobs....
The command '/bin/sh -c make -j4' returned a non-zero code: 2
```
---
Some context: Trying to verify a new toy OS and having a bunch of issues since I can't use the standard C library that ships with Frama-C (as there is no C library available in this environment) so I've ended up copying the axiomatic clauses from the `__fc_xxx.h` headers directly.
I saw on StackOverflow that a few bugs that seemed to be affecting me were recently patched on master but not yet released, so I spun up a Dockerfile in order to try to see if any of the verification could be fixed by trying it with the latest head.
However, it doesn't seem to be working - much less getting even simple programs to verify correctly :/ Hence why I'm trying to update everything to latest to see if I can't get _any_ verification to work.
Anyway this is the latest issue I've hit trying to get everything up to date.
Note that there is a lot of stuff in there that isn't directly related to this bug - this is a stripped down Dockerfile, and there is a bunch of extra stuff that comes after this step that I removed to keep things small.https://git.frama-c.com/pub/frama-c/-/issues/2494type error in generated why file2021-04-15T09:17:39ZFabrice Derepastype error in generated why fileID0000178:
**This issue was created automatically from Mantis Issue 178. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000178:
**This issue was created automatically from Mantis Issue 178. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000178 | Frama-C | Plug-in > jessie | public | 2009-07-09 | 2009-07-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | derepas | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Let us consider the following program 'simple.c':
void g(int * j, int *k) {
int tmp= *j;
*j=*k;
*k=tmp;
}
void f(int * vector, int size) {
int i=0;
if (i<size)
g (&vector[i],&vector[i+1]);
}
The command line 'frama-c -main f -jessie simple.c' generates the following error:
[kernel...] preprocessing with "gcc -C -E -I. -dD simple.c"
Starting Jessie translation
Producing Jessie files in subdir simple.jessie
File simple.jessie/simple.jc written.
File simple.jessie/simple.cloc written.
Calling Jessie tool in subdir simple.jessie
Generating Why function g
Generating Why function f
Calling VCs generator.
gwhy-bin [...] why/simple.why
Computation of VCs...
File "why/simple.why", line 552, characters 9-49:
Term i is expected to have type int
make: *** [simple.stat] Erreur 1
Jessie subprocess failed: make -f simple.makefile gui
The funny thing is that when the body of function g is empty this error does not occur (though the error seems to be in function f).Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2456Frama-C/Jessie: typing error2021-04-15T09:17:47ZVirgile PrevostoFrama-C/Jessie: typing errorID0000040:
**This issue was created automatically from Mantis Issue 40. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000040:
**This issue was created automatically from Mantis Issue 40. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000040 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7554 from old bts, reported by Dillon Pariente]
Hello,
The two following files can be compiled separately:
//===== FILE FOO.c
typedef struct {float k;} las;
void g (float * y);
void f (las *c) { g(&(c->k)); }
//===== FILE SPECS.h
typedef struct {float k;} las;
//@ requires \valid(c); assigns c->k;
void f (las * c);
but the command line below:
//===== COMMAND LINE
frama-c.byte.exe -jessie-analysis -jessie-gui FOO.c SPECS.h
generates the following error:
//===== STDOUT
Calling Jessie tool in subdir wholeprogram.jessie File "wholeprogram.jc", line 401, characters 15-26: typing
error: type float_P[..] expected instead of real
Jessie subprocess failed: jessie -why-opt -split-user-conj -v
-why-opt -fast-wp -separation -locs wholeprogram.cloc w
holeprogram.jcClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2445Frama-C/Jessie: memory set problem2021-04-15T09:17:47ZVirgile PrevostoFrama-C/Jessie: memory set problemID0000039:
**This issue was created automatically from Mantis Issue 39. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000039:
**This issue was created automatically from Mantis Issue 39. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000039 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-11-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7548 from old bts, reported by Dillon Pariente]
Hello,
(Issue already sent to discussion-list, and now registred into the BTS! Sorry for this "duplication".)
Launching:
frama-c.byte.exe -jessie-analysis -jessie-gen-goals foo.c
with foo.c containing:
//*****************************************
typedef struct {int i;int j;} las;
/*@ requires \valid(a) && \valid(b);
assigns *a, *b; */
void g (int *a,int *b){ *a=11; *b=15; }
/*@ requires \valid(p) ;
assigns p->i,p->j;
*/
void f (las *p)
{ g (&(p->i), &(p->j)); }
//*****************************************
returns the following error (Jessie/Why version is 2.18):
memory (mem-field(int_M),b_21)
in memory set (mem-field(int_M),a_20),
(mem-field(int_M),b_21)
File "jc/jc_interp_misc.ml", line 716, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 716, characters 7-13: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jcClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2357Jessie: struct field's validity2021-04-15T09:17:41ZDillon ParienteJessie: struct field's validityID0000102:
**This issue was created automatically from Mantis Issue 102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000102:
**This issue was created automatically from Mantis Issue 102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000102 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2010-07-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **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 :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
The following annotated code can not be proved by ATPs.
Function f() needs an invariant on global var v :
//@ global invariant aa: \valid(&v.c);
that should normally be generated automatically.
Function f2() needs a type invariant :
//@ type invariant Tt(las* l) = \valid(&(l->c)); but this type invariant is visibly not taken into account in the Why generated file (predicate Tt does exist but is not axiomatized).
Source code:
typedef struct { int c; } las;
las v;
//@ requires \valid(p);
void g(int * p);
void f(){ g(&v.c); }
//@ requires \valid(x);
void f2(las * x){ g(&(x->c)); }
Commande line:
frama-c -jessie-analysis -jessie-gui file.cClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2339assigns nothing ?2021-04-15T09:17:13Zmantis-gitlab-migrationassigns nothing ?ID0000617:
**This issue was created automatically from Mantis Issue 617. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000617:
**This issue was created automatically from Mantis Issue 617. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000617 | Frama-C | Plug-in > jessie | public | 2010-10-26 | 2010-11-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jnarboux | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Using the following example:
/*@
ensures \result == 1;
assigns \nothing;
*/
int foo()
{
int v[9];
v[0] =1;
return 1;
}
I get:
[kernel] preprocessing with "gcc -C -E -I. -dD bug.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir bug.jessie
[jessie] File bug.jessie/bug.jc written.
[jessie] File bug.jessie/bug.cloc written.
[jessie] Calling Jessie tool in subdir bug.jessie
Generating Why function foo
[jessie] Calling VCs generator.
gwhy-bin [...] why/bug.why
Computation of VCs...
File "why/bug.why", line 392, characters 20-42:
Unbound variable int_P_v_1_alloc_table
make: *** [bug.stat] Erreur 1
is it normal ? if I remove the assign nothing it works.
Julien NarbouxClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/1832journalization of -print option2022-07-12T07:07:41ZPatrick Baudinjournalization of -print optionID0001450:
**This issue was created automatically from Mantis Issue 1450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001450:
**This issue was created automatically from Mantis Issue 1450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001450 | Frama-C | Kernel | public | 2013-07-04 | 2013-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Loading a script file issued previously with -journal-enable option should perform the same job as previously done.
That is not the case with -print option:
Once the -print option is journalized, executing that journal performs two print!
> frama-c -print file.c -journal-enable
> frama-c -load-script frama_c_journal.ml
### Additional Information :
> cat file.c
//@ lemma l : 1 == 1;
> frama-c -print file.c -journal-enable
[kernel] preprocessing with "gcc -C -E -I. file.c"
/* Generated by Frama-C */
/*@ lemma l: 1 ? 1;
*/
[kernel] writing journal in file `frama_c_journal.ml'.
> frama-c -load-script frama_c_journal.ml
[kernel] preprocessing with "gcc -C -E -I. file.c"
/* Generated by Frama-C */
/*@ lemma l: 1 ? 1;
*/
/* Generated by Frama-C */
/*@ lemma l: 1 ? 1;
*/Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/893access to nested union/struct component causes crash2021-03-29T16:12:05ZJochen Burghardtaccess to nested union/struct component causes crashID0001803:
**This issue was created automatically from Mantis Issue 1803. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001803:
**This issue was created automatically from Mantis Issue 1803. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001803 | Frama-Clang | Kernel | public | 2014-06-06 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
If, in the resolved issue #1754, the outermost "struct" is changed to "union" (file "1_4_2us.cpp"), the crash re-appears:
Now output intermediate result
1_4_2us.cpp:2:[fclang] failure: No usable default constructor for _s::_w
[kernel] Current source was: 1_4_2us.cpp:2
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 "convert.ml", line 1367, characters 30-75
Called from file "convert.ml", line 1399, characters 17-43
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 1425, characters 23-65
Called from file "convert.ml", line 1802, characters 21-133
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 1876, characters 19-78
Called from file "convert.ml", line 2102, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 2106, characters 4-79
Called from file "frama_Clang_register.ml", line 82, characters 13-36
Called from file "src/kernel/file.ml", line 1058, characters 10-43
Called from file "src/kernel/file.ml", line 1102, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1099, characters 6-520
Called from file "src/kernel/file.ml", line 2144, characters 12-30
Called from file "src/kernel/file.ml", line 2229, characters 4-27
Called from file "src/kernel/ast.ml", line 113, characters 2-28
Called from file "src/kernel/ast.ml", line 125, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-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 fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
If instead, or additionally, the inner "struct" is changed to "union" (files "1_4_2su.cpp" and "1_4_2uu.cpp"), a strange warning is issued:
Now output intermediate result
1_4_2su.cpp:3:[kernel] warning: Calling undeclared function Frama_C_memcpy. Old style K&R code?
## Attachments
- [1_4_2us.cpp](/uploads/d21782d1d8724590e1a9f532c053ab0f/1_4_2us.cpp)
- [1_4_2su.cpp](/uploads/c40254eb1bf606da7ca5bb1fd976753e/1_4_2su.cpp)
- [1_4_2uu.cpp](/uploads/b8d0faf5f634dc32b476e057713a797c/1_4_2uu.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/891struct type inside 'extern "C"' causes crash, except as lhs of typedef2021-03-29T16:16:35ZJochen Burghardtstruct type inside 'extern "C"' causes crash, except as lhs of typedefID0001965:
**This issue was created automatically from Mantis Issue 1965. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001965:
**This issue was created automatically from Mantis Issue 1965. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001965 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
132.cpp:4:[fclang] failure: Unknown declaration in extern C structure definition
[kernel] Current source was: 132.cpp:4
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 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2032, characters 10-61
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
When activated, each of the lines 5 and 6 causes a similar crash. This problem prohibits use of <stdio.h>.
## Attachments
- [132.cpp](/uploads/c8d869273866f020befb12a0e330ae22/132.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/886throw/catch of struct causes crash2021-03-29T16:21:09ZJochen Burghardtthrow/catch of struct causes crashID0001957:
**This issue was created automatically from Mantis Issue 1957. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001957:
**This issue was created automatically from Mantis Issue 1957. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001957 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
[kernel] Current source was: 117.cpp:12
The full backtrace is:
Raised at file "hashtbl.ml", line 229, characters 23-32
Called from file "src/kernel/exn_flow.ml", line 492, characters 23-63
Called from file "src/kernel/exn_flow.ml", line 509, characters 55-77
Called from file "list.ml", line 57, characters 20-23
Called from file "src/kernel/exn_flow.ml", line 624, characters 20-60
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2045, characters 15-31
Called from file "cil/src/cil.ml", line 3094, characters 5-86
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 3254, characters 16-40
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3483, characters 14-39
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3445, characters 5-91
Called from file "cil/src/cil.ml", line 3537, characters 16-38
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 2129, characters 24-57
Called from file "cil/src/cil.ml", line 3531, characters 5-53
Called from file "cil/src/cil.ml", line 6193, characters 17-37
Called from file "cil/src/cil.ml", line 6200, characters 3-20
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 6217, characters 15-39
Called from file "src/kernel/exn_flow.ml", line 687, characters 4-62
Called from file "src/kernel/file.ml", line 1617, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1694, characters 2-36
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The active code is probably minimal causing the crash; the problem remains if any of the commented-out lines is activated.
## Attachments
- [117.cpp](/uploads/033f024cfa988a542749b29f197f174f/117.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/878insufficient precoditions given to Alt-Ergo to prove validity of memory acces...2021-04-15T07:31:44ZJochen Burghardtinsufficient precoditions given to Alt-Ergo to prove validity of memory access for user-defined "->" operatorID0002026:
**This issue was created automatically from Mantis Issue 2026. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002026:
**This issue was created automatically from Mantis Issue 2026. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002026 | Frama-Clang | Plug-in > wp | public | 2014-12-11 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The goal given to Alt-Ergo for the memory access in line 13 is:
566 goal main_assert_rte_mem_access:
567 forall t_1,t : int farray.
568 forall a : addr.
569 linked(t) ->
570 valid_rw(t_1, shiftfield_F__Z1X_a(a), 1)
where "t_1" doesn't appear outside the conclusion (line 570), and therefor the formula doesn't hold.
It looks like some "assigns \nothing" was missing in the C++ source; however, there is no more place where such a contract could be added. Maybe some function that is used internally by Cxx needs an additional "assigns" clause?
## Attachments
- [402.cpp](/uploads/a8e1183a90e9cb8e331049d590b3eaa2/402.cpp)
- [main_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/b5497d0bcb4de5a5afd6458a58f4e8ac/main_assert_rte_mem_access_Alt-Ergo.mlw)
- [402a.cpp](/uploads/e84e1416b4bf04f413a3f61071eeb1c4/402a.cpp)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/862namespace prefix in annotation causes segmentation fault2021-03-29T16:41:05ZJochen Burghardtnamespace prefix in annotation causes segmentation faultID0001985:
**This issue was created automatically from Mantis Issue 1985. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001985:
**This issue was created automatically from Mantis Issue 1985. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001985 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
## Attachments
- [147.cpp](/uploads/ee910fafdfbabeb2abdb356f31ad4a03/147.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/858parsing of hex int constant swallows following semicolon2021-03-29T16:45:10ZJochen Burghardtparsing of hex int constant swallows following semicolonID0001980:
**This issue was created automatically from Mantis Issue 1980. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001980:
**This issue was created automatically from Mantis Issue 1980. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001980 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
142.cpp:2:26: Expecting ';' after post-condition
Now output intermediate result
The problem disappears if the "x" and the "0x" is omitted in line 2, thus changing the hexadecimal constant to an octal and decimal one, respectively.
The problem also disappears if the file is renamed to "142.c".
## Attachments
- [142.cpp](/uploads/bc26ae501b50d3387fca4ecd361abe51/142.cpp)Virgile PrevostoVirgile Prevosto