Merge branch 'feature/boris/valid-function-predicate' into 'master'

Adapt to branch feature/boris/valid-function-predicate



See merge request !20

src/plugins/e-acsl/mmodel_analysis.ml

@@ -310,6 +310,7 @@ module rec Transfer
     | Pfresh _ -> Error.not_yet "\\fresh"
     | Pseparated _ -> Error.not_yet "\\separated"
     | Pdangling _ -> Error.not_yet "\\dangling"
+    | Pvalid_function _ -> Error.not_yet "\\valid_function"
     | Ptrue | Pfalse | Papp _ | Prel _
     | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _ 
     | Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->

src/plugins/e-acsl/translate.ml

@@ -564,6 +564,7 @@ and named_predicate_content_to_exp ?name kf env p =
   | Papp _ -> not_yet env "logic function application"
   | Pseparated _ -> not_yet env "\\separated"
   | Pdangling _ -> not_yet env "\\dangling"
+  | Pvalid_function _ -> not_yet env "\\valid_function"
   | Prel(rel, t1, t2) -> 
     let e, env = 
       comparison_to_exp ~loc kf env (relation_to_binop rel) t1 t2 None 

src/plugins/e-acsl/typing.ml

@@ -452,6 +452,7 @@ let rec type_predicate_named p =
   | Papp _ -> Error.not_yet "logic function application"
   | Pseparated _ -> Error.not_yet "\\separated"
   | Pdangling _ -> Error.not_yet "\\dangling"
+  | Pvalid_function _ -> Error.not_yet "\\valid_function"
   | Prel(_, t1, t2) -> 
     ignore (type_term t1);
     ignore (type_term t2)