Commit 973d4e3a authored by Sylvain Dailler's avatar Sylvain Dailler

Attribute model_func does not exist

parent 0da5f41e
......@@ -77,49 +77,6 @@ let add_model_element (el: term) info_model =
let info_model = S.remove el info_model in
S.add el info_model
let add_old attr_str =
let pos = Str.search_forward (Str.regexp "@") attr_str 0 in
let after = String.sub attr_str pos ((String.length attr_str)-pos) in
if after = "@init" then
(String.sub attr_str 0 pos) ^ "@old"
else attr_str
with Not_found -> attr_str ^ "@old"
let model_trace_for_postcondition ~attrs (info: vc_term_info) =
(* Modifies the model_trace attribute of a term in the postcondition:
- if term corresponds to the initial value of a function
parameter, model_trace attribute will have postfix @old
- if term corresponds to the return value of a function,
add model_trace attribute in a form function_name@result
let trace_attr = get_model_trace_attr ~attrs in
let attr_str = add_old trace_attr.attr_string in
if attr_str = trace_attr.attr_string then
let other_attrs = Sattr.remove trace_attr attrs in
(Ident.create_attribute attr_str)
with Not_found ->
(* no model_trace attribute => the term represents the return value *)
((Opt.get_def "" info.vc_func_name) ^ "@result"))
let get_fun_name name =
let splitted = Strings.bounded_split ':' name 2 in
match splitted with
| _::[second] ->
| _ ->
let check_enter_vc_term t in_goal vc_term_info =
(* Check whether the term that triggers VC is entered.
If it is entered, extract the location of the term and if the VC is
......@@ -128,19 +85,7 @@ let check_enter_vc_term t in_goal vc_term_info =
if in_goal && Sattr.mem Ident.model_vc_attr t.t_attrs then begin
vc_term_info.vc_inside <- true;
vc_term_info.vc_loc <- t.t_loc;
(* Attribute "model_func" => the VC is postcondition or precondition *)
(* Extract the function name from "model_func" attribute *)
let fun_attr =
Sattr.choose (Sattr.filter
(fun a -> Strings.has_prefix "model_func:" a.attr_string)
vc_term_info.vc_func_name <- Some (get_fun_name fun_attr.attr_string);
with Not_found ->
(* No "model_func" => the VC is not postcondition or precondition *)
vc_term_info.vc_loc <- t.t_loc
let check_exit_vc_term t in_goal info =
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