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] similar assertions not all validated

  • Subject: [Frama-c-discuss] similar assertions not all validated
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 17 Apr 2012 15:42:50 +0200
  • In-reply-to: <0627805BEE18C14981A31E75C2452AA123AD5E490A@Y000IMRV02.rd1.rf1>
  • References: <0627805BEE18C14981A31E75C2452AA123AD5E490A@Y000IMRV02.rd1.rf1>
Hello,

2012/4/17 MULLER Nicolas (SAGEM DEFENSE SECURITE) <nicolas.muller at sagem.com>:
> the question here is why are the provers not able to prove those two lines
> of annotations but could prove them in the next few lines but with different
> variables ?

The invariants of your loops are invalid. I attach a patch that fixes them.

With the above patch applied, several loop invariants and assertions
are not proved, equally spread on your three loops. I haven't tried to
prove them.

How I found that? Using value analysis plugin of frama-c. If you use:
  frama-c-gui -val -slevel 1000 abs_new.c

You'll see that the invariant at line 16 ("(i == 0) && (i < 51)") is
proven invalid by value analysis:
"""
abs_new.orig.c:20:[value] Loop invariant got status invalid (stopping
propagation)
"""

Using i==1 obviously invalidates your invariant.

And all the remaining of your code is considered dead.

Why on your initial code the loop invariants where proven valid? My
guess is that the invalid invariant or an unproven assertion was used
as hypothesis to prove the remaining VCs. But I let Frama-C experts
explain the precise reason.

My advice would be to avoid using assertions. As they are taken as
hypothesis for following code, wrong assertions can lead to prove
incorrect logic annotations. Better is to write correct annotations
that are proved progressively, one line after the other.

Best regards,
d.

PS: Used versions: Frama-C Nitrogen, Why (i.e. Jessie) 2.30, Why3 of
latest git, Alt-Ergo 0.94 and Z3 3.2.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: abs_new_invariant-fix.patch
Type: application/octet-stream
Size: 1088 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120417/ff36de4f/attachment.obj>