From eba2f8069ca83c46adbce7bcf1ae6bda97092cf0 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 2 Mar 2011 10:28:50 +0000
Subject: [PATCH] use File.create_rebuilt_project_from_visitor + bug fixed with
predicate false and true
---
src/plugins/e-acsl/main.ml | 2 +-
src/plugins/e-acsl/visit.ml | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 959e309b8c0..f3b84c5c309 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 1a77b07266f..0296ff7ab0c 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"
--
GitLab