Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2

Closed
Open
Created May 06, 2020 by Jens Gerlach@gerlach

[wp] non-provable local typing constraints in lemmas

Steps to reproduce the issue

The attached archive contains the ACSL function Count together with several lemma. Also contained are

  • a Makefile
  • a coq proof in file wp0.script.20 for lemma CountBounds that works for Frama-C 20
  • an attempt of a coq proof in file wp0.script.21 for lemma CountBounds that fails for Frama-C 21
  • The files CountBounds.v.20 and CountBounds.v.21 contain the coq code as extracted from CoqIde

Expected behaviour

My problem is that I am unable to adapt the coq proof that worked fro Frama-C 20 to the newer version of Frama-C.

Actual behaviour

I suspect that this is related to changes in the generated Coq code of the VC of lemma CountBounds This can be best seen when calling diff CountBounds.v.20 CountBounds.v.21.

$ diff CountBounds.v.20  CountBounds.v.21 
39,40c39,40
<   (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((i < i_1)%Z) ->
<   ((is_sint32 i_2%Z)) ->
---
>   let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((x_1 <> i_2)%Z) ->
>   ((i < i_1)%Z) -> ((is_sint32 i_2%Z)) -> ((is_sint32 x_1)) ->

Fix ideas

I think the issue is caused by the condition ((is_sint32 x_1)) for the newly introduced term x_1 := (t.[ (shift_sint32 a x) ])%Z. I haven't found a way to satisfy the condition ((is_sint32 x_1)) and I suspect that it is not possible. If it is possible, then I apologise and ask for a hint.

Regards

Jens Gerlach

CoqFramac21.tar

Edited May 12, 2020 by Loïc Correnson
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking