View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002305 | Frama-C | Plug-in > E-ACSL | public | 2017-05-29 14:50 | 2018-11-30 10:07 | ||||
Reporter | evdenis | ||||||||
Assigned To | fmaurica | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C 14-Silicon | ||||||||
Target Version | Frama-C 18-Argon | Fixed in Version | Frama-C 18-Argon | ||||||
Summary | 0002305: E-ACSL: proper bitfileds handling | ||||||||
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)); | ||||||||
Steps To Reproduce | frama-c -e-acsl-prepare -rte -rte-precond ./bf.c -then -e-acsl -then-last -print | ||||||||
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): | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
signoles (manager) 2018-10-02 15:59 |
A patch similar to yours was implemented: E-ACSL now ignores annotations containing addresses from bitfields. A sound support for such terms is postponed yet. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2017-05-29 14:50 | evdenis | New Issue | |
2017-05-29 14:50 | evdenis | Status | new => assigned |
2017-05-29 14:50 | evdenis | Assigned To | => signoles |
2017-05-29 14:50 | evdenis | File Added: bf.c | |
2017-05-29 14:50 | evdenis | File Added: bitfileds.patch | |
2017-05-29 14:51 | signoles | Assigned To | signoles => kvorobyov |
2017-10-24 17:42 | signoles | Assigned To | kvorobyov => signoles |
2018-02-22 10:33 | signoles | Assigned To | signoles => fmaurica |
2018-10-02 13:24 | signoles | Target Version | => Frama-C 18-Argon |
2018-10-02 15:59 | signoles | Note Added: 0006657 | |
2018-10-02 15:59 | signoles | Status | assigned => resolved |
2018-10-02 15:59 | signoles | Resolution | open => fixed |
2018-11-30 10:07 | signoles | Fixed in Version | => Frama-C 18-Argon |
2018-11-30 10:07 | signoles | Status | resolved => closed |