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 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • 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
  • #1002

Closed
Open
Created Feb 01, 2014 by Jens Gerlach@gerlach

assigns clause appears unprovable

ID0001638: This issue was created automatically from Mantis Issue 1638. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001638 Frama-C Plug-in > wp public 2014-02-01 2014-07-17
Reporter jens Assigned To correnson Resolution open
Priority urgent Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Fluorine-20130601 Target Version - Fixed in Version -

Description :

It appears that assigns clauses of functions that modify an array cannot be verified at all. I attach a simple example of a function set_zero that sets all elements of an array to zero (file set_zero.c). Attached is also an attempt to prove the assigns clause with Coq (see file wp0.script). I do not see how from 0 <= n 0 < i one can conclude i <= n

Please, correct me if I am totally missing something.

Additional Information :

Here is my proof attempt for the assigns clause:

Proof. forward. remember a_0 as a. remember n_0 as n. remember i_0 as i. remember Mint_0 as M0. remember Mint_1 as M1.

cut (i <= n). auto with zarith.

assert(less_equal: 0 <= n). assumption. apply Zle_lt_or_eq in less_equal. rewrite or_comm in less_equal.

destruct less_equal as [equal | less]. (* case equal *) rewrite <- equal. assert (~(i <= 0)). auto with zarith. contradict H7.

(* what now ? *)

Qed.

Attachments

  • set_zero.c
  • pb_assigns.c <- now verified.
Edited Aug 05, 2021 by Allan Blanchard
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking