Learning how to prove Frama-C pre-condition goals

Question

I have the following sample code:

typedef struct {
    BYTE    fs_type;        /* FAT sub-type (0:Not mounted) */
    BYTE    drv;            /* Physical drive number */
} FATFS_temp;

FATFS_temp *FatFs_temp[1];  /* Pointer to the file system objects (logical drives) */

/*@ 
@   requires (vol <= 0) && (fs != \null) ==> \valid((fs)) ; // problematic one

@   behavior mount:
@       //assumes \valid(fs) && vol <= 0;
@       assumes fs != \null && vol <= 0;
@       ensures (vol <= 0) ==> (FatFs_temp[vol] == \old(fs));
@       ensures fs->fs_type == 0;

@   behavior unmount:
@       assumes fs == \null && vol <= 0;        
@       ensures (vol <= 0) ==> (FatFs_temp[vol] == \null);

@   behavior error:
@       assumes vol > 0;
@       ensures \result == 88;  

@   complete behaviors mount, unmount, error;
@   disjoint behaviors mount, unmount, error;
*/

int f_mount_temp (
    BYTE vol,       /* Logical drive number to be mounted/unmounted */
    FATFS_temp *fs      /* Pointer to new file system object (NULL for unmount)*/
)
{
    FATFS_temp *rfs;

    if (vol >= 1)           /* Check if the drive number is valid */
        return 88;
    rfs = FatFs_temp[vol];              /* Get current fs object */

    if (rfs) {
        rfs->fs_type = 0;           /* Clear old fs object */
    }

    if (fs) {
        fs->fs_type = 0;            /* Clear new fs object */
    }
    FatFs_temp[vol] = fs;               /* Register new fs object */

    return 22;
}

But Frama-C / Why3 couldn't prove one of the 'requires' as commented in the code. the .Why file states the following:

goal WP "expl:Pre-condition (file src/ff_temp.c, line 12) in 'f_mount_temp'":
  forall vol_0 : int.
  forall malloc_0 : map int int.
  forall fatFs_temp_0 : map int addr.
  forall fs_0 : addr.
  (fs_0 <> null) ->
  (vol_0 <= 0) ->
  ((linked malloc_0)) ->
  ((is_uint8 vol_0)) ->
  (forall k_0 : int. (0 <= k_0) -> (k_0 <= 0) -> (null = fatFs_temp_0[k_0])) ->
  ((valid_rw malloc_0 fs_0 2))

end

for the sake of learning, my questions are:

1) what is wrong with that pre-condition?

2) based on the outputs in the .Why file, what should my approach be to find out whats wrong?

3) can someone point me to resources to learn how to go about debugging my function contracts?

---

EDIT:

i ran Frama-c with the following flags: "-wp -wp-rte -wp-fct f_mount_temp" i did not call this f_mount_temp from elsewhere. i ran Frama-c to check on this f_mount_temp() directly.

now its clearer to me, its likely the additional assertions that caused the pre-condition to fail. the processed function contracts are the following, with the comments indicating the status of each assertion:

/*@ requires vol ≤ 0 ∧ fs ≢ \null ⇒ \valid(fs); // unknown

    behavior mount: // unknown
      assumes fs ≢ \null ∧ vol ≤ 0;
      ensures \old(vol) ≤ 0 ⇒ FatFs_temp[\old(vol)] ≡ \old(fs);
      ensures \old(fs)->fs_type ≡ 0;

    behavior unmount: //unknown
      assumes fs ≡ \null ∧ vol ≤ 0;
      ensures \old(vol) ≤ 0 ⇒ FatFs_temp[\old(vol)] ≡ \null;

    behavior error: //unknown
      assumes vol > 0;
      ensures \result ≡ 88;

    complete behaviors mount, unmount, error; // green
    disjoint behaviors mount, unmount, error; // green
 */

the inline assertions added by the -wp-rfe flags are:

int f_mount_temp(BYTE vol, FATFS_temp *fs) {
  int __retres;
  FATFS_temp *rfs;
  if ((int)vol >= 1) {
    __retres = 88;
    goto return_label;
  }
  /*@ assert rte: index_bound: vol < 1; */ // ok
  rfs = FatFs_temp[vol];
  if (rfs) {
    /*@ assert rte: mem_access: \valid(&rfs->fs_type); */ //unknown
    rfs->fs_type = (unsigned char)0;
  }
  if (fs) {
    /*@ assert rte: mem_access: \valid(&fs->fs_type); */ // unknown
    fs->fs_type = (unsigned char)0;
  }
  /*@ assert rte: index_bound: vol < 1; */ // unknown
  FatFs_temp[vol] = fs;
  __retres = 22;
  return_label: return __retres;
}

Answer 1

1) what is wrong with that pre-condition?

You are using && and ==> as if their relative precedences were well-known. This is wrong from a human point of view, because as ==> does not appear in many languages other than ACSL, only ACSL specialists can know what a formula that depends on its precedence means.

Apart from that, there can never be anything wrong with a pre-condition in a code snippet that does not involve a call to the function. The pre-condition it not a property that is proved with respect to the implementation of the function but with respect to the context in which the function is used. You could have made a mistake and written the logical equivalent of \false and the pre-condition would still be fine for your snippet (it would only mean that all calls to the function are invalid and must themselves be proved to be unreachable).

For your question to make sense, it would have to either:

• involve the proof (or lack of proof) of a post-condition of f_mount_temp and provide this function's implementation, or
• involve the proof (or lack of proof) of a pre-condition of f_mount_temp and the code of the function in which f_mount_temp is called, including that function's pre-conditions, so that it is possible to tell whether this calling function respects f_mount_temp's pre-condition. In this latter case it is not necessary to provide f_mount_temp's code or post-condition, unless it is called several times in the caller. Also the code of the other functions called from the caller need not be provided, but their contracts should be.

What you have done here, providing f's code and asking why f's pre-condition is not proved, is not coherent.

2) based on the outputs in the .Why file, what should my approach be to find out whats wrong?

This is not a bad place to ask, and I think that you could receive help if you ask again with the right bits of information.

3) can someone point me to resources to learn how to go about debugging my function contracts?

I am not aware of many of these, but this site could become a resource explaining the most common debugging tricks if you ask again…