0002305: E-ACSL: proper bitfileds handling - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002305

Frama-C

Plug-in > E-ACSL

public

2017-05-29 14:50

2018-02-22 10:33

Reporter

evdenis

Assigned To

fmaurica

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Frama-C 14 Silicon

Target Version

Fixed in Version

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

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

Notes
There are no notes attached to this issue.

Issue History
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