Commit c46553b1 authored by MARCHE Claude's avatar MARCHE Claude

avoid infinite loop in CFG translation

parent b6b769e2
......@@ -42,6 +42,7 @@
"cfg", CFG;
"goto", GOTO;
"var", VAR;
"switch", SWITCH;
"abstract", ABSTRACT;
"absurd", ABSURD;
"alias", ALIAS;
......
......@@ -379,7 +379,8 @@ let translate_cfg preconds block blocks =
Wstdlib.Mstr.empty
blocks
in
let visited = ref [] in
let startlabel = "start" in
let visited = ref [startlabel] in
let rec traverse startlabel preconds bl acc (funs,ret_funs) =
match bl with
| [] -> assert false
......@@ -394,7 +395,11 @@ let translate_cfg preconds block blocks =
traverse startlabel preconds bl acc (funs,ret_funs)
| CFGinvariant(id,t) ->
let funs = (startlabel, preconds, id, t, acc) :: funs in
traverse id.id_str [t] rem [] (funs,ret_funs)
if List.mem id.id_str !visited then (funs,ret_funs) else
begin
visited := id.id_str :: !visited;
traverse id.id_str [t] rem [] (funs,ret_funs)
end
| CFGswitch _ ->
failwith "switch not suported yet"
| CFGexpr e when rem=[] ->
......@@ -403,7 +408,7 @@ let translate_cfg preconds block blocks =
| CFGexpr e ->
traverse startlabel preconds rem (e::acc) (funs,ret_funs)
in
traverse "start" preconds block [] ([],[])
traverse startlabel preconds block [] ([],[])
let e_ref = mk_expr ~loc:Loc.dummy_position Eref
......
......@@ -81,8 +81,8 @@ instr:
{ mk_cfginstr (CFGgoto $2) $startpos $endpos }
| contract_expr
{ mk_cfginstr (CFGexpr $1) $startpos $endpos }
| SWITCH contract_expr cases END
{ mk_cfginstr (CFGswitch ($2,$3)) $startpos $endpos }
| SWITCH contract_expr WITH cases END
{ mk_cfginstr (CFGswitch ($2,$4)) $startpos $endpos }
| INVARIANT ident LEFTBRC term RIGHTBRC
{ mk_cfginstr (CFGinvariant($2,$4)) $startpos $endpos }
......
......@@ -40,7 +40,40 @@ let cfg cfg_inv (x:int) : int
y
}
let cfg cfg_infinite_loop (x:int) : int
requires { x >= 0 }
ensures { result >= 2 }
=
var (y:int);
{
y <- 0;
goto L;
}
L {
y <- y + 1;
invariant I { exists z. y = z+z+1 };
y <- y + 1;
goto L;
}
let cfg cfg_finite_loop (x:int) : int
requires { x >= 0 }
ensures { result >= 2 }
=
var (y:int);
{
y <- 0;
goto L;
}
L {
y <- y + 1;
invariant I { exists z. y = z+z+1 };
y <- y + 1;
switch y <= x with
| True -> goto L
| False -> y
end
}
let main () =
......
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