Skip to content
GitLab
Projects Groups 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
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • 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
  • #259
Closed
Open
Issue created Jan 19, 2018 by mantis-gitlab-migration@mantis-gitlab-migration

Invalid sizeof(struct) calculation in Sulfur

ID0002344: This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002344 Frama-C Plug-in > wp public 2018-01-19 2018-07-11
Reporter abustany Assigned To correnson Resolution no change required
Priority normal Severity minor Reproducibility always
Platform x86_64 OS Linux OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version Frama-C 17-Chlorine

Description :

FramaC version: Sulfur-20171101 (cannot select it in BTS because of #2343 (closed))

With the following C code:


#include <stdint.h> #include <string.h>

typedef struct { uint8_t a; uint8_t b; uint8_t c;

uint16_t d; uint16_t e; uint16_t f; char g[4086]; uint16_t h; } message_t;

/@ requires \valid(msg); @/ void reset_message(message_t *msg) { memset(msg, 0, sizeof(message_t)); }


Running: frama-c -wp -wp-fct reset_message -wp-rte -wp-print err.c

produces the following unprovable goal:


Assume { (* Heap ) Have: (region(msg_0.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0). ( Pre-condition *) Have: valid_rw(Malloc_0, msg_0, 4093). } Prove: valid_rw(Malloc_0, shift_sint8(w, 0), 4098).


Using the Typed+cast model doesn't help.

I'm not really sure how the size of the struct is computed (with regard to alignment or padding), but somehow two different parts of the code seem to disagree here.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking