Remove ETX operator from AL

Reviewed By: dulmarod

Differential Revision: D5804550

fbshipit-source-id: 24f3b7f

infer/lib/linter_rules/linters.al

@@ -61,10 +61,8 @@ DEFINE-CHECKER BAD_POINTER_COMPARISON = {
 						is_nsnumber
 					);
 
-  LET etx =
+  LET etx = eu HOLDS-NEXT WITH-TRANSITION Cond;
-		IN-EXCLUSIVE-NODE IfStmt, ForStmt, WhileStmt, ConditionalOperator WITH-TRANSITION Cond
+
-				(eu)
-		HOLDS-EVENTUALLY;
 
  	SET report_when =
 					WHEN

infer/src/clang/cFrontend_errors.ml

@@ -261,8 +261,7 @@ let rec apply_substitution f sub =
    -> EG (trans, apply_substitution f1 sub)
   | ET (ntl, sw, f1)
    -> ET (sub_list_param ntl, sw, apply_substitution f1 sub)
-  | ETX (ntl, sw, f1)
+
-   -> ETX (sub_list_param ntl, sw, apply_substitution f1 sub)
 
 let expand_formula phi _map _error_msg =
   let fail_with_circular_macro_definition name error_msg =
@@ -323,8 +322,6 @@ let expand_formula phi _map _error_msg =
      -> EG (trans, expand f1 map error_msg)
     | ET (tl, sw, f1)
      -> ET (tl, sw, expand f1 map error_msg)
-    | ETX (tl, sw, f1)
-     -> ETX (tl, sw, expand f1 map error_msg)
   in
   expand phi _map _error_msg
 

infer/src/clang/cTL.ml

@@ -58,7 +58,7 @@ type t =
   | EU of transitions option * t * t
   | EH of ALVar.alexp list * t
   | ET of ALVar.alexp list * transitions option * t
-  | ETX of ALVar.alexp list * transitions option * t
+
 
 let has_transition phi =
   match phi with
@@ -81,7 +81,6 @@ let has_transition phi =
   | EG (trans_opt, _)
   | EU (trans_opt, _, _)
   | ET (_, trans_opt, _)
-  | ETX (_, trans_opt, _)
    -> Option.is_some trans_opt
 
 (* "set" clauses are used for defining mandatory variables that will be used
@@ -193,9 +192,6 @@ module Debug = struct
     | ET (arglist, trans, phi)
      -> Format.fprintf fmt "ET[%a][%a](%a)" (Pp.comma_seq Format.pp_print_string)
           (nodes_to_string arglist) pp_transition trans pp_formula phi
-    | ETX (arglist, trans, phi)
-     -> Format.fprintf fmt "ETX[%a][%a](%a)" (Pp.comma_seq Format.pp_print_string)
-          (nodes_to_string arglist) pp_transition trans pp_formula phi
 
   let pp_ast ~ast_node_to_highlight ?(prettifier= Fn.id) fmt root =
     let pp_node_info fmt an =
@@ -982,27 +978,6 @@ and eval_ET tl trs phi an lcxt =
   in
   eval_formula f an lcxt
 
-and eval_ETX tl trs phi an lcxt =
-  let lcxt', tl' =
-    match (lcxt.CLintersContext.et_evaluation_node, Ctl_parser_types.ast_node_has_kind tl an) with
-    | None, true
-     -> let an_alexp = ALVar.Const (Ctl_parser_types.ast_node_kind an) in
-        ( { lcxt with
-            CLintersContext.et_evaluation_node=
-              Some (Ctl_parser_types.ast_node_unique_string_id an) }
-        , [an_alexp] )
-    | _, _
-     -> (lcxt, tl)
-  in
-  let f =
-    match trs with
-    | Some _
-     -> EF (None, InNode (tl', EX (trs, phi)))
-    | None
-     -> EF (None, InNode (tl', phi))
-  in
-  eval_formula f an lcxt'
-
 (* Formulas are evaluated on a AST node an and a linter context lcxt *)
 and eval_formula f an lcxt : Ctl_parser_types.ast_node option =
   debug_eval_begin (debug_create_payload an f lcxt) ;
@@ -1045,7 +1020,5 @@ and eval_formula f an lcxt : Ctl_parser_types.ast_node option =
         eval_formula (And (f1, EX (trans, EG (trans, f1)))) an lcxt
     | ET (tl, sw, phi)
      -> eval_ET tl sw phi an lcxt
-    | ETX (tl, sw, phi)
-     -> eval_ETX tl sw phi an lcxt
   in
   debug_eval_end res ; res

infer/src/clang/cTL.mli

@@ -71,10 +71,7 @@ type t =
       (** ET[T][l] phi <=>
                                                                there exists a descentant an of the current node such that an is of type in set T
                                                                making a transition to a node an' via label l, such that in an phi holds. *)
-  | ETX of ALVar.alexp list * transitions option * t
+
-      (** ET[T][l] phi <=>
-                                                               there exists a descentant an of the current node such that an is of type in set T
-                                                               making a transition to a node an' via label l, such that in an phi holds. *)
 
 (* "set" clauses are used for defining mandatory variables that will be used
    by when reporting issues: eg for defining the condition.

infer/src/clang/ctl_lexer.mll

@@ -43,7 +43,6 @@ rule token = parse
   | "HOLDS-EVERYWHERE-ALWAYS" { AG }
   | "HOLDS-IN-SOME-SUPERCLASS-OF" { EH }
   | "IN-NODE" { ET }
-  | "IN-EXCLUSIVE-NODE" { ETX }
   | "WHEN" { WHEN }
   | "HOLDS-IN-NODE" { HOLDS_IN_NODE }
   | "WITH-TRANSITION" {WITH_TRANSITION}

infer/src/clang/ctl_parser.mly

@@ -51,7 +51,6 @@
 %token LESS_THAN
 %token GREATER_THAN
 %token ET
-%token ETX
 %token WITH_TRANSITION
 %token WHEN
 %token HOLDS_IN_NODE
@@ -280,9 +279,6 @@ formula:
   | ET node_list WITH_TRANSITION transition_label formula_EF
      { L.(debug Linters Verbose) "\tParsed ET with transition '%a'@\n" CTL.Debug.pp_transition $4;
        CTL.ET ($2, $4, $5)}
-  | ETX node_list WITH_TRANSITION transition_label formula_EF
-     { L.(debug Linters Verbose) "\tParsed ETX ith transition '%a'@\n" CTL.Debug.pp_transition $4;
-       CTL.ETX ($2, $4, $5)}
   | EX WITH_TRANSITION transition_label formula_with_paren
     { L.(debug Linters Verbose) "\tParsed EX with transition '%a'@\n" CTL.Debug.pp_transition $3;
       CTL.EX ($3, $4)}