--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on December 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problems with recognition of the variant



Hello,

Le 12/12/2014 08:22, Roberto Bagnara a ?crit :
> Apparently the latest version
> of Frama-C is not able to prove that a nonzero unsigned quantity
> shifted to the right by a nonzero number of positions results
> in a strict decrease.

Frama-C is known to be weak on bit-related operations. It has been told 
on this list that this part is under work.

>  Replacing shift by integer division does
> not help.

This is strange. On attached example, the variant with a division is 
proved without any issue.

"""
$ frama-c -wp shift-variant.c
[kernel] preprocessing with "gcc -C -E -I.  shift-variant.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
shift-variant.c:9:[wp] warning: Missing assigns clause (assigns 
'everything' instead)
shift-variant.c:23:[wp] warning: Missing assigns clause (assigns 
'everything' instead)
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_testVariant_div_loop_term_positive : Valid 
(12ms) (4)
[wp] [Alt-Ergo] Goal typed_testVariant_div_loop_term_decrease : Valid 
(20ms) (10)
[wp] [Alt-Ergo] Goal typed_testVariant_loop_term_positive : Valid (15ms) (4)
[wp] [Alt-Ergo] Goal typed_testVariant_loop_term_decrease : Unknown
[wp] Proved goals:    3 / 4
      Qed:             0
      Alt-Ergo:        3  (12ms-20ms) (10) (unknown: 1)
"""

Best regards,
david

-------------- next part --------------
void
testVariant(unsigned long n) {
  unsigned long i;

  i = n;
 
  /*@loop variant i;
   */
  while (i >= 2UL) {
    i >>= 2UL;
    }

}

void
testVariant_div(unsigned long n) {
  unsigned long i;

  i = n;
 
  /*@loop variant i;
   */
  while (i >= 2UL) {
    i /= 4UL;
    }

}