Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • 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 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • 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
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