From de5d11d62557b4e1ff84690d0bd81eef15a8e18e Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Fri, 14 Mar 2008 15:24:09 +0100
Subject: [PATCH] Translate assertions.
---
src/compiledData.ml | 4 ++--
src/evalEq.ml | 9 ++++++++-
src/evalEq.mli | 5 ++++-
src/lazyCompiler.ml | 5 +++--
src/test/should_work/call/call06.lus | 3 ++-
5 files changed, 19 insertions(+), 7 deletions(-)
diff --git a/src/compiledData.ml b/src/compiledData.ml
index 62608c0b..00a5fef9 100644
--- a/src/compiledData.ml
+++ b/src/compiledData.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 14/03/2008 (at 10:59) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/03/2008 (at 15:21) by Erwan Jahier> *)
(**
@@ -312,7 +312,7 @@ and node_def_eff =
| BodyEff of node_body_eff
and node_body_eff = {
- asserts_eff : (val_eff srcflagged) list;
+ asserts_eff : (val_exp_eff srcflagged) list;
eqs_eff : (eq_info_eff srcflagged) list;
}
diff --git a/src/evalEq.ml b/src/evalEq.ml
index abe6a37a..4b20930e 100644
--- a/src/evalEq.ml
+++ b/src/evalEq.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 14/03/2008 (at 09:45) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/03/2008 (at 15:17) by Erwan Jahier> *)
open Lxm
open SyntaxTreeCore
@@ -158,6 +158,13 @@ and (translate_slice_info : id_solver -> slice_info -> int -> Lxm.t ->
EvalConst.eval_array_slice id_solver si size lxm
+(**********************************************************************************)
+let (translate_assertions : CompiledData.id_solver ->
+ SyntaxTreeCore.val_exp Lxm.srcflagged ->
+ CompiledData.val_exp_eff Lxm.srcflagged) =
+ fun id_solver vef ->
+ Lxm.flagit (translate_val_exp id_solver vef.it) vef.src
+
(**********************************************************************************)
let (type_check: eq_info_eff srcflagged -> unit) =
diff --git a/src/evalEq.mli b/src/evalEq.mli
index 441b63ba..b43c39f0 100644
--- a/src/evalEq.mli
+++ b/src/evalEq.mli
@@ -1,6 +1,9 @@
-(** Time-stamp: <modified the 12/03/2008 (at 14:14) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/03/2008 (at 15:17) by Erwan Jahier> *)
val f : CompiledData.id_solver -> SyntaxTreeCore.eq_info Lxm.srcflagged ->
CompiledData.eq_info_eff Lxm.srcflagged
+
+val translate_assertions : CompiledData.id_solver ->
+ SyntaxTreeCore.val_exp Lxm.srcflagged -> CompiledData.val_exp_eff Lxm.srcflagged
diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml
index 2b3e2ef4..4e5566ae 100644
--- a/src/lazyCompiler.ml
+++ b/src/lazyCompiler.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 14/03/2008 (at 13:28) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/03/2008 (at 15:16) by Erwan Jahier> *)
open Lxm
@@ -602,7 +602,8 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
filled
*)
BodyEff {
- asserts_eff = []; (* XXX finish me! *)
+ asserts_eff =
+ List.map (EvalEq.translate_assertions node_id_solver) nb.asserts;
eqs_eff = List.map (EvalEq.f node_id_solver) nb.eqs;
}
)
diff --git a/src/test/should_work/call/call06.lus b/src/test/should_work/call/call06.lus
index c174ddfb..293cb36b 100644
--- a/src/test/should_work/call/call06.lus
+++ b/src/test/should_work/call/call06.lus
@@ -3,5 +3,6 @@ extern function bip(x,y : bool) returns (z,t : bool);
node call06(x,y : bool) returns (z,t : bool);
let
- (z,t) = bip(x,y);
+ assert (x=>z);
+ (z,t) = bip(x,y);
tel
--
GitLab