GitLab

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.