ThingML Checker

[brice-morin]

This issue is to discuss the set of rules that should be checked in the future ThingML checker. This will be used e.g. by the compilers to refuse to generate erroneous code, warn about potential problems and perform some optimization (remove dead code, etc).

• [X] [NOTICE] non-connected port (some messages could be lost)
• [X] [NOTICE] cycle in connectors (could create some deadlocks, though this is likely to be properly handled in the generated code)
• [X] [ERROR] internal auto transition (with no event): this will loop (With guard => NOTICE)
• [X] [WARN] cycle of auto transition: this is very likely to loop (depending on if the scheduler prioritizes empty events, which in theory it should).
• [X] [WARN] message never sent (a port declares more sends messages than the implementation actually uses)
• [X] [NOTICE] message never received (a port declares more receives messages than the implementation actually uses)
• [ ] [WARN] properties/variables never read
• [X] [WARN] function never called
• [X] [ERROR] function called with wrong number of parameters
• [X] [ERROR] message sent with wrong number of parameters
• [X] [WARN] non-reachable state (no transition points to this state)
• [X] [NOTICE] sink state (no transition go out of this state, which in some cases might be OK)
• [X] [ERROR] two outgoing transition on the same state with the same trigger and no guard (indeterminism)
• [X] [WARN] two outgoing transition on the same state with the same trigger and guard (potential indeterminism if both guards evaluate to true at runtime) (Done only if one transition has no guard)
• [X] [ERROR][Arduino] when a message with a string parameter is used on an asynchronous port
• [X] [WARN]/[ERROR][C] When a pointer is passed as argument of a message (for C compilers)
• [X] [WARN]/[ERROR][C] When an array is declared without cardinality (for C compilers)
• [ ] [WARN]/[ERROR] Basic type checking (we will not develop a fully fledged type checker), to avoid writing 2 and true or "debug myVar = " + 2 or expressions that reduce to that kind of non-sense

[nharrand]

We can add:

• [ERROR] when a message with a string parameter is used on an asynchronous port on arduino

About

• [WARN] non-connected port (some messages could be lost)
• [WARN] message never sent/received

I'm afraid it is a common case when libraries are used (One does not always need each option of a library)

[brice-morin]

Yes, that is why it is just warning. As in Java, we could imagine having some annotation to ignore some warning, so that the developer explicitly takes the responsibility of ignoring the warning when he knows what he is doing.

[nharrand]

We should also add

• [WARN]/[ERROR] When a pointer is passed as argument of a message (for C compilers)