From d93b723f741213e11120d598640efa9ecb65f0ea Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 19 Mar 2020 09:25:18 +0100
Subject: [PATCH] [Cabs] Lint
---
.Makefile.lint | 1 -
src/kernel_services/parsetree/cabs.ml | 234 +++++++++++++-------------
2 files changed, 117 insertions(+), 118 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 5c046710443..bf8a261de3b 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -95,7 +95,6 @@ ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_state.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_state.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/typed_parameter.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/typed_parameter.mli
-ML_LINT_KO+=src/kernel_services/parsetree/cabs.ml
ML_LINT_KO+=src/kernel_services/parsetree/cabshelper.ml
ML_LINT_KO+=src/kernel_services/parsetree/cabshelper.mli
ML_LINT_KO+=src/kernel_services/parsetree/logic_ptree.mli
diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml
index 3db49d24d3d..9294f5b774a 100644
--- a/src/kernel_services/parsetree/cabs.ml
+++ b/src/kernel_services/parsetree/cabs.ml
@@ -51,7 +51,7 @@
type cabsloc = Filepath.position * Filepath.position
type typeSpecifier = (* Merge all specifiers into one type *)
- Tvoid (* Type specifier ISO 6.7.2 *)
+ | Tvoid (* Type specifier ISO 6.7.2 *)
| Tchar
| Tbool
| Tshort
@@ -75,10 +75,10 @@ type typeSpecifier = (* Merge all specifiers into one type *)
| TtypeofT of specifier * decl_type (* GCC __typeof__ *)
and storage =
- NO_STORAGE | AUTO | STATIC | EXTERN | REGISTER
+ | NO_STORAGE | AUTO | STATIC | EXTERN | REGISTER
and funspec =
- INLINE | VIRTUAL | EXPLICIT
+ | INLINE | VIRTUAL | EXPLICIT
and cvspec =
| CV_CONST | CV_VOLATILE | CV_RESTRICT
@@ -90,7 +90,7 @@ and cvspec =
(* on to the compiler. Thus, we can represent e.g. 'int long float x' even *)
(* though the compiler will of course choke. *)
and spec_elem =
- SpecTypedef
+ | SpecTypedef
| SpecCV of cvspec (* const/volatile *)
| SpecAttr of attribute (* __attribute__ *)
| SpecStorage of storage
@@ -107,23 +107,23 @@ and specifier = spec_elem list
* constructor for ARRAY and PTR is the inner-level in the meaning of the
* declared type) *)
and decl_type =
- | JUSTBASE (* Prints the declared name *)
- | PARENTYPE of attribute list * decl_type * attribute list
- (* Prints "(attrs1 decl attrs2)".
- * attrs2 are attributes of the
- * declared identifier and it is as
- * if they appeared at the very end
- * of the declarator. attrs1 can
- * contain attributes for the
- * identifier or attributes for the
- * enclosing type. *)
- | ARRAY of decl_type * attribute list * expression
- (* Prints "decl [ attrs exp ]".
- * decl is never a PTR. *)
- | PTR of attribute list * decl_type (* Prints "* attrs decl" *)
- | PROTO of decl_type * single_name list * single_name list * bool
- (* Prints "decl (args[, ...])".
- * decl is never a PTR.*)
+ | JUSTBASE (* Prints the declared name *)
+ | PARENTYPE of attribute list * decl_type * attribute list
+ (* Prints "(attrs1 decl attrs2)".
+ * attrs2 are attributes of the
+ * declared identifier and it is as
+ * if they appeared at the very end
+ * of the declarator. attrs1 can
+ * contain attributes for the
+ * identifier or attributes for the
+ * enclosing type. *)
+ | ARRAY of decl_type * attribute list * expression
+ (* Prints "decl [ attrs exp ]".
+ * decl is never a PTR. *)
+ | PTR of attribute list * decl_type (* Prints "* attrs decl" *)
+ | PROTO of decl_type * single_name list * single_name list * bool
+ (* Prints "decl (args[, ...])".
+ * decl is never a PTR.*)
(* The base type and the storage are common to all names. Each name might
* contain type or storage modifiers *)
@@ -160,19 +160,19 @@ and enum_item = string * expression * cabsloc
** Declaration definition (at toplevel)
*)
and definition =
- FUNDEF of
- (Logic_ptree.spec*cabsloc) option * single_name * block *
- cabsloc * cabsloc
- | DECDEF of (Logic_ptree.spec*cabsloc) option * init_name_group * cabsloc
- (* global variable(s), or function prototype *)
- | TYPEDEF of name_group * cabsloc
- | ONLYTYPEDEF of specifier * cabsloc
- | GLOBASM of string * cabsloc
- | PRAGMA of expression * cabsloc
- | LINKAGE of string * cabsloc * definition list (* extern "C" { ... } *)
- | GLOBANNOT of Logic_ptree.decl list
- (** Logical declaration (axiom, logic, etc.)*)
- | CUSTOM of Logic_ptree.custom_tree * string * cabsloc
+ | FUNDEF of
+ (Logic_ptree.spec*cabsloc) option * single_name * block *
+ cabsloc * cabsloc
+ | DECDEF of (Logic_ptree.spec*cabsloc) option * init_name_group * cabsloc
+ (* global variable(s), or function prototype *)
+ | TYPEDEF of name_group * cabsloc
+ | ONLYTYPEDEF of specifier * cabsloc
+ | GLOBASM of string * cabsloc
+ | PRAGMA of expression * cabsloc
+ | LINKAGE of string * cabsloc * definition list (* extern "C" { ... } *)
+ | GLOBANNOT of Logic_ptree.decl list
+ (** Logical declaration (axiom, logic, etc.)*)
+ | CUSTOM of Logic_ptree.custom_tree * string * cabsloc
(** the file name, and then the list of toplevel forms.
@plugin development guide *)
@@ -186,92 +186,92 @@ and file = Datatype.Filepath.t * (bool * definition) list
(* A block contains a list of local label declarations ( GCC's ({ __label__
* l1, l2; ... }) ) , a list of definitions and a list of statements *)
and block =
- { blabels: string list;
- battrs: attribute list;
- bstmts: statement list
- }
+ { blabels: string list;
+ battrs: attribute list;
+ bstmts: statement list
+ }
(* GCC asm directives have lots of extra information to guide the optimizer *)
and asm_details =
- { aoutputs: (string option * string * expression) list; (* optional name, constraints and expressions for outputs *)
- ainputs: (string option * string * expression) list; (* optional name, constraints and expressions for inputs *)
- aclobbers: string list; (* clobbered registers *)
- alabels: string list (* the labels for "asm goto" statements in gcc >= 4.6 *)
- }
+ { aoutputs: (string option * string * expression) list; (* optional name, constraints and expressions for outputs *)
+ ainputs: (string option * string * expression) list; (* optional name, constraints and expressions for inputs *)
+ aclobbers: string list; (* clobbered registers *)
+ alabels: string list (* the labels for "asm goto" statements in gcc >= 4.6 *)
+ }
and raw_statement =
- NOP of cabsloc
- | COMPUTATION of expression * cabsloc
- | BLOCK of block * cabsloc * cabsloc
- | SEQUENCE of statement * statement * cabsloc
- | IF of expression * statement * statement * cabsloc
- | WHILE of loop_invariant * expression * statement * cabsloc
- | DOWHILE of loop_invariant * expression * statement * cabsloc
- | FOR of loop_invariant *
- for_clause * expression * expression * statement * cabsloc
- | BREAK of cabsloc
- | CONTINUE of cabsloc
- | RETURN of expression * cabsloc
- | SWITCH of expression * statement * cabsloc
- | CASE of expression * statement * cabsloc
- | CASERANGE of expression * expression * statement * cabsloc
- | DEFAULT of statement * cabsloc
- | LABEL of string * statement * cabsloc
- | GOTO of string * cabsloc
- | COMPGOTO of expression * cabsloc (* GCC's "goto *exp" *)
- | DEFINITION of definition (*definition or declaration of a variable or type*)
-
- | ASM of attribute list * (* typically only volatile and const *)
- string list * (* template *)
- asm_details option * (* extra details to guide GCC's optimizer *)
- cabsloc
-
-(* Exception mechanism *)
- | THROW of expression option * cabsloc
- (** throws the corresponding expression. [None] corresponds to
- re-throwing the exception currently being caught (thus is only
- meaningful in a catch clause). This node is not generated by the
- C parser, but can be used by external front-ends.
+ | NOP of cabsloc
+ | COMPUTATION of expression * cabsloc
+ | BLOCK of block * cabsloc * cabsloc
+ | SEQUENCE of statement * statement * cabsloc
+ | IF of expression * statement * statement * cabsloc
+ | WHILE of loop_invariant * expression * statement * cabsloc
+ | DOWHILE of loop_invariant * expression * statement * cabsloc
+ | FOR of loop_invariant *
+ for_clause * expression * expression * statement * cabsloc
+ | BREAK of cabsloc
+ | CONTINUE of cabsloc
+ | RETURN of expression * cabsloc
+ | SWITCH of expression * statement * cabsloc
+ | CASE of expression * statement * cabsloc
+ | CASERANGE of expression * expression * statement * cabsloc
+ | DEFAULT of statement * cabsloc
+ | LABEL of string * statement * cabsloc
+ | GOTO of string * cabsloc
+ | COMPGOTO of expression * cabsloc (* GCC's "goto *exp" *)
+ | DEFINITION of definition (*definition or declaration of a variable or type*)
+
+ | ASM of attribute list * (* typically only volatile and const *)
+ string list * (* template *)
+ asm_details option * (* extra details to guide GCC's optimizer *)
+ cabsloc
+
+ (* Exception mechanism *)
+ | THROW of expression option * cabsloc
+ (** throws the corresponding expression. [None] corresponds to
+ re-throwing the exception currently being caught (thus is only
+ meaningful in a catch clause). This node is not generated by the
+ C parser, but can be used by external front-ends.
*)
- | TRY_CATCH of statement * (single_name option * statement) list * cabsloc
- (** [TRY_CATCH(s,clauses,loc)] catches exceptions thrown by execution of
- [s], according to [clauses]. An
- exception [e] is caught by the first clause
- [(spec,(name, decl, _, _)),body]
- such that the type of [e] is compatible with [(spec,decl)]. [name]
- is then associated to a copy of [e], and [body] is executed. If the
- [single_name] is [None], all exceptions are caught by the corresponding
- clause.
-
- The corresponding [TryCatch] node in {!Cil_types.stmtkind} has a refined
- notion of catching that allows a clause to match for more than
- one type using appropriate conversions
- (see also {!Cil_types.catch_binder}).
-
- This node is not generated by the C parser, but can be used by external
- front-ends.
- *)
-
- (** MS SEH *)
- | TRY_EXCEPT of block * expression * block * cabsloc
- | TRY_FINALLY of block * block * cabsloc
- (* annotations *)
- | CODE_ANNOT of (Logic_ptree.code_annot * cabsloc)
- | CODE_SPEC of (Logic_ptree.spec * cabsloc)
+ | TRY_CATCH of statement * (single_name option * statement) list * cabsloc
+ (** [TRY_CATCH(s,clauses,loc)] catches exceptions thrown by execution of
+ [s], according to [clauses]. An
+ exception [e] is caught by the first clause
+ [(spec,(name, decl, _, _)),body]
+ such that the type of [e] is compatible with [(spec,decl)]. [name]
+ is then associated to a copy of [e], and [body] is executed. If the
+ [single_name] is [None], all exceptions are caught by the corresponding
+ clause.
+
+ The corresponding [TryCatch] node in {!Cil_types.stmtkind} has a refined
+ notion of catching that allows a clause to match for more than
+ one type using appropriate conversions
+ (see also {!Cil_types.catch_binder}).
+
+ This node is not generated by the C parser, but can be used by external
+ front-ends.
+ *)
+
+ (** MS SEH *)
+ | TRY_EXCEPT of block * expression * block * cabsloc
+ | TRY_FINALLY of block * block * cabsloc
+ (* annotations *)
+ | CODE_ANNOT of (Logic_ptree.code_annot * cabsloc)
+ | CODE_SPEC of (Logic_ptree.spec * cabsloc)
and statement = { mutable stmt_ghost: bool; stmt_node:raw_statement }
and loop_invariant = Logic_ptree.code_annot list
and for_clause =
- FC_EXP of expression
- | FC_DECL of definition
+ | FC_EXP of expression
+ | FC_DECL of definition
(*
** Expressions
*)
and binary_operator =
- ADD | SUB | MUL | DIV | MOD
+ | ADD | SUB | MUL | DIV | MOD
| AND | OR
| BAND | BOR | XOR | SHL | SHR
| EQ | NE | LT | GT | LE | GE
@@ -280,25 +280,25 @@ and binary_operator =
| BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
and unary_operator =
- MINUS | PLUS | NOT | BNOT | MEMOF | ADDROF
+ | MINUS | PLUS | NOT | BNOT | MEMOF | ADDROF
| PREINCR | PREDECR | POSINCR | POSDECR
and expression = { expr_loc : cabsloc; expr_node: cabsexp }
and cabsexp =
- NOTHING
+ | NOTHING
| UNARY of unary_operator * expression
| LABELADDR of string (* GCC's && Label *)
| BINARY of binary_operator * expression * expression
| QUESTION of expression * expression * expression
- (* A CAST can actually be a constructor expression *)
+ (* A CAST can actually be a constructor expression *)
| CAST of (specifier * decl_type) * init_expression
- (* There is a special form of CALL in which the function called is
- __builtin_va_arg and the second argument is sizeof(T). This
- should be printed as just T *)
+ (* There is a special form of CALL in which the function called is
+ __builtin_va_arg and the second argument is sizeof(T). This
+ should be printed as just T *)
| CALL of expression * expression list * expression list
| COMMA of expression list
| CONSTANT of constant
@@ -321,11 +321,11 @@ and constant =
| CONST_WCHAR of int64 list
| CONST_STRING of string
| CONST_WSTRING of int64 list
- (* ww: wstrings are stored as an int64 list at this point because
- * we might need to feed the wide characters piece-wise into an
- * array initializer (e.g., wchar_t foo[] = L"E\xabcd";). If that
- * doesn't happen we will convert it to an (escaped) string before
- * passing it to Cil. *)
+ (* ww: wstrings are stored as an int64 list at this point because
+ * we might need to feed the wide characters piece-wise into an
+ * array initializer (e.g., wchar_t foo[] = L"E\xabcd";). If that
+ * doesn't happen we will convert it to an (escaped) string before
+ * passing it to Cil. *)
and init_expression =
| NO_INIT
@@ -333,14 +333,14 @@ and init_expression =
| COMPOUND_INIT of (initwhat * init_expression) list
and initwhat =
- NEXT_INIT
+ | NEXT_INIT
| INFIELD_INIT of string * initwhat
| ATINDEX_INIT of expression * initwhat
| ATINDEXRANGE_INIT of expression * expression
- (* Each attribute has a name and some
- * optional arguments *)
+(* Each attribute has a name and some
+ * optional arguments *)
and attribute = string * expression list
(*
--
GitLab