Merge pull request #1011 from daniel-larraz/duplicate-const-arg

Fix node calls with same argument in constant and non-constant parameters

src/lustre/lustreTransSys.ml

@@ -796,16 +796,24 @@ let call_terms_of_node_call mk_fresh_state_var globals
        call_locals)
   in
 
+  let non_constant_inputs =
+    (* Filter out inputs that are constants FOR THE CALLEE. *)
+    D.fold2
+      (fun formal_idx formal_sv actual_sv acc ->
+        if StateVar.is_const formal_sv then acc
+        else D.add formal_idx actual_sv acc
+      )
+      inputs
+      call_inputs
+      D.empty
+    |> D.values
+  in
+
   (* Return actual parameters of transition relation at bound in the
      correct order *)
   let trans_params_of_bound term_of_state_var pre_term_of_state_var =
     init_params_of_bound term_of_state_var @ (
-      ( (D.values call_inputs) @ D.values call_outputs @ call_locals )
-      |> List.filter (
-        (* Filter out svars that are constants FOR THE CALLEE. *)
-        fun sv ->
-          SVM.find sv state_var_map_down |> StateVar.is_const |> not
-      )
+      ( non_constant_inputs @ D.values call_outputs @ call_locals )
       |> List.map pre_term_of_state_var
     )
   in

src/transSys.ml

@@ -20,7 +20,7 @@ open Lib
 
 module P = Property
 module SVM = StateVar.StateVarMap
-module SVS = StateVar.StateVarSet
+(* module SVS = StateVar.StateVarSet *)
 
 (* Offset of state variables in initial state constraint *)
 let init_base = Numeral.zero
@@ -1201,7 +1201,7 @@ let flatten_instances subsystems =
     subsystems 
 *)
 
-
+(*
 let rec map_cex_prop_to_subsystem' 
     filter_out_values
     ({ scope; subsystems } as trans_sys) 
@@ -1288,7 +1288,7 @@ let rec map_cex_prop_to_subsystem'
 
 let map_cex_prop_to_subsystem filter_out_values trans_sys cex prop = 
   map_cex_prop_to_subsystem' filter_out_values trans_sys [] cex prop 
-
+*)
 
 (*
 

src/transSys.mli

@@ -79,7 +79,10 @@ type instance =
 
     map_down : StateVar.t StateVar.StateVarMap.t;
     (** Map from the state variables of this system to the state
-        variables of the instance *)
+        variables of the instance. If the same variable is passed in
+        multiple arguments, the variable is only associated to
+        one of the formal parameters. Notice that for output and
+        local variables there is a one-to-one correspondence. *)
 
     map_up : StateVar.t StateVar.StateVarMap.t;
     (** Map from state variables of the called system to the state
@@ -365,7 +368,7 @@ val get_sofar_term: t -> Lib.position -> (Term.t * bool) option
 
 val get_max_depth : t -> int
 
-val map_cex_prop_to_subsystem : (Scope.t -> instance -> (StateVar.t * Model.value list) list ->  Model.value list -> Model.value list) -> t -> (StateVar.t * Model.value list) list -> Property.t -> t * instance list * (StateVar.t * Model.value list) list * Property.t 
+(*val map_cex_prop_to_subsystem : (Scope.t -> instance -> (StateVar.t * Model.value list) list ->  Model.value list -> Model.value list) -> t -> (StateVar.t * Model.value list) list -> Property.t -> t * instance list * (StateVar.t * Model.value list) list * Property.t *)
 
 (** {1 State Variables} *)
 

tests/regression/success/duplicate-const-arg.lus

@@ -0,0 +1,11 @@
+
+node M(const C:int; x:int) returns (y:int);
+let
+  y = x + C;
+tel
+
+node N(const C:int) returns (z:int);
+let
+   z = M(C, C);
+   --%PROPERTY z = 2*C;
+tel