| 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 | |
| Platform | | OS | | OS Version | |
| 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
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 |  bf.c [^] (231 bytes) 2017-05-29 14:50 [Show Content] [Hide Content]#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);
}
 bitfileds.patch [^] (1,280 bytes) 2017-05-29 14:50 [Show Content] [Hide Content]diff --git a/translate.ml b/translate.ml
index 674e15c..a835057 100644
--- a/translate.ml
+++ b/translate.ml
@@ -629,15 +629,17 @@ and named_predicate_content_to_exp ?name kf env p =
| Pvalid_read _ -> "valid_read"
| _ -> assert false
in
- let typ = Cil.unrollType(Typing.typ_of_term(t)) in
- match typ with
- | TPtr(TInt(_,attr), _) ->
- 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
- | _ -> 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):
|
|
Relationships 
Relationships