Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
    • Help
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project
    • Project
    • Details
    • Activity
    • Releases
    • Cycle Analytics
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
  • Issues 58
    • Issues 58
    • List
    • Board
    • Labels
    • Milestones
  • Merge Requests 8
    • Merge Requests 8
  • Registry
    • Registry
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #206

Closed
Open
Opened Oct 10, 2018 by Guillaume Melquiond@melquion
  • Report abuse
  • New issue
Report abuse New issue

Incorrect detection of effect interference during extraction, part 2

use ref.Ref, mach.int.Int63
let f (x: ref (ref int63)): int63 = x.contents <- ref 3; 0
let g () = let y = ref 5 in f (ref y) + !y

is extracted to

let f (x: ((int) ref) ref) : int =
  begin let o = ref 3 in x.contents <- o; 0 end
let g (_: unit) : int = let y = ref 5 in let o = f (ref y) in o + (!y)

So, the "read" effect of !y has been inlined past the "reset" effect of f (ref y). Contrarily to #200 (closed) , the obtained extracted code does not exhibit an unsoundness. But, if one were to model the C free function using only a reset effect on the pointed zone (which is not the case currently, since resets are not available in the surface language), then it would presumably be possible to provoke a use-after-free bug.

Assignee
Assign to
1.2.0
Milestone
1.2.0
Assign milestone
Time tracking
None
Due date
No due date
2
Labels
component: extraction soundness
Assign labels
  • View project labels
Reference: why3/why3#206