Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 177
    • Issues 177
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #236

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 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
  • bitfileds.patch
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking