Commit 6f77d846 authored by MARCHE Claude's avatar MARCHE Claude

no need for a return exception anymore

parent 54af3ec2
......@@ -393,10 +393,12 @@ let translate_instr e =
| CFGexpr e -> e
*)
(*
let return_exn = mk_id ~loc:Loc.dummy_position "Return"
let mk_return ~loc e =
mk_expr ~loc (Eraise(Qident return_exn,Some e))
*)
let divergent_attr = ATstr (Ident.create_attribute "vc:divergent")
......@@ -445,7 +447,7 @@ let translate_cfg preconds block blocks =
cases
in
mk_expr ~loc (Ematch(e,branches,[]))
| CFGexpr e when rem=[] -> mk_return ~loc e
| CFGexpr e when rem=[] -> e (* mk_return ~loc e *)
| CFGexpr e1 ->
let e2 = traverse_block rem in
mk_seq ~loc e1 e2
......@@ -472,7 +474,7 @@ let declare_local (loc,idopt,ghost,tyopt) body =
| _ -> failwith "invalid variable declaration"
let build_path_function xpostconds (startlabel, preconds, body) : Ptree.fundef =
let build_path_function retty postconds (startlabel, preconds, body) : Ptree.fundef =
let body =
List.fold_left
(fun acc t ->
......@@ -482,15 +484,10 @@ let build_path_function xpostconds (startlabel, preconds, body) : Ptree.fundef =
body preconds
in
let loc = Loc.dummy_position in
(* this function never returns normally so we put false as normal postcondition *)
let spec = { empty_spec with
sp_post = [(loc,[pat_wild ~loc,term_false ~loc])];
sp_xpost = xpostconds}
in
let loc = Loc.dummy_position in
let spec = { empty_spec with sp_post = postconds} in
let id = mk_id ~loc ("_from_" ^ startlabel) in
let arg = (loc,None,false,Some unit_type) in
(id,false,Expr.RKnone, [arg], Some unit_type, pat_wild ~loc, Ity.MaskVisible, spec, body)
(id,false,Expr.RKnone, [arg], Some retty, pat_wild ~loc, Ity.MaskVisible, spec, body)
let translate_letcfg (id,args,retty,pat,spec,locals,block,blocks) =
......@@ -501,17 +498,20 @@ let translate_letcfg (id,args,retty,pat,spec,locals,block,blocks) =
let body =
mk_expr ~loc (Eidapp(Qident (mk_id ~loc "_from_start"),[mk_unit ~loc]))
in
(*
let body =
mk_seq ~loc body (mk_expr ~loc Eabsurd)
in
*)
(*
let xpost =
List.map
(fun (loc,l) ->
(loc,List.map (fun x -> (Qident return_exn, Some x)) l))
spec.sp_post
in
let defs =
List.map (build_path_function xpost) funs
*) let defs =
List.map (build_path_function retty spec.sp_post) funs
in
let body =
mk_expr ~loc (Erec(defs,body))
......@@ -519,9 +519,11 @@ let translate_letcfg (id,args,retty,pat,spec,locals,block,blocks) =
let body =
List.fold_right declare_local locals body
in
(*
let body =
mk_expr ~loc (Eoptexn(return_exn,Ity.MaskVisible,body))
in
*)
(* ignore termination *)
let body =
mk_expr ~loc (Eattr(divergent_attr,body))
......
......@@ -41,7 +41,7 @@ let cfg cfg_inv (x:int) : int
y
}
(*
let cfg cfg_infinite_loop (x:int) : int
requires { x >= 0 }
ensures { result >= 2 }
......@@ -57,7 +57,7 @@ let cfg cfg_infinite_loop (x:int) : int
y <- y + 1;
goto L;
}
*)
let cfg cfg_finite_loop (x:int) : int
requires { x >= 0 }
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="basic.mlcfg"/>
<theory name="Basic" proved="true">
<goal name="cfgassert&#39;vc" expl="VC for cfgassert" proved="true">
<transf name="split_vc" proved="true" >
<goal name="cfgassert&#39;vc.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="271"/></proof>
</goal>
<goal name="cfgassert&#39;vc.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="211"/></proof>
</goal>
<goal name="cfgassert&#39;vc.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="209"/></proof>
</goal>
</transf>
</goal>
<goal name="cfggoto&#39;vc" expl="VC for cfggoto" proved="true">
<transf name="split_vc" proved="true" >
<goal name="cfggoto&#39;vc.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="797"/></proof>
</goal>
<goal name="cfggoto&#39;vc.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="722"/></proof>
</goal>
</transf>
</goal>
<goal name="cfg_inv&#39;vc" expl="VC for cfg_inv" proved="true">
<transf name="split_vc" proved="true" >
<goal name="cfg_inv&#39;vc.0" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="868"/></proof>
</goal>
<goal name="cfg_inv&#39;vc.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="753"/></proof>
</goal>
<goal name="cfg_inv&#39;vc.2" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="897"/></proof>
</goal>
<goal name="cfg_inv&#39;vc.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="768"/></proof>
</goal>
<goal name="cfg_inv&#39;vc.4" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="898"/></proof>
</goal>
<goal name="cfg_inv&#39;vc.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="737"/></proof>
</goal>
</transf>
</goal>
<goal name="cfg_infinite_loop&#39;vc" expl="VC for cfg_infinite_loop" proved="true">
<transf name="split_vc" proved="true" >
<goal name="cfg_infinite_loop&#39;vc.0" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="840"/></proof>
</goal>
<goal name="cfg_infinite_loop&#39;vc.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="772"/></proof>
</goal>
<goal name="cfg_infinite_loop&#39;vc.2" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="1607"/></proof>
</goal>
<goal name="cfg_infinite_loop&#39;vc.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="842"/></proof>
</goal>
<goal name="cfg_infinite_loop&#39;vc.4" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="737"/></proof>
</goal>
</transf>
</goal>
<goal name="cfg_finite_loop&#39;vc" expl="VC for cfg_finite_loop" proved="true">
<transf name="split_vc" proved="true" >
<goal name="cfg_finite_loop&#39;vc.0" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="840"/></proof>
</goal>
<goal name="cfg_finite_loop&#39;vc.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="772"/></proof>
</goal>
<goal name="cfg_finite_loop&#39;vc.2" expl="check" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="1662"/></proof>
</goal>
<goal name="cfg_finite_loop&#39;vc.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="853"/></proof>
</goal>
<goal name="cfg_finite_loop&#39;vc.4" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="1217"/></proof>
</goal>
<goal name="cfg_finite_loop&#39;vc.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="737"/></proof>
</goal>
</transf>
</goal>
<goal name="main&#39;vc" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="776"/></proof>
</goal>
</theory>
</file>
</why3session>
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