How to use option -wp-gen in Frama-C 20 ?

[jensgerlach]

How does the option -wp-gen work in Frama-C 20? Specifically, I would like to obtain the proof obligations for cvc4 (or the other supported provers) of the example find.c below. I tried

frama-c -wp -wp-rte -wp-gen -wp-prover cvc4 -wp-out find.wp find.c

but the directory find.wp is empty except for the empty subdirectory typed.

find.c

/*@
  requires   \valid_read(a + (0..n-1));
  assigns    \nothing;
  ensures    0 <= \result <= n;

  behavior some:
    assumes  \exists integer i; 0 <= i < n && a[i] == val;
    assigns  \nothing;
    ensures  0 <= \result < n;
    ensures  a[\result] == val;
    ensures  \forall integer i; 0 <= i < \result ==> a[i] != val;

  behavior none:
    assumes  \forall integer i; 0 <= i < n ==> a[i] != val;
    assigns  \nothing;
    ensures  \result == n;

  complete behaviors;
  disjoint behaviors;
*/
unsigned int
find(const int* a, unsigned int n, int val)
{
  /*@
    loop invariant 0 <= i <= n;
    loop invariant \forall integer k; 0 <= k < i ==> a[k] != val;
    loop assigns i;
    loop variant n-i;
   */
  for (unsigned int i = 0u; i < n; i++) {
    if (a[i] == val) {
      return i;
    }
  }

  return n;
}

[anonymous3444]

Hi..iam a university student..we're learning frama-c can u help me doing loop pgms?

[jensgerlach]

Probably not.

https://stackoverflow.com/help/how-to-ask

[correnson]

Option -wp-gen is not currently working (it was designed for -wp-prover native:* outputs only). There is a trick : when using cache, digests are computed by pretty-printing the Why3 task for each prover, which is indeed very closed to what is actually sent to solvers, but in pseudo-why3 syntax. These preprints are generated in temporary directory but you can reveal them by using -wp-out <dir>.