Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic

  • Subject: [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Wed, 4 Sep 2013 14:13:27 +0000
  • In-reply-to: <CAC3Lx=aO-5GZmk_SOJ1w8=9P=VoXFM0K1Wf7xptVXR1a4YXYwA@mail.gmail.com>
  • References: <CAC3Lx=aO-5GZmk_SOJ1w8=9P=VoXFM0K1Wf7xptVXR1a4YXYwA@mail.gmail.com>
Hello,

Replacing in the source code in the main() function:

  for (i=98; i>0; i--) {
    if (pop() != i)
      abort();
  }

by:

  for (i=98; i>0; i--) {
	unsigned tmp = pop();
    if (tmp != i)
      abort();
  }

permits to bypass the problem (ie, almost all VCs are discharged).

I let Frama-C experts explain what occurred in more details?!

HTH,
D.

> -----Message d'origine-----
> De?: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-
> discuss-bounces at lists.gforge.inria.fr] De la part de David MENTRE
> Envoy??: mercredi 4 septembre 2013 15:18
> ??: Frama-C public discussion
> Objet?: [Frama-c-discuss] Issues with WP on program doing simple
> pointer arithmetic
> 
> Hello,
> 
> I am trying to verify with WP (Frama-C Fluorine June release, Alt-Ergo
> 0.95.1) the absence of Run Time Errors (RTE) in the attached program
> which does some simple pointer manipulation.
> 
> I don't understand to main points:
>   1. In main(), why WP cannot prove simple invariant like "0 <= i <=
> 99;"? The call to pop() or push() apparently annoys it. But I don't
> understand why. In loop(), I have similar invariant without such call
> which are correctly proved.
> 
>   2. Why WP does not even try to prove ("Status: no verification
> attempted") some predicates: \valid() in pop() and push() requires
> clauses, loop assigns and variant in main(), even rte for i++ in the
> first loop of main()? In the same way, in loop() function I have a
> requirement on \valid(global_i_ptr) and this predicate is properly
> checked and proved.
> 
> If somebody has some enlightenments, I would very glad to hear them.
> 
> I launch WP with:
>  frama-c-gui -cpp-command 'gcc -C -E -I/path/to/share/frama-c/libc'
> -wp -wp-rte -wp-par 8 q6_stack.c
> 
> The properties are proved using Value analysis and -slevel 1000 (except
> assigns and loop variant which are not looked at).
> 
> Best regards,
> david