frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:34:04Z
https://git.frama-c.com/pub/frama-c/-/issues/242
Missing __END_DECLS in ./share/libc/__fc_alloc_axiomatic.h
2021-02-22T13:34:04Z
mantis-gitlab-migration
Missing __END_DECLS in ./share/libc/__fc_alloc_axiomatic.h
ID0002400:
**This issue was created automatically from Mantis Issue 2400. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002400:
**This issue was created automatically from Mantis Issue 2400. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002400 | Frama-C | Plug-in > clang | public | 2018-09-21 | 2018-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | richardlford | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Ubuntu via WSL | **OS Version** | 16 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
In file ./share/libc/__fc_alloc_axiomatic.h there is a
__BEGIN_DECLS but no matching __END_DECLS.
When __BEGIN_DECLS expands to 'extern "C" {' and __END_DECLS expands
to '}' this results in miss-matched braces and the following
code appears to be under and extern "C". This leads to
errors, e.g. when template definitions are encountered.
### Additional Information :
Adding in the missing __END_DECLS removes this problem.
### Steps To Reproduce :
Install Frama-C Chlorine and frama-clang-0.0.6.
use the command "frama-c version.cpp" where version.cpp has this content:
// 'Hello World!' program
#include <iostream>
int main()
{
std::cout << "Hello World, version is "<< __cplusplus << "!" << std::endl;
return 0;
}
## Attachments
- [version.cpp](/uploads/346834ddcee99405a81e7ee8cce118f4/version.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/241
Newer releases of FramaC produce apparent WP plug-in bug
2021-02-22T14:01:18Z
mantis-gitlab-migration
Newer releases of FramaC produce apparent WP plug-in bug
ID0002403:
**This issue was created automatically from Mantis Issue 2403. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002403:
**This issue was created automatically from Mantis Issue 2403. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002403 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2018-10-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached code base is a small example in which a reactive program interacts with peripherals via memory mapped I/O through a constant address. While earlier releases of framaC (Phosphorous) was able to generate full and faithful altergo for our proofs, the new version produces syntactically malformed altergo for the following boolean logic function defined in our example's ACSL:
mac.h line 35:
logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_\
packet.object_low == 0x0A) && (mac->mac_packet.payload_length == 0x00));
Whereas such boolean logic functions were correctly axiomatized in the older (Phosphorous) release, the current version is axiomatizing such a function as :
function L_isAMessage
() :
bool =
andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))
note that the argument to the logic function is absent, and the fields of hte mac_t referenced in the logic function are rendered as "#{w_i}", about which altergo then complains. These malformed altergo expressions seem to have been generated by the pretty printer's find_var function.
### Steps To Reproduce :
tar -xvf framaBug.tar.gz
make wp
## Attachments
- [framaBug.tar.gz](/uploads/54add4d4c38c4a03cb21e9dd404eef64/framaBug.tar.gz)
- [frmaBug.tar.gz](/uploads/fccae63bbfa3517b0d9bc45326a5f0e6/frmaBug.tar.gz)
https://git.frama-c.com/pub/frama-c/-/issues/240
frama-clang fails to compile
2022-09-28T11:04:53Z
mantis-gitlab-migration
frama-clang fails to compile
ID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002402 | Frama-C | Plug-in > clang | public | 2018-10-01 | 2018-10-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | barafael | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 18.04 LTS |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to compile frama-clang, I encounter
Error: Unbounded constructor ASinteger
in file convert_acsl.ml.
ASidentifier is also missing.
### Steps To Reproduce :
Get sources for frama-clang-0.0.6, configure, make
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/236
E-ACSL: proper bitfileds handling
2021-02-22T13:35:41Z
mantis-gitlab-migration
E-ACSL: proper bitfileds handling
ID0002305:
**This issue was created automatically from Mantis Issue 2305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002305:
**This issue was created automatically from Mantis Issue 2305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002305 | Frama-C | Plug-in > E-ACSL | public | 2017-05-29 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | fmaurica | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
E-ACSL generates code which takes address from bitfields. This leads to compilation error.
Test:
#include <stdbool.h>
struct bitfields {
int i : 2;
bool j : 1;
} t;
int test(struct bitfields *a)
{
return a->i;
}
int main(int argc, char **argv)
{
//@ assert \valid_read(&(t.j));
t.j = 1;
return test(&t);
}
E-ACSL code:
struct bitfields t;
int test(struct bitfields *a)
{
int __retres;
/*@ assert rte: mem_access: \valid_read(&a->i); */
{
int __gen_e_acsl_valid_read;
__e_acsl_store_block((void *)(& a),4U);
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& a->i), // ERROR
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",
(char *)"test",
(char *)"rte: mem_access: \\valid_read(&a->i)",10);
__retres = (int)a->i;
}
__e_acsl_delete_block((void *)(& a));
return __retres;
}
int main(int argc, char **argv)
{
int tmp;
__e_acsl_memory_init(& argc,& argv,4U);
__e_acsl_globals_init();
/*@ assert \valid_read(&t.j); */
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& t.j), // ERROR
sizeof(_Bool));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",
(char *)"main",(char *)"\\valid_read(&t.j)",15);
}
__e_acsl_initialize((void *)(& t.j),sizeof(_Bool)); //ERROR
t.j = (_Bool)1;
tmp = test(& t);
__e_acsl_delete_block((void *)(& t));
__e_acsl_memory_clean();
return tmp;
}
GCC Output on E-ACSL code:
# gcc ./generated.c
generated.c: In function ‘test’:
generated.c:86:60: error: cannot take address of bit-field ‘i’
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& a->i),
^
generated.c: In function ‘main’:
generated.c:112:60: error: cannot take address of bit-field ‘j’
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& t.j),
^
generated.c:117:32: error: cannot take address of bit-field ‘j’
__e_acsl_initialize((void *)(& t.j),sizeof(_Bool));
### Additional Information :
Quickfix (doesn't handle __e_acsl_initialize):
diff --git a/translate.ml b/translate.ml
index b5229db..1ea272e 100644
--- a/translate.ml
+++ b/translate.ml
@@ -704,7 +704,17 @@ and named_predicate_content_to_exp ?name kf env p =
| Pvalid_read _ -> "valid_read"
| _ -> assert false
in
- mmodel_call_with_size ~loc kf name Cil.intType env t
+ let ptyp = Cil.unrollType(Typing.typ_of_term(t)) in
+ let typ = match ptyp with
+ | TPtr(a,_) -> a
+ | _ -> assert false
+ in
+ let attr = Cil.typeAttrs typ in
+ if Cil.hasAttribute Cil.bitfield_attribute_name attr
+ then
+ not_yet env "Can't take address from variable with bitfield."
+ else
+ mmodel_call_with_size ~loc kf name Cil.intType env t
in
if !is_visiting_valid then begin
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
### Steps To Reproduce :
frama-c -e-acsl-prepare -rte -rte-precond ./bf.c -then -e-acsl -then-last -print
## Attachments
- [bf.c](/uploads/0e5781355d2eea694674f62ca97a7cc3/bf.c)
- [bitfileds.patch](/uploads/119108c3c57130706e94675406221748/bitfileds.patch)
https://git.frama-c.com/pub/frama-c/-/issues/235
RTE assertion for signed right shift is wrong
2021-02-22T12:57:02Z
mantis-gitlab-migration
RTE assertion for signed right shift is wrong
ID0002354:
**This issue was created automatically from Mantis Issue 2354. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002354:
**This issue was created automatically from Mantis Issue 2354. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002354 | Frama-C | Plug-in > RTE | public | 2018-02-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | xleroy | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Consider:
/*@ ensures \result == arg >> 2; */
int toto(int arg) { return arg >> 2; }
"frama-c -wp -wp-rte" fails to verify this rather tautological spec because the RTE pass inserts the assertion
/*@ assert rte: shift: 0 ≤ arg; */
I think this is an incorrect reading of the ISO C 90 and C 99 specs: right-shift of a signed integer expression that has a negative value is implementation-defined, but is not an undefined behavior. (See ISO C 99 section 6.5.7 item 5.)
I would suggest that WP and RTE accept the spec above, so that I can actually reason about the right shift, probably by adding axioms specifying how right shifts of negative numbers work on the platforms I am (and everyone is) interested in.
https://git.frama-c.com/pub/frama-c/-/issues/234
E-ACSL: internal error: raised at file "src/libraries/project/project.ml", li...
2021-02-22T12:57:00Z
mantis-gitlab-migration
E-ACSL: internal error: raised at file "src/libraries/project/project.ml", line 402
ID0002386:
**This issue was created automatically from Mantis Issue 2386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002386:
**This issue was created automatically from Mantis Issue 2386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002386 | Frama-C | Plug-in > E-ACSL | public | 2018-07-06 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | fmaurica | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Error:
<pre>
$ frama-с -version
Chlorine-20180501
$ frama-с -e-acsl memchr.c
...
[e-acsl] test.c:21: Warning:
E-ACSL construct `variant' is not yet supported. Ignoring annotation.
[e-acsl] test.c:27: Warning:
invalid E-ACSL construct
`non integer variable k in quantification ∀ u8 *k; (u8 *)s ≤ k < p ⇒ *k ≢ (u8)c'.
Ignoring annotation.
[kernel] test.c:26: Failure:
mkBinOp: p - (unsigned char const *)s == __gen_e_acsl_at - n
[kernel] Current source was: test.c:39
The full backtrace is:
Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023
Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 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
Frama-C aborted: internal error.
</pre>
Example code:
<pre>
/*@ requires \typeof(s) <: \type(u8 *);
requires \valid((u8 *)s+(0..n-1));
assigns \nothing;
behavior found:
assumes \exists u8 *p; (u8 *)s <= p < (u8 *)s + n && *p == (u8) c;
ensures s <= \result <= s + n;
ensures \forall u8 *p; (u8 *)s <= p < (u8 *)\result ==> *p != (u8) c;
ensures *((u8 *)\result) == (u8) c;
behavior not_exists:
assumes \forall u8 *p; (u8 *)s <= p < (u8 *)s + n ==> *p != (u8) c;
ensures \result == \null;
complete behaviors;
disjoint behaviors;
*/
void *memchr(const void *s, int c, size_t n)
{
const unsigned char *p = s;
/*@ loop invariant 0 <= n <= \at(n,Pre);
loop invariant (u8 *)s <= p <= (u8 *)s + \at(n,Pre);
loop invariant p - s == \at(n,Pre) - n;
loop invariant \forall u8 *k; (u8 *)s <= k < p ==> *k != (u8) c;
loop variant n;
*/
while (n-- != 0) {
if ((unsigned char) c == *p++) {
return (void *)(p - 1);
}
}
//@ assert n == (size_t)(-1);
return NULL;
}
int main(int argc, char *argv[])
{
const char *s = "1234567890";
void *ptr;
ptr = memchr(s, '0', 11);
ptr = memchr(s, 'a', 11);
ptr = ptr;
return 0;
}
</pre>
## Attachments
- [memchr.c](/uploads/6c87db6bb9861d6b6bb7f2ceb372297c/memchr.c)
- [memchr_v2.c](/uploads/d8f9701b3619dadb6d3936ef60d08be8/memchr_v2.c)
https://git.frama-c.com/pub/frama-c/-/issues/233
Name of RTE plugin in documentation
2021-02-22T13:59:32Z
Jens Gerlach
Name of RTE plugin in documentation
ID0002398:
**This issue was created automatically from Mantis Issue 2398. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002398:
**This issue was created automatically from Mantis Issue 2398. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002398 | Frama-C | Documentation > manuals | public | 2018-09-04 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
The RTE plugin manual has two titles: On the title page it reads "Annotation Generation".
On the third page it reads "Frama-C’s annotation generator plug-in".
Neither title mentions "RTE". Is this intentional?
### Steps To Reproduce :
See http://frama-c.com/download/rte-manual-Chlorine-20180501.pdf
https://git.frama-c.com/pub/frama-c/-/issues/231
Generate out-of-scope variable when using quantified variable in a \old
2021-02-22T12:56:54Z
Julien Signoles
Generate out-of-scope variable when using quantified variable in a \old
ID0001762:
**This issue was created automatically from Mantis Issue 1762. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001762:
**This issue was created automatically from Mantis Issue 1762. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001762 | Frama-C | Plug-in > E-ACSL | public | 2014-04-25 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | fmaurica | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
===== a.i =====
/*@ ensures \forall integer i; 0 <= i < 10 ==> \old(t[i]) == 0; */
void f(int *t) { }
int main(void) {
int t[10];
int i;
for(i = 0; i < 10; i++) t[i] = 0;
f(t);
return 0;
}
================
$ frama-c a.i -e-acsl -then-on e-acsl -print -ocode res.i
$ ./gcc.sh res.i
compiling res.i
res.i: In function ‘__e_acsl_f’:
res.i:84:53: error: ‘__e_acsl_i’ undeclared (first use in this function)
res.i:84:53: note: each undeclared identifier is reported only once for each fun
https://git.frama-c.com/pub/frama-c/-/issues/229
FE_* API is available on OpenBSD
2021-02-22T12:56:52Z
mantis-gitlab-migration
FE_* API is available on OpenBSD
ID0002379:
**This issue was created automatically from Mantis Issue 2379. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002379:
**This issue was created automatically from Mantis Issue 2379. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002379 | Frama-C | Kernel > libc | public | 2018-06-18 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | any | **OS** | OpenBSD | **OS Version** | 6.3 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
please include attached patch.
## Attachments
- [patch-src_libraries_utils_c_bindings_c](/uploads/5d11f5d41c049aab5269993f94365e40/patch-src_libraries_utils_c_bindings_c)
https://git.frama-c.com/pub/frama-c/-/issues/228
user error: scalar value (of type int) initialized by compound initializer
2021-02-22T12:56:50Z
mantis-gitlab-migration
user error: scalar value (of type int) initialized by compound initializer
ID0002384:
**This issue was created automatically from Mantis Issue 2384. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002384:
**This issue was created automatically from Mantis Issue 2384. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002384 | Frama-C | Kernel | public | 2018-07-04 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Example:
<pre>
struct test {
union {
int a;
long b;
};
};
static struct test t = { { .a = 0 } };
</pre>
Run:
<pre>
$ gcc -c test.c
$ echo $?
0
$ frama-c test.c
</pre>
Error Log:
<pre>
[kernel] Parsing test.c (with preprocessing)
[kernel] test.c:1: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
[kernel] test.c:8: User Error:
scalar value (of type int) initialized by compound initializer
6 };
7
8 static struct test t = { { .a = 0 } };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[kernel] User Error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
</pre>
Frama-C Version:
<pre>
$ frama-c -version
Chlorine-20180501
</pre>
## Attachments
- [test.c](/uploads/9b2870c999eda7e90e97626672511315/test.c)
- [restore-initializers.patch](/uploads/9236fdb360274563d8f5bbc41595bd8c/restore-initializers.patch)
https://git.frama-c.com/pub/frama-c/-/issues/227
Failed to install framaC on macosx using opam
2021-02-22T12:56:48Z
mantis-gitlab-migration
Failed to install framaC on macosx using opam
ID0002399:
**This issue was created automatically from Mantis Issue 2399. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002399:
**This issue was created automatically from Mantis Issue 2399. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002399 | Frama-C | Opam | public | 2018-09-11 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.gimbert | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Apple | **OS** | macosx | **OS Version** | HighSierra 10.3. |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Followed step by step the install procedure on http://frama-c.com/install-chlorine-20180501.html#installing-frama-c-on-macos
Failed at the last step, because compilation of alt-ergo 1.30 fails with following message
hugo-3:~ gimbert$ opam install frama-c
The following actions will be performed:
∗ install alt-ergo 1.30 [required by frama-c]
∗ install frama-c 20180502
Alt-Ergo Graphical Interface can be used by the WP plug-in
Yojson enables kernel option -json-compilation-database
===== ∗ 2 =====
Do you want to continue ? [Y/n] Y
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[alt-ergo] Archive in cache
[frama-c] Archive in cache
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[ERROR] The compilation of alt-ergo failed at "make".
Processing 1/2: [alt-ergo: rm]
#=== ERROR while installing alt-ergo.1.30 =====================================#
# opam-version 1.2.2
# os darwin
# command make
# path /Users/gimbert/.opam/system/build/alt-ergo.1.30
# compiler system (4.07.0)
# exit-code 2
# env-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.env
# stdout-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.out
# stderr-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.err
### stdout ###
# [...]
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myDynlink.mli
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myDynlink.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myZip.mli
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myZip.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.mli
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.mli
# ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numbersInterface.mli
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numsNumbers.mli
### stderr ###
# Makefile.users:264: .depend: No such file or directory
# File "/Users/gimbert/.opam/system/build/alt-ergo.1.30/src/util/numsNumbers.mli", line 24, characters 47-62:
# Error: Unbound module Big_int
# make: *** [src/util/numsNumbers.cmi] Error 2
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
The following actions were aborted
∗ install frama-c 20180502
The following actions failed
∗ install alt-ergo 1.30
No changes have been performed
https://git.frama-c.com/pub/frama-c/-/issues/225
Some issues related to Frama-C 18.0 (beta) "Argon"
2021-02-22T13:33:32Z
Jens Gerlach
Some issues related to Frama-C 18.0 (beta) "Argon"
ID0002408:
**This issue was created automatically from Mantis Issue 2408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002408:
**This issue was created automatically from Mantis Issue 2408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002408 | Frama-C | Plug-in > wp | public | 2018-11-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
This entry serves to link my GitHub issues on Argon (beta) to the BTS. The issues are
https://github.com/Frama-C/Frama-C-snapshot/issues/12
https://github.com/Frama-C/Frama-C-snapshot/issues/13
https://github.com/Frama-C/Frama-C-snapshot/issues/14
https://git.frama-c.com/pub/frama-c/-/issues/224
`strlen` used from code makes it no longer possible to prove `assigns \nothing`.
2021-02-22T12:56:40Z
mantis-gitlab-migration
`strlen` used from code makes it no longer possible to prove `assigns \nothing`.
ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002380 | Frama-C | Plug-in > wp | public | 2018-06-23 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | namin | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
`strlen` used from code makes it no longer possible to prove `assigns \nothing`. The definition in the Frama-C library has `@ assigns \result \from indirect:s[0..];`, but this should not prevent check?
### Steps To Reproduce :
$ cat bug.c
#include <string.h>
/*@
requires strlen(s)>=0 && \valid(s+(0..strlen(s)));
assigns \nothing;
*/
int len(char *s) {
return strlen(s);
}
$ frama-c -wp -wp-rte -wp-prover CVC4,alt-ergo bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function len
[wp] 5 goals scheduled
[wp] [Failed] Goal typed_len_assign_normal_part1
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (324ms)
[wp] [Failed] Goal typed_len_assign_exit
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (322ms)
[wp] Proved goals: 3 / 5
Qed: 2 (0.35ms-0.85ms-2ms)
Alt-Ergo: 1 (15ms) (20) (unknown: 2)
CVC4: 0 (interrupted: 2)
https://git.frama-c.com/pub/frama-c/-/issues/223
2D variable length array
2021-02-22T14:01:16Z
Julien Signoles
2D variable length array
ID0002186:
**This issue was created automatically from Mantis Issue 2186. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002186:
**This issue was created automatically from Mantis Issue 2186. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002186 | Frama-C | Kernel | public | 2015-11-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
2D variable length arrays are valid wrt C99 but rejected by Frama-C:
=====
extern int n;
int main(void) {
int a[n]; // accepted
int b[n][n]; // should be accepted, but refused
return 0;
}
=====
$ frama-c a.i
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing a.i (no preprocessing)
a.i:4:[kernel] warning: Variable-sized local variable a
a.i:5:[kernel] user error: Length of array is not a constant: n
a.i:5:[kernel] warning: Variable-sized local variable b
[kernel] user error: stopping on file "a.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
Reported by email by G. Karpenkov
https://git.frama-c.com/pub/frama-c/-/issues/219
Too many edges in call graph
2021-02-22T12:56:35Z
mantis-gitlab-migration
Too many edges in call graph
ID0000435:
**This issue was created automatically from Mantis Issue 435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000435:
**This issue was created automatically from Mantis Issue 435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000435 | Frama-C | Plug-in > callgraph | public | 2010-03-28 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dclist | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
For some reason there are three edges on non-recursive function calls
in the dot file produced by frama-c -scg (see attached)
frama-c -scg foo.dot foo.c && dot -Tpng foo.dot
--------------------------------
int fact(int n)
{
if(n <= 0)
return 0;
else
return fact(n-1);
}
void foo(void)
{
printf("foo\n");
}
int main(void)
{
fact(10);
foo();
}
## Attachments
- [scg-frama.ps](/uploads/490d044b58af5d6a44bce73501b37139/scg-frama.ps)
https://git.frama-c.com/pub/frama-c/-/issues/216
Strange dot callgraphs
2021-02-22T12:56:30Z
mantis-gitlab-migration
Strange dot callgraphs
ID0000989:
**This issue was created automatically from Mantis Issue 989. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000989:
**This issue was created automatically from Mantis Issue 989. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000989 | Frama-C | Plug-in > callgraph | public | 2011-10-19 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
First of all, the callgraph shown in the GUI is not the same than the one generated with the [-cg] option. In the GUI, some of the functions are not displayed at all (g1 and g2 in the enclosed example).
Moreover, in both graphs (from the GUI and the command line), there is an edge between [g] and [nxt] even if [g] doesn't directly call [nxt]...
## Attachments
- [toto.c](/uploads/32fad344b4c6d0d290edf568bdd94f1b/toto.c)
https://git.frama-c.com/pub/frama-c/-/issues/197
Plug-in crash with "Unregistered_library_function" error
2021-02-22T13:35:13Z
Kostyantyn Vorobyov
Plug-in crash with "Unregistered_library_function" error
ID0002192:
**This issue was created automatically from Mantis Issue 2192. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002192:
**This issue was created automatically from Mantis Issue 2192. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002192 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | kvorobyov | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 14-Silicon |
### Description :
/** Instrumentation of the following program leads to the plug-in crash with Unexpected error (Misc.Unregistered_library_function("__store_block")) */
#include <stdlib.h>
char *a;
main(char *argv[]) {
a = argv = atoi(argv[1]);
}
### Additional Information :
This error has been extracted by creduce from one of the SPEC CPU2000 179.art benchmark. There seems to be an issue while processing the atoi ACSL contract. This error is triggered in at least 6 more SPEC benchmarks.
https://git.frama-c.com/pub/frama-c/-/issues/196
Wrong specification for standard library function memmove
2021-02-22T12:56:09Z
Pascal Cuoq
Wrong specification for standard library function memmove
ID0001648:
**This issue was created automatically from Mantis Issue 1648. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001648:
**This issue was created automatically from Mantis Issue 1648. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001648 | Frama-C | Kernel | public | 2014-02-17 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
CONTEXT:
This issue does not originate from an industrial application. It is reported for the lulz.
DESCRIPTION:
The post-condition for memmove() incorrectly describes its effects when source and destination overlap.
/*@ ...
@ ensures memcmp((char*)dest,(char*)src,n) == 0;
...
@*/
extern void *memmove(void *dest, const void *src, size_t n);
In order to be maximally useful, the memcmp logic function, which is defined thus:
/*@ axiomatic MemCmp {
@ logic ℤ memcmp{L}(char *s1, char *s2, ℤ n)
@ reads s1[0..n - 1], s2[0..n - 1];
...
would need to be parameterized by two labels L1 and L2, and state that the memory zone pointed by s1 in L1 is identical to the memory zone pointed by s2 in L2.
Andre Maroneze
Andre Maroneze
https://git.frama-c.com/pub/frama-c/-/issues/188
With -no-lib-entry, the dimension of global structs is not passed to the gene...
2021-02-22T12:55:57Z
Nicky Williams
With -no-lib-entry, the dimension of global structs is not passed to the generator
ID0001490:
**This issue was created automatically from Mantis Issue 1490. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001490:
**This issue was created automatically from Mantis Issue 1490. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001490 | Frama-C | Plug-in > pathcrawler | public | 2013-10-01 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nicky | **Assigned To** | muriel | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Compare the fixed_domain.pl file produced by running
frama-c -pc-analyzer -main test_me microwave.c
and
frama-c -pc-analyzer -main test_me microwave.c -lib-entry
There is no const_dim_input clause for structs mw_state and mw_inputs with the -no-lib-entry option
### Additional Information :
ajout de unrollType dans save_const_dim_input
## Attachments
- [microwave.c](/uploads/97d81542bcb5cea3951f8aaca63fa263/microwave.c)
https://git.frama-c.com/pub/frama-c/-/issues/183
missing E-ACSL code when ignoring asm annotation
2021-03-30T13:44:49Z
mantis-gitlab-migration
missing E-ACSL code when ignoring asm annotation
ID0002413:
**This issue was created automatically from Mantis Issue 2413. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002413:
**This issue was created automatically from Mantis Issue 2413. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002413 | Frama-C | Plug-in > E-ACSL | public | 2018-12-05 | 2018-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.18 OCaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
//////////////// asm.c
void func()
{
int i = 0;
int *ptr=&i;
/*@ assert \valid(ptr); */
*ptr = 0;
}
int main(int argc, char **argv)
{
func();
__asm__ ("");
return 0;
}
////////////////
### Additional Information :
When one comments the __asm__ line and compare the generated code, it seems that the list of missing functions are :
__e_acsl_memory_clean
__e_acsl_store_block
__e_acsl_delete_block
__e_acsl_initialize
__e_acsl_full_init
The problem is similar on Chlorine and Argon.
i and ptr could also be global static variables, it doesn't change anything
### Steps To Reproduce :
$ frama-c -machdep gcc_x86_64 asm.c -e-acsl -then-last -print -ocode eacsl_asm.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing asm.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] asm.c:11: Warning:
E-ACSL construct `asm' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
$ gcc -DE_ACSL_SEGMENT_MMODEL -Wno-attributes -I$(frama-c -print-share-path)/e-acsl/ -o asm eacsl_asm.c $(frama-c -print-share-path)/e-acsl/e_acsl_rtl.c $(frama-c -print-share-path)/../../lib/libeacsl-dlmalloc.a $(frama-c -print-share-path)/../../lib/libeacsl-gmp.a -lm
$ ./asm
Assertion failed at line 5 in function func.
The failing predicate is:
\valid(ptr).
Aborted
## Attachments
- [asm.c](/uploads/82f7e07cbdb3e0f4c91f1bc55aa7f411/asm.c)
Julien Signoles
Julien Signoles