Commit 9251281e authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: a bug to fix in test-pgm

parent d8f1cdd7
{
use import list.List
logic f(int, int) : int
logic c : int
type 'a t
}
parameter sub : x:int -> y:int -> { x>=y } int { result=x-y }
parameter malloc : int -> {} 'a t { result=result }
parameter imp_sub :
x:int ref -> y:int ref -> { !x >= !y } unit writes x { !x = old(!x) - !y }
parameter r : int ref
parameter write : v:int -> {} unit writes r { !r = v }
exception E of int
exception F
let test () =
{ !r = 0 }
while !r < 100 do
invariant { !r <= 100 }
r := !r + 1
done
{ !r = 100 }
let foo () = malloc 1 : int t
(*
Local Variables:
......
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