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] problems with recognition of the variant

  • Subject: [Frama-c-discuss] problems with recognition of the variant
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Fri, 12 Dec 2014 08:33:24 +0100
  • In-reply-to: <548A97AE.7010808@cs.unipr.it>
  • References: <CAAEWojUFkWjLv9yDjp37=zP0coN1xnFxuuhNc0ER_570HpFpYQ@mail.gmail.com> <548A97AE.7010808@cs.unipr.it>
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;
    }

}