Commit ca7899d1 authored by Sylvain Dailler's avatar Sylvain Dailler

Simplify transformation for counterexample code

parent 3e532a25
......@@ -15,32 +15,10 @@ open Decl
open Theory
open Ty
let model_trace_regexp = Str.regexp "model_trace:"
(* The term with attribute "model_trace:name" will be
in the counterexample with name "name" *)
let attr_starts_with regexp a =
try
ignore(Str.search_forward regexp a.attr_string 0);
true
with Not_found -> false
let string_starts_with regexp s =
try
ignore(Str.search_forward regexp s 0);
true
with Not_found -> false
let get_attr attrs regexp =
Sattr.choose (Sattr.filter (attr_starts_with regexp) attrs)
let is_proj_for_array_attr proj_name =
let b =
try
string_starts_with (Str.regexp "'First\\|'Last\\|\\.") proj_name
with Not_found -> false in
b
match Str.search_forward (Str.regexp "'First\\|'Last\\|\\.") proj_name 0 with
| _ -> true
| exception Not_found -> false
(*
(* Debugging functions *)
......@@ -229,15 +207,8 @@ let build_projections_map projs =
in
Sls.fold build_map projs Ty.Mty.empty
(* TODO we want to be able to write this. It seems not possible with Trans and
more efficient than the version we have below.
let meta_transform2 f : Task.task -> Task.task = fun task ->
Trans.apply (Trans.fold (fun d t ->
Trans.apply (Trans.add_decls (f d)) t) task) task
*)
(* [meta_transform2 f t] Generate new declarations by applying f to each declaration of t
and then append these declarations to t *)
(* [meta_transform2 f t] Generate new declarations by applying f to each
declaration of t and then append these declarations to t *)
let meta_transform2 f : Task.task Trans.trans =
let list_decl = Trans.fold (fun d l -> l @ (f d)) [] in
Trans.bind list_decl (fun x -> Trans.add_decls x)
......
......@@ -12,15 +12,6 @@
(* Handling of attributes *)
val model_trace_regexp: Str.regexp
(* The term tagged with "model_trace:name" will be in counterexample
with name "name" *)
val attr_starts_with: Str.regexp -> Ident.attribute -> bool
val get_attr: Ident.Sattr.t -> Str.regexp -> Ident.Sattr.elt
val intro_projections_counterexmp : Env.env -> Task.task Trans.trans
(**
Transformation that for each declared abstract function or predicate
......
......@@ -22,9 +22,6 @@ let meta_vc_location =
Theory.register_meta_excl "vc_location" [Theory.MTstring]
~desc:"Location@ of@ the@ term@ that@ triggers@ vc@ in@ the@ form@ file:line:col."
let model_trace_prefix = "model_trace:"
(* The term tagged with "model_trace:name" will be in counterexample with name "name" *)
(* Information about the term that triggers VC. *)
type vc_term_info = {
vc_inside : bool;
......@@ -35,10 +32,6 @@ type vc_term_info = {
(* true if VC was generated for precondition or postcondition *)
}
let get_attr attrs prefix =
let check l = Strings.has_prefix prefix l.attr_string in
Sattr.choose (Sattr.filter check attrs)
let is_model_vc_attr l =
attr_equal l model_vc_attr || attr_equal l model_vc_post_attr
......@@ -76,18 +69,18 @@ let model_trace_for_postcondition ~attrs =
Returns attrs with model_trace attribute modified if there
exist model_trace attribute in attrs, attrs otherwise.
*)
try
let trace_attr = get_attr attrs model_trace_prefix in
let attr_str = add_old trace_attr.attr_string in
if attr_str = trace_attr.attr_string then
match get_model_trace_attr ~attrs with
| trace_attr ->
let attr_str = add_old trace_attr.attr_string in
if attr_str = trace_attr.attr_string then
attrs
else
let other_attrs = Sattr.remove trace_attr attrs in
Sattr.add
(Ident.create_attribute attr_str)
other_attrs
| exception Not_found ->
attrs
else
let other_attrs = Sattr.remove trace_attr attrs in
Sattr.add
(Ident.create_attribute attr_str)
other_attrs
with Not_found ->
attrs
(* Preid table necessary to avoid duplication of *_vc_constant *)
module Hprid = Exthtbl.Make (struct
......
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