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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • 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
  • #2549

Closed
Open
Created Apr 02, 2021 by Ricardo M. Correia@wizeman3 of 3 tasks completed3/3 tasks

Undefined behavior in pointer arithmetic

Before submitting the issue, please confirm (by adding a X in the [ ]):

  • the issue has not yet been reported on Gitlab;
  • the issue has not yet been reported on our old BTS (note: the old BTS is deprecated);
  • you installed Frama-C as prescribed in the instructions.

Contextual information

  • Frama-C installation mode: package from NixOS/nixpkgs
  • Frama-C version: 21.1 and master commit 2fc09908 (from 2021-03-31) (as reported by frama-c -version)
  • Plug-in used: WP
  • OS name: NixOS
  • OS version: 20.09+patches

Please add specific information deemed relevant with regard to this issue.

Steps to reproduce the issue

Given the following C file called pointer.c:

#include <stddef.h>

/*@
    requires \valid(&p[0..len-1]);
*/
int *one_minus(int *p) /*@ ghost (size_t len) */
{
    return p - 1;
}

/*@
    requires \valid(&p[0..len-1]);
*/
int *plus_two(int *p, size_t len)
{
    return p + len + 1;
}

... I then run the following frama-c command:

$ frama-c -wp -wp-prover Z3 -wp-rte -wp-smoke-tests -wp-par 8 -wp-cache rebuild -warn-signed-downcast -warn-unsigned-downcast -warn-unsigned-overflow -warn-right-shift-negative "$@" -then -report-no-proven -report pointer.c

Expected behaviour

I would've expected Frama-C to point out that both functions can have undefined behavior, i.e. they should have unproven properties/goals.

Perhaps I'm misunderstand Frama-C's limitations or the C standard, but as far as I understand, C considers references to 1 index below or 2 indexes above the valid addresses of an allocated array to be undefined behaviors, i.e. you can't even reference those addresses. Thus, dereference is not even necessary for undefined behavior, except for the special case of 1 index past the valid addresses of an allocated array, which is valid to reference but not valid to dereference.

Actual behaviour

With Frama-C 21.1, I get the following result:

[kernel] Parsing pointer.c (with preprocessing) 
[rte] annotating function one_minus
[rte] annotating function plus_two
[wp] 2 goals scheduled                                                                                                                                                                        
[wp] [Cache] updated:2                                                                         
[wp] Proved goals:    2 / 2
  Qed:                           0  (0.89ms-1ms)
  Z3 4.8.8 (counterexamples):    2
[report] Computing properties status...
--------------------------------------------------------------------------------
--- No status to report
-------------------------------------------------------------------------------- 

No warnings or errors.

I skipped Frama-C 22.0 because I encountered more serious, but unrelated, correctness issues in that version.

With Frama-C master branch, commit 2fc09908 (from 2021-03-31):

[kernel] Parsing pointer.c (with preprocessing)
[rte] annotating function one_minus
[rte] annotating function plus_two
[wp] 2 goals scheduled
[wp] [Cache] updated:2
[wp] Proved goals:    2 / 2
  Qed:                           0  (0.94ms-2ms)
  Z3 4.8.8 (counterexamples):    2
[wp:pedantic-assigns] pointer.c:6: Warning: 
  No 'assigns' specification for function 'one_minus'.
  Callers assumptions might be imprecise.
[wp:pedantic-assigns] pointer.c:14: Warning: 
  No 'assigns' specification for function 'plus_two'.
  Callers assumptions might be imprecise.
[report] Computing properties status...
--------------------------------------------------------------------------------
--- No status to report
--------------------------------------------------------------------------------

Just a couple of warnings about callers assumptions being imprecise. This doesn't indicate that there's a problem with the function implementations.

Fix ideas

I don't know of any workarounds. I'm guessing new goals should be added to make sure pointers can only point to either valid memory addresses or addresses one past the end of an array.

Edited Nov 10, 2021 by Virgile Prevosto
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking