Commit 8c721d48 authored by MARCHE Claude's avatar MARCHE Claude

ML example exposing bug 12244

parent 383157bb
......@@ -933,6 +933,9 @@ test-api: src/why.cma
ocaml $(EXTCMA) src/why.cma -I src examples/use_api.ml \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
bts12244: src/why.cma
ocaml $(EXTCMA) src/why.cma -I src examples/bts12244.ml
## Examples : Plugins ##
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(*******************
This file exposes bug 12244 directly using the API
******************)
open Why
open Format
(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* builds the environment from the [loadpath] *)
let env : Env.env = Lexer.create_env (Whyconf.loadpath main)
let int_theory : Theory.theory = Env.find_theory env ["int"] "Int"
(*
An arithmetic goal: 1 = 2
*)
let one : Term.term = Term.t_const (Term.ConstInt "1")
let two : Term.term = Term.t_const (Term.ConstInt "2")
let fmla : Term.term = Term.t_equ one two
let task = Task.use_export None int_theory
let goal_id = Decl.create_prsymbol (Ident.id_fresh "G")
let task = Task.add_prop_decl task Decl.Pgoal goal_id fmla
(*
let () = printf "@[task:@\n%a@]@." Pretty.print_task task
*)
let inline = Trans.lookup_transform "inline_goal" env
let split = Trans.lookup_transform_l "split_goal" env
let task_inline = Trans.apply inline task
let () = printf "@[task == task_inline ? %b@]@." (task == task_inline)
let task_split =
match Trans.apply split task with
| [t] -> t
| _ -> assert false
let () = printf "@[task == task_split ? %b@]@." (task == task_split)
......@@ -1486,16 +1486,15 @@ let transformation_on_goal g tr =
let b =
match subgoals with
| [task] ->
let s1 = task_checksum (get_task g) in
let s2 = task_checksum task in
(*
eprintf "Transformation returned only one task. sum before = %s, sum after = %s@." (task_checksum g.task) (task_checksum task);
eprintf "addresses: %x %x@." (Obj.magic g.task) (Obj.magic task);
*)
s1 <> s2
(*
(* let s1 = task_checksum (get_task g) in *)
(* let s2 = task_checksum task in *)
(* (\* *)
(* eprintf "Transformation returned only one task. sum before = %s, sum after = %s@." (task_checksum g.task) (task_checksum task); *)
(* eprintf "addresses: %x %x@." (Obj.magic g.task) (Obj.magic task); *)
(* *\) *)
(* s1 <> s2 *)
task != (get_task g)
*)
| _ -> true
in
if b then
......
......@@ -159,6 +159,8 @@ theory TestInline
use import int.Int
goal T : 1 = 2
logic p (x:int) (y:int) = x <= 3 and y <= 7
goal G : p 4 4
......
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