Commit a18b4dd5 authored by Lucas Baudin's avatar Lucas Baudin
Browse files

[Abstract Interpretation] Flags, disjunctive domain

parent 05bd7740
module While1
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
let b(x:int) : int
ensures { result = 18 }
......
open Why3
let is_box = Debug.register_flag ~desc:Pp.empty_formatted "ai-box"
let is_poly = Debug.register_flag ~desc:Pp.empty_formatted "ai-poly"
let is_disj = Debug.register_flag ~desc:Pp.empty_formatted "ai-disj"
let no_ai = Debug.register_flag ~desc:Pp.empty_formatted "no-ai"
let read_channel env path file c =
let a = Env.read_channel Pmodule.mlw_language env (file ^ ".mlw") c in
let module A = Infer_ai.Make (struct let env = env let widening = 2 module D = Domain.Polyhedra end) in
Wstdlib.Mstr.map A.infer_loop_invariants a
let dom =
if Debug.test_flag is_box then
(module Domain.Box : Domain.DOMAIN)
else
(module Domain.Polyhedra : Domain.DOMAIN)
in
let module D = (val dom) in
let dom =
if Debug.test_flag is_disj then
(module Disjunctive_domain_fast.Make(D) : Domain.DOMAIN)
else dom in
let module A = Infer_ai.Make (struct
let env = env
let widening = 5
module D : Domain.DOMAIN = (val dom)
end) in
if Debug.test_flag no_ai then a else Wstdlib.Mstr.map A.infer_loop_invariants a
open Pmodule
open Wstdlib
let convert mm =
let convert m = m.mod_theory in
if Mstr.is_empty mm then Mstr.empty else
match (snd (Mstr.choose mm)).mod_theory.th_path with
| "why3" :: path ->
match (snd (Mstr.choose mm)).mod_theory.th_path with
| "why3" :: path ->
begin try Env.base_language_builtin path
with Not_found -> Mstr.map convert mm end
| _ -> Mstr.map convert mm
with Not_found -> Mstr.map convert mm end
| _ -> Mstr.map convert mm
let imlw_language = Env.register_language Env.base_language convert
......
Supports Markdown
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