summaryrefslogtreecommitdiff
path: root/frontend
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-26 16:57:10 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-26 16:57:10 +0200
commitf3d89408ebb44f77f257b2cb51a4bdd74b9268d0 (patch)
treeadc4b2505f907ea031c0a8d082b077702d8f49eb /frontend
parentdcdcedf42c8c3a3041c0fcda6a5a3362777672f5 (diff)
downloadscade-analyzer-f3d89408ebb44f77f257b2cb51a4bdd74b9268d0.tar.gz
scade-analyzer-f3d89408ebb44f77f257b2cb51a4bdd74b9268d0.zip
Many things, sorry for the mess.
- Implement two new enumeration domains (they don't bring us much) : multi valuation for variables ; multi valuation for variables and pairs of variables (not really sure it works) - Make it so that the number of init/time variables is reduced (do not create new init/time variables on node instanciation, only inside activate blocks and automaton states) - Some work on EDD (it is currently broken and does not compile)
Diffstat (limited to 'frontend')
-rw-r--r--frontend/typing.ml53
1 files changed, 30 insertions, 23 deletions
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 0f19b93..167caea 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -117,7 +117,26 @@ let node_vars p f nid =
vars_in_node nid (decls_of_node n)
(*
- extract_all_vars : prog -> scope -> var list
+ clock_vars : rooted_prog -> scope -> var list
+*)
+let clock_vars rp (node, prefix, _) =
+ let v =
+ if not (rp.no_time_scope (node^"/"))
+ then
+ [
+ false, node^"/"^prefix^"time", TInt;
+ false, "N"^node^"/"^prefix^"time", TInt]
+ else [] in
+ let v =
+ if rp.init_scope (node^"/")
+ then
+ (false, node^"/"^prefix^"init", bool_type)::
+ (false, "N"^node^"/"^prefix^"init", bool_type)::v
+ else v in
+ v
+
+(*
+ extract_all_vars : rooted_prog -> scope -> var list
Extracts all variables with names given according to
naming convention used here and in transform.ml :
@@ -154,10 +173,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
let rec do_branch = function
| AST_activate_body b ->
let bvars = vars_in_node node b.act_locals in
- bvars @
- extract_all_vars rp
- (node, b.act_id^".", b.body)
- (bvars@n_vars)
+ let b_scope = node, b.act_id^".", b.body in
+ bvars @ clock_vars rp b_scope @
+ extract_all_vars rp b_scope (bvars@n_vars)
| AST_activate_if(c, a, b) ->
vars_of_expr c @ do_branch a @ do_branch b
in do_branch b
@@ -167,11 +185,10 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
List.flatten
(List.map (fun (e, _, _) -> vars_of_expr e) st.until)
in
+ let st_scope = (node, aid^"."^st.st_name^".", st.body) in
let svars = vars_in_node node st.st_locals in
- svars @ tvars @
- extract_all_vars rp
- (node, aid^"."^st.st_name^".", st.body)
- (tvars@n_vars)
+ svars @ tvars @ clock_vars rp st_scope @
+ extract_all_vars rp st_scope (tvars@n_vars)
in
let st_ids = List.map (fun (st, _) -> st.st_name) states in
(false, node^"/"^aid^".state", TEnum st_ids)::
@@ -179,18 +196,6 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
(List.flatten (List.map do_state states))
in
let v = List.flatten (List.map vars_of_eq eqs) in
- let v =
- if not (rp.no_time_scope (node^"/"))
- then
- (false, node^"/"^prefix^"time", TInt)::
- (false, "N"^node^"/"^prefix^"time", TInt)::v
- else v in
- let v =
- if rp.init_scope (node^"/")
- then
- (false, node^"/"^prefix^"init", bool_type)::
- (false, "N"^node^"/"^prefix^"init", bool_type)::v
- else v in
v
@@ -208,7 +213,6 @@ let root_prog p root no_time_scope init_scope =
(extract_const_decls p)
in
- let root_vars = vars_in_node "" (decls_of_node root_node) in
let rp = {
p; root_scope; root_node;
@@ -219,6 +223,9 @@ let root_prog p root no_time_scope init_scope =
const_vars;
all_vars = [] } in
- { rp with all_vars = root_vars @ extract_all_vars rp root_scope root_vars }
+ let root_vars = vars_in_node "" (decls_of_node root_node) in
+ let root_clock_vars = clock_vars rp root_scope in
+
+ { rp with all_vars = root_clock_vars @ root_vars @ extract_all_vars rp root_scope root_vars }