diff --git a/src/kEvent.ml b/src/kEvent.ml index de042a710..4fc0f4752 100644 --- a/src/kEvent.ml +++ b/src/kEvent.ml @@ -2227,82 +2227,97 @@ let update_trans_sys_sub input_sys analysis trans_sys events = update_trans_sys' trans_sys invars prop_status tl (* Property found true for k steps *) - | (m, PropStatus (p, (Property.PropKTrue k as s))) :: tl -> + | (m, PropStatus (p, (Property.PropKTrue k as s))) :: tl -> ( - (* Change property status in transition system *) - TransSys.set_prop_ktrue trans_sys k p; + try + (* Change property status in transition system *) + TransSys.set_prop_ktrue trans_sys k p; - (* Continue with propert status added to accumulator *) - update_trans_sys' - trans_sys - invars - ((m, (p, s)) :: prop_status) - tl + (* Continue with property status added to accumulator *) + update_trans_sys' + trans_sys + invars + ((m, (p, s)) :: prop_status) + tl + with TransSys.PropertyNotFound _-> + (* Continue without changes *) + update_trans_sys' trans_sys invars prop_status tl + ) (* Property found invariant *) - | (m, PropStatus (p, (Property.PropInvariant cert as s))) :: tl -> + | (m, PropStatus (p, (Property.PropInvariant cert as s))) :: tl -> ( - (* Output proved property *) - log_proved m L_warn trans_sys None p; + try + (* Change property status (of all instances with name [p]) *) + TransSys.set_prop_invariant trans_sys p cert; - (* Change property status (of all instances with name [p]) *) - TransSys.set_prop_invariant trans_sys p cert; + (* Output proved property *) + log_proved m L_warn trans_sys None p; - let term = - TransSys.props_list_of_bound trans_sys Numeral.zero - |> List.assoc p - in + let term = + TransSys.props_list_of_bound trans_sys Numeral.zero + |> List.assoc p + in - (* Retrieve scope to add to invariants. *) - let scope = TransSys.scope_of_trans_sys trans_sys in + (* Retrieve scope to add to invariants. *) + let scope = TransSys.scope_of_trans_sys trans_sys in - let invars = - try (* Add proved property as invariant *) - TransSys.add_invariant trans_sys term cert false - |> insert_inv scope invars false - with Not_found -> (* Skip if named property not found *) - invars - in + let invars = + try (* Add proved property as invariant *) + TransSys.add_invariant trans_sys term cert false + |> insert_inv scope invars false + with Not_found -> (* Skip if named property not found *) + invars + in - let invars = - (* Get property by name *) - let prop = TransSys.property_of_name trans_sys p in - match prop.Property.prop_source with - | Property.Assumption (_, (_, pos)) -> ( - (* If property is a contract assumption that a caller had to prove, - check whether the other assumptions have been proved invariant too. - If so, set SoFar(assumptions) invariant in transition system. - *) - match check_sofar_invariance trans_sys pos with - | Some inv -> insert_inv scope invars false inv - | None -> invars - ) - | _ -> invars - in + let invars = + (* Get property by name *) + let prop = TransSys.property_of_name trans_sys p in + match prop.Property.prop_source with + | Property.Assumption (_, (_, pos)) -> ( + (* If property is a contract assumption that a caller had to prove, + check whether the other assumptions have been proved invariant too. + If so, set SoFar(assumptions) invariant in transition system. + *) + match check_sofar_invariance trans_sys pos with + | Some inv -> insert_inv scope invars false inv + | None -> invars + ) + | _ -> invars + in - (* Continue with property status added to accumulator *) - update_trans_sys' - trans_sys - invars - ( (m, (p, s)) :: prop_status ) - tl + (* Continue with property status added to accumulator *) + update_trans_sys' + trans_sys + invars + ( (m, (p, s)) :: prop_status ) + tl + with TransSys.PropertyNotFound _-> + (* Continue without changes *) + update_trans_sys' trans_sys invars prop_status tl + ) (* Property found false *) - | (m, PropStatus (p, (Property.PropFalse cex as s))) :: tl -> + | (m, PropStatus (p, (Property.PropFalse cex as s))) :: tl -> ( - (* Output disproved property *) - log_cex true m L_warn input_sys analysis trans_sys p cex ; + try + (* Change property status in transition system *) + TransSys.set_prop_false trans_sys p cex; - (* Change property status in transition system *) - TransSys.set_prop_false trans_sys p cex; + (* Output disproved property *) + log_cex true m L_warn input_sys analysis trans_sys p cex ; - (* Continue with property status added to accumulator *) - update_trans_sys' - trans_sys - invars - ((m, (p, s)) :: prop_status) - tl + (* Continue with property status added to accumulator *) + update_trans_sys' + trans_sys + invars + ((m, (p, s)) :: prop_status) + tl + with TransSys.PropertyNotFound _-> + (* Continue without changes *) + update_trans_sys' trans_sys invars prop_status tl + ) (* Property found false *) | (m, StepCex (p, cex)) :: tl -> diff --git a/src/transSys.ml b/src/transSys.ml index d284c48e4..c0d56306d 100644 --- a/src/transSys.ml +++ b/src/transSys.ml @@ -22,6 +22,8 @@ module P = Property module SVM = StateVar.StateVarMap (* module SVS = StateVar.StateVarSet *) +exception PropertyNotFound of string + (* Offset of state variables in initial state constraint *) let init_base = Numeral.zero @@ -1401,7 +1403,7 @@ let set_prop_status { properties } p s = ) false in - if not found then raise Not_found + if not found then raise (PropertyNotFound p) let set_prop_invariant trans_sys p cert = @@ -1425,7 +1427,7 @@ let set_prop_unknown { properties } p = | _ -> found ) false in - if not found then raise Not_found + if not found then raise (PropertyNotFound p) (* Return current status of all properties *) let get_prop_status_all_nocands t = diff --git a/src/transSys.mli b/src/transSys.mli index 9460e7aa8..920f372a5 100644 --- a/src/transSys.mli +++ b/src/transSys.mli @@ -39,6 +39,7 @@ @author Adrien Champion *) +exception PropertyNotFound of string (* Dependencies: initial state predicate may occur in the transition relation in condacts, and if we support reset. *)