diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml index 959e309b8c046acdf381ccf62a81e8bafae19394..f3b84c5c3098f64a983c172bfb457aa6f4446639 100644 --- a/src/plugins/e-acsl/main.ml +++ b/src/plugins/e-acsl/main.ml @@ -63,7 +63,7 @@ let generate_code = (fun name -> try let visit prj = Visit.do_visit ~prj true in - File.create_project_from_visitor name visit + File.create_rebuilt_project_from_visitor name visit with Visit.Typing_error s -> Options.abort "%s" s) diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml index 1a77b07266fd6f1285363aa79474643a230b1cac..0296ff7ab0c0f98505f75b486713a2bc991730f8 100644 --- a/src/plugins/e-acsl/visit.ml +++ b/src/plugins/e-acsl/visit.ml @@ -47,8 +47,8 @@ let mk_if acc e p = let convert_named_predicate acc generate p = let mk_if e = mk_if acc e p in match p.content with - | Pfalse -> if generate then mk_if (zero ~loc:unknown_loc) else acc - | Ptrue -> if generate then mk_if (one ~loc:unknown_loc) else acc + | Pfalse -> if generate then mk_if (one ~loc:unknown_loc) else acc + | Ptrue -> if generate then mk_if (zero ~loc:unknown_loc) else acc | Papp _ -> not_yet "logic function application" | Pseparated _ -> not_yet "separated" | Prel _ -> not_yet "relation"