Commit 8e493c49 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Add tests

parent a289a249
use map.Map
use array.Array
use mach.c.C
use int.Int
use mach.int.UInt64
val f (p1 p2: ptr uint64) : unit
requires { valid p1 2 }
requires { valid p2 2 }
requires { offset p1 = 0 }
requires { offset p2 = 1 }
alias { p1.data with p2.data }
writes { p1.data.elts,p2.data.elts }
let g () : unit
=
let p1 = malloc 5 in
let p2 = malloc 5 in
let p3 = incr p2 1 in
f p1 p3
\ No newline at end of file
use map.Map
use array.Array
use mach.c.C
use int.Int
use mach.int.UInt64
val alloc2 () : (r1:ptr uint64, r2:ptr uint64)
ensures { offset r1 = 0 /\ offset r2 = 0 }
ensures { valid r1 0 /\ valid r2 0 }
alias { r1.data with r2.data }
let free2_sep (p1 p2:ptr uint64) : unit
requires { offset p1 = 0 }
requires { offset p2 = 0 }
requires { valid p1 0 }
requires { valid p2 0 }
writes { p1, p1.data, p2, p2.data }
=
free p1;
free p2
let bad () =
let r1, r2 = alloc2 () in
free2_sep r1 r2
\ No newline at end of file
use map.Map
use array.Array
use mach.c.C
use int.Int
use mach.int.UInt64
let double_free (p1 p2:ptr uint64)
requires { offset p1 = 0 }
requires { offset p2 = 0 }
alias { p1.data with p2.data }
requires { valid p1 0 }
requires { valid p2 0 }
=
free p1; (* resets p2 *)
free p2
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment