Module LustreSyntaxChecks

Check various syntactic properties that do not depend on type information

module LA = LustreAst
type error_kind =
  1. | Unknown of string
  2. | UndefinedLocal of HString.t
  3. | DuplicateLocal of HString.t * Lib.position
  4. | DuplicateOutput of HString.t * Lib.position
  5. | UndefinedOutput of HString.t
  6. | DuplicateProperty of HString.t
  7. | InvalidPropertyName of HString.t
  8. | UndefinedNode of HString.t
  9. | UndefinedContract of HString.t
  10. | DanglingIdentifier of HString.t
  11. | QuantifiedVariableInPre of string * HString.t
  12. | QuantifiedVariableInNodeArgument of HString.t * HString.t
  13. | QuantifiedPatternVariableInNodeArgument of HString.t * HString.t * HString.t
  14. | SymbolicArrayIndexInNodeArgument of HString.t * HString.t
  15. | SymbolicArrayIndexInRestart of HString.t
  16. | QuantifiedVariableInLazyGuardedNodeCall of HString.t * HString.t
  17. | SymbolicArrayIndexInLazyGuardedNodeCall of HString.t * HString.t
  18. | QuantifiedVariableInLazyGuardedTemporalBranch of HString.t
  19. | SymbolicArrayIndexInLazyGuardedTemporalBranch of HString.t
  20. | SymbolicArrayIndexInTemporalBranch of HString.t
  21. | QuantifiedPatternVariableInTemporalBranch of HString.t * HString.t
  22. | QuantifiedVariableInTypeAscription of HString.t
  23. | SymbolicArrayIndexInTypeAscription of HString.t
  24. | IllegalNodeCall of HString.t * string
  25. | IllegalAnyOp of string
  26. | NodeCallInConstant of HString.t
  27. | NodeCallInGlobalTypeDecl of HString.t
  28. | IllegalTemporalOperator of string * string
  29. | IllegalImportOfContractWithNodeCall of HString.t
  30. | UnsupportedClockedInputOrOutput
  31. | UnsupportedClockedLocal of HString.t
  32. | UnsupportedExpression of LustreAst.expr
  33. | IllegalInRestartBlock of string
  34. | IllegalRestartBlock of string
  35. | UnsupportedParametricDeclaration
  36. | UnsupportedAssignment
  37. | MissingComprehensionSize of HString.t
  38. | UnboundedComprehensionIndex of HString.t
  39. | DuplicateComprehensionIndex of HString.t
  40. | ComprehensionSizeMentionsIndex of HString.t * HString.t
  41. | BooleanComprehensionSize of HString.t * LustreAst.expr
  42. | ArrayDefinition of HString.t * HString.t list * LustreAst.expr list option
  43. | AssumptionVariablesInContractNode
  44. | MisplacedVarInFrameBlock of LustreAst.ident
  45. | MisplacedAssertInFrameBlock
  46. | OpaqueWithoutContract of LustreAst.ident
  47. | LemmaWithoutContract of LustreAst.ident
  48. | TransparentWithoutBody of LustreAst.ident
  49. | IllegalHistoryVar of LustreAst.ident
  50. | InductiveVarsWithArrayConstr of LustreAst.expr
  51. | DuplicatePatternVariable of HString.t
  52. | AssignmentToPatternVariable of HString.t
  53. | MissingDecreasesClause of HString.t
  54. | IllegalDecreasesMeasure of HString.t
  55. | CallInDecreasesMeasure of HString.t
  56. | OperatorInDecreasesMeasure of string
  57. | UnsupportedDecreasesMeasure
  58. | MultipleDecreasesClauses of HString.t
  59. | DecreasesClauseInContractNodeDecl of HString.t
  60. | MisplacedDecreasesClause of HString.t
  61. | DecreasesClauseInLemmaWithoutBody of HString.t
  62. | MisplacedAuto
  63. | LemmaCallOutsideCallStatement of HString.t
  64. | CallStatementCallsNonLemma of HString.t
  65. | InvalidUnderscore
type error = [
  1. | `LustreSyntaxChecksError of Lib.position * error_kind
]
val error_message : error_kind -> string
type warning_kind =
  1. | UnusedBoundVariableWarning of HString.t
type warning = [
  1. | `LustreSyntaxChecksWarning of Lib.position * warning_kind
]
val warning_message : warning_kind -> string
val error_if_lus_strict : warning_kind -> bool
val syntax_check : LA.t -> ([> warning ] list * LA.t, [> error ]) Stdlib.result
val no_quant_vars_in_calls_to_non_inlinable_funcs : TypeCheckerContext.tc_context -> NodeId.Set.t -> NodeId.Set.t -> LA.t -> ([> warning ] list, [> error ]) Stdlib.result

no_quant_vars_in_calls_to_non_inlinable_funcs tc_ctx inlinable_funcs uf_callable_funcs ast checks that no quantified variable is in an argument of a call to a node or function that is neither in inlinable_funcs nor in uf_callable_funcs, the recursive functions a call applied to quantified variables is compiled to an application of (see LustreUserFunctions.uf_callable_functions). Both sets are those the normalizer is given.