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. | SymbolicArrayIndexInNodeArgument of HString.t * HString.t
  14. | SymbolicArrayIndexInRestart of HString.t
  15. | QuantifiedVariableInLazyGuardedNodeCall of HString.t * HString.t
  16. | SymbolicArrayIndexInLazyGuardedNodeCall of HString.t * HString.t
  17. | QuantifiedVariableInLazyGuardedTemporalBranch of HString.t
  18. | SymbolicArrayIndexInLazyGuardedTemporalBranch of HString.t
  19. | QuantifiedVariableInTypeAscription of HString.t
  20. | SymbolicArrayIndexInTypeAscription of HString.t
  21. | IllegalNodeCall of HString.t * string
  22. | IllegalAnyOp of string
  23. | NodeCallInConstant of HString.t
  24. | NodeCallInGlobalTypeDecl of HString.t
  25. | IllegalTemporalOperator of string * string
  26. | IllegalImportOfStatefulContract of HString.t
  27. | UnsupportedClockedInputOrOutput
  28. | UnsupportedClockedLocal of HString.t
  29. | UnsupportedExpression of LustreAst.expr
  30. | IllegalInRestartBlock of string
  31. | IllegalRestartBlock of string
  32. | UnsupportedParametricDeclaration
  33. | UnsupportedAssignment
  34. | MissingComprehensionSize of HString.t
  35. | UnboundedComprehensionIndex of HString.t
  36. | DuplicateComprehensionIndex of HString.t
  37. | ComprehensionSizeMentionsIndex of HString.t * HString.t
  38. | BooleanComprehensionSize of HString.t * LustreAst.expr
  39. | ArrayDefinition of HString.t * HString.t list * LustreAst.expr list option
  40. | AssumptionVariablesInContractNode
  41. | MisplacedVarInFrameBlock of LustreAst.ident
  42. | MisplacedAssertInFrameBlock
  43. | OpaqueWithoutContract of LustreAst.ident
  44. | LemmaWithoutContract of LustreAst.ident
  45. | TransparentWithoutBody of LustreAst.ident
  46. | IllegalHistoryVar of LustreAst.ident
  47. | InductiveVarsWithArrayConstr of LustreAst.expr
  48. | DuplicatePatternVariable of HString.t
  49. | AssignmentToPatternVariable of HString.t
  50. | MissingDecreasesClause of HString.t
  51. | IllegalDecreasesMeasure of HString.t
  52. | CallInDecreasesMeasure of HString.t
  53. | OperatorInDecreasesMeasure of string
  54. | UnsupportedDecreasesMeasure
  55. | MultipleDecreasesClauses of HString.t
  56. | DecreasesClauseInContractNodeDecl of HString.t
  57. | MisplacedDecreasesClause of HString.t
  58. | DecreasesClauseInLemmaWithoutBody of HString.t
  59. | MisplacedAuto
  60. | LemmaCallOutsideCallStatement of HString.t
  61. | CallStatementCallsNonLemma of HString.t
  62. | 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.