--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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